---

Step * of Lemma realexp_functionality

∀[x1:{x:ℝ| r0 < x} ]. ∀[x2,y1,y2:ℝ].  (realexp(x1;y1) = realexp(x2;y2)) supposing ((y1 = y2) and (x1 = x2))
BY
{ ((Auto THEN Unfold `realexp` 0) THEN (RWO  "expr-req" 0 THENA Auto)) }

1
1. x1 : {x:ℝ| r0 < x} 
2. x2 : ℝ
3. y1 : ℝ
4. y2 : ℝ
5. x1 = x2
6. y1 = y2
⊢ e^y1 * ln(x1) = e^y2 * ln(x2)

---

Latex:

---

Latex:
\mforall{}[x1:\{x:\mBbbR{}|  r0  <  x\}  ].  \mforall{}[x2,y1,y2:\mBbbR{}].
    (realexp(x1;y1)  =  realexp(x2;y2))  supposing  ((y1  =  y2)  and  (x1  =  x2))


By

---

Latex:
((Auto  THEN  Unfold  `realexp`  0)  THEN  (RWO    "expr-req"  0  THENA  Auto))

---

Home Index