---

Step * of Lemma realexp-nat

∀[x:{x:ℝ| r0 < x} ]. ∀[n:ℕ].  (realexp(x;r(n)) = x^n)
BY
{ (InductionOnNat THEN (RWO "rnexp-req" 0 THENA Auto) THEN AutoSplit) }

1
1. x : {x:ℝ| r0 < x} 
2. n : ℤ
3. 0 = 0 ∈ ℤ
⊢ realexp(x;r0) = r1

2
1. x : {x:ℝ| r0 < x} 
2. n : ℤ
3. n ≠ 0
4. 0 < n
5. realexp(x;r(n - 1)) = x^n - 1
⊢ realexp(x;r(n)) = (x * x^n - 1)

---

Latex:

---

Latex:
\mforall{}[x:\{x:\mBbbR{}|  r0  <  x\}  ].  \mforall{}[n:\mBbbN{}].    (realexp(x;r(n))  =  x\^{}n)


By

---

Latex:
(InductionOnNat  THEN  (RWO  "rnexp-req"  0  THENA  Auto)  THEN  AutoSplit)

---

Home Index