---

Step * of Lemma rnexp-rexp

∀[x:ℝ]. ∀[N:ℕ].  (e^x^N = e^r(N) * x)
BY
{ InductionOnNat }

1
.....basecase..... 
1. x : ℝ
2. N : ℤ
⊢ e^x^0 = e^r0 * x

2
.....upcase..... 
1. x : ℝ
2. N : ℤ
3. 0 < N
4. e^x^N - 1 = e^r(N - 1) * x
⊢ e^x^N = e^r(N) * x

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  \mforall{}[N:\mBbbN{}].    (e\^{}x\^{}N  =  e\^{}r(N)  *  x)


By

---

Latex:
InductionOnNat

---

Home Index