---

Step * of Lemma rnexp-mul

No Annotations
∀[n,m:ℕ]. ∀[x:ℝ].  (x^m^n = x^m * n)
BY
{ (InductionOnNat THEN Reduce 0) }

1
1. n : ℤ
⊢ ∀[m:ℕ]. ∀[x:ℝ].  (r1 = x^m * 0)

2
.....upcase..... 
1. n : ℤ
2. 0 < n
3. ∀[m:ℕ]. ∀[x:ℝ].  (x^m^n - 1 = x^m * (n - 1))
⊢ ∀[m:ℕ]. ∀[x:ℝ].  (x^m^n = x^m * n)

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n,m:\mBbbN{}].  \mforall{}[x:\mBbbR{}].    (x\^{}m\^{}n  =  x\^{}m  *  n)


By

---

Latex:
(InductionOnNat  THEN  Reduce  0)

---

Home Index