---

Step * of Lemma qexp-one

∀[n:ℕ]. (1 ↑ n = 1 ∈ ℚ)
BY
{ InductionOnNat }

1
.....basecase..... 
1. n : ℤ
⊢ 1 ↑ 0 = 1 ∈ ℚ

2
.....upcase..... 
1. n : ℤ
2. 0 < n
3. 1 ↑ n - 1 = 1 ∈ ℚ
⊢ 1 ↑ n = 1 ∈ ℚ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  (1  \muparrow{}  n  =  1)


By

---

Latex:
InductionOnNat

---

Home Index