---

Step * 2 2 of Lemma rexp-radd


1. ∀z:ℝ. ((r0 ≤ z) ⇒ (∀x:ℝ. (e^x + z = (e^x * e^z))))
2. x : ℝ
3. y : ℝ
4. ∃z:ℝ. ((r0 ≤ z) ∧ (r0 ≤ (z + y)))
⊢ e^x + y = (e^x * e^y)
BY
{ (ExRepD
   THEN ((FLemma `rexp-of-nonneg` [-2] THENA Auto) THEN (Assert r0 < e^z BY (RWO  "-1<" 0 THEN Auto)))
   THEN (nRMul ⌜e^z⌝ 0⋅ THENA Auto)) }

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

---

Latex:

---

Latex:

1.  \mforall{}z:\mBbbR{}.  ((r0  \mleq{}  z)  {}\mRightarrow{}  (\mforall{}x:\mBbbR{}.  (e\^{}x  +  z  =  (e\^{}x  *  e\^{}z))))
2.  x  :  \mBbbR{}
3.  y  :  \mBbbR{}
4.  \mexists{}z:\mBbbR{}.  ((r0  \mleq{}  z)  \mwedge{}  (r0  \mleq{}  (z  +  y)))
\mvdash{}  e\^{}x  +  y  =  (e\^{}x  *  e\^{}y)


By

---

Latex:
(ExRepD
  THEN  ((FLemma  `rexp-of-nonneg`  [-2]  THENA  Auto)  THEN  (Assert  r0  <  e\^{}z  BY  (RWO    "-1<"  0  THEN  Auto)))
  THEN  (nRMul  \mkleeneopen{}e\^{}z\mkleeneclose{}  0\mcdot{}  THENA  Auto))

---

Home Index