---

Step * 1 of Lemma rexp-radd

.....assertion..... 
∀z:ℝ. ((r0 ≤ z) ⇒ (∀x:ℝ. (e^x + z = (e^x * e^z))))
BY
{ (Auto
   THEN (FLemma `rexp-of-nonneg` [-2] THENA Auto)
   THEN (Assert r0 < e^z BY
               (RWO  "-1<" 0 THEN Auto))
   THEN (InstLemma `rexp-unique` [⌜λ2x.(e^x + z/e^z)⌝]⋅ THENA (Auto THEN Try ((RWO "-1" 0 THEN Auto))))) }

1
.....antecedent..... 
1. z : ℝ
2. r0 ≤ z
3. x : ℝ
4. r1 ≤ e^z
5. r0 < e^z
⊢ (e^r0 + z/e^z) = r1

2
.....antecedent..... 
1. z : ℝ
2. r0 ≤ z
3. x : ℝ
4. r1 ≤ e^z
5. r0 < e^z
⊢ d((e^x + z/e^z))/dx = λx.(e^x + z/e^z) on (-∞, ∞)

3
1. z : ℝ
2. r0 ≤ z
3. x : ℝ
4. r1 ≤ e^z
5. r0 < e^z
6. ∀x:ℝ. ((e^x + z/e^z) = e^x)
⊢ e^x + z = (e^x * e^z)

---

Latex:

---

Latex:
.....assertion..... 
\mforall{}z:\mBbbR{}.  ((r0  \mleq{}  z)  {}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  (e\^{}x  +  z  =  (e\^{}x  *  e\^{}z))))


By

---

Latex:
(Auto
  THEN  (FLemma  `rexp-of-nonneg`  [-2]  THENA  Auto)
  THEN  (Assert  r0  <  e\^{}z  BY
                          (RWO    "-1<"  0  THEN  Auto))
  THEN  (InstLemma  `rexp-unique`  [\mkleeneopen{}\mlambda{}\msubtwo{}x.(e\^{}x  +  z/e\^{}z)\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  Try  ((RWO  "-1"  0  THEN  Auto)))
              ))

---

Home Index