---

Step * 1 3 1 of Lemma rexp-radd


1. z : ℝ
2. r0 ≤ z
3. x : ℝ
4. r1 ≤ e^z
5. r0 < e^z
6. ∀x:ℝ. ((e^x + z/e^z) = e^x)
7. (e^x + z/e^z) = e^x
8. ((e^x + z/e^z) * e^z) = (e^x * e^z)
⊢ e^x + z = (e^x * e^z)
BY
{ ((RWO "-1<" 0 THENA Auto) THEN MoveToConcl 5 THEN GenConclTerms Auto [⌜e^x + z⌝;⌜e^z⌝]⋅ THEN All Thin) }

1
1. v : ℝ
2. v1 : ℝ
⊢ (r0 < v1) ⇒ (v = ((v/v1) * v1))

---

Latex:

---

Latex:

1.  z  :  \mBbbR{}
2.  r0  \mleq{}  z
3.  x  :  \mBbbR{}
4.  r1  \mleq{}  e\^{}z
5.  r0  <  e\^{}z
6.  \mforall{}x:\mBbbR{}.  ((e\^{}x  +  z/e\^{}z)  =  e\^{}x)
7.  (e\^{}x  +  z/e\^{}z)  =  e\^{}x
8.  ((e\^{}x  +  z/e\^{}z)  *  e\^{}z)  =  (e\^{}x  *  e\^{}z)
\mvdash{}  e\^{}x  +  z  =  (e\^{}x  *  e\^{}z)


By

---

Latex:
((RWO  "-1<"  0  THENA  Auto)
  THEN  MoveToConcl  5
  THEN  GenConclTerms  Auto  [\mkleeneopen{}e\^{}x  +  z\mkleeneclose{};\mkleeneopen{}e\^{}z\mkleeneclose{}]\mcdot{}
  THEN  All  Thin)

---

Home Index