---

Step * of Lemma qexp-exp

∀[n:ℕ]. ∀[x:ℤ].  (x ↑ n = x^n ∈ ℚ)
BY
{ xxx(InductionOnNat THEN Auto THEN RWW "qexp-zero" 0 THEN Try (Complete (Auto)))xxx }

1
.....wf..... 
1. n : ℤ
2. x : ℤ
⊢ x^0 = x^0 ∈ ℚ

2
1. n : ℤ
2. 0 < n
3. ∀[x:ℤ]. (x ↑ n - 1 = x^(n - 1) ∈ ℚ)
4. x : ℤ
⊢ x ↑ n = x^n ∈ ℚ

---

Latex:

---

Latex:
\mforall{}[n:\mBbbN{}].  \mforall{}[x:\mBbbZ{}].    (x  \muparrow{}  n  =  x\^{}n)


By

---

Latex:
xxx(InductionOnNat  THEN  Auto  THEN  RWW  "qexp-zero"  0  THEN  Try  (Complete  (Auto)))xxx

---

Home Index