---

Step * 2 of Lemma rnexp-rexp

.....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
BY
{ ((Subst' N ~ (N - 1) + 1 0 THENA Auto)
   THEN (RWO "rnexp-add1" 0 THENA Auto)
   THEN (RWO "-1" 0 THENA Auto)
   THEN (RWO "rexp-radd<" 0 THENA Auto)
   THEN BLemma `rexp_functionality`
   THEN Auto
   THEN nRNorm 0
   THEN Auto) }

---

Latex:

---

Latex:
.....upcase..... 
1.  x  :  \mBbbR{}
2.  N  :  \mBbbZ{}
3.  0  <  N
4.  e\^{}x\^{}N  -  1  =  e\^{}r(N  -  1)  *  x
\mvdash{}  e\^{}x\^{}N  =  e\^{}r(N)  *  x


By

---

Latex:
((Subst'  N  \msim{}  (N  -  1)  +  1  0  THENA  Auto)
  THEN  (RWO  "rnexp-add1"  0  THENA  Auto)
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (RWO  "rexp-radd<"  0  THENA  Auto)
  THEN  BLemma  `rexp\_functionality`
  THEN  Auto
  THEN  nRNorm  0
  THEN  Auto)

---

Home Index