---

Step * of Lemma qexp_wf

∀[r:ℚ]. ∀[n:ℕ].  (r ↑ n ∈ ℚ)
BY
{ (Unfold `qexp` 0 THEN Auto) }

1
1. r : ℚ
2. n : ℕ
3. a : ℤ
4. b : ℕ+
5. qrep(r) = <a, b> ∈ (ℤ × ℕ+)
⊢ b^n ∈ ℤ-o

---

Latex:

---

Latex:
\mforall{}[r:\mBbbQ{}].  \mforall{}[n:\mBbbN{}].    (r  \muparrow{}  n  \mmember{}  \mBbbQ{})


By

---

Latex:
(Unfold  `qexp`  0  THEN  Auto)

---

Home Index