---

Step * of Lemma qexp-eq-q-rng-nexp

∀[n:ℕ]. ∀[r:ℚ].  (r ↑ n = q-rng-nexp(r;n) ∈ ℚ)
BY
{ xxx(Auto
      THEN Unfold `qexp` 0
      THEN (CallByValueReduce 0 THENA Auto)
      THEN (GenConclAtAddr [2;1] THENA Auto)
      THEN D -2
      THEN Reduce 0)xxx }

1
1. n : ℕ
2. r : ℚ
3. v1 : ℤ
4. v2 : ℕ+
5. qrep(r) = <v1, v2> ∈ (ℤ × ℕ+)
⊢ mk-rational(v1^n;v2^n) = q-rng-nexp(r;n) ∈ ℚ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[r:\mBbbQ{}].    (r  \muparrow{}  n  =  q-rng-nexp(r;n))


By

---

Latex:
xxx(Auto
        THEN  Unfold  `qexp`  0
        THEN  (CallByValueReduce  0  THENA  Auto)
        THEN  (GenConclAtAddr  [2;1]  THENA  Auto)
        THEN  D  -2
        THEN  Reduce  0)xxx

---

Home Index