---

Step * of Lemma rlog_functionality

∀[x:{x:ℝ| r0 < x} ]. ∀[y:ℝ].  rlog(x) = rlog(y) supposing x = y
BY
{ (Auto
   THEN (Assert r0 < rmin(r1;x) BY
               EAuto 1)
   THEN (Assert ∀t:ℝ. ((t ∈ [rmin(r1;x), rmax(r1;x)]) ⇒ t ≠ r0) BY
               (Reduce 0 THEN Auto))) }

1
1. x : {x:ℝ| r0 < x} 
2. y : ℝ
3. x = y
4. r0 < rmin(r1;x)
5. ∀t:ℝ. ((t ∈ [rmin(r1;x), rmax(r1;x)]) ⇒ t ≠ r0)
⊢ rlog(x) = rlog(y)

---

Latex:

---

Latex:
\mforall{}[x:\{x:\mBbbR{}|  r0  <  x\}  ].  \mforall{}[y:\mBbbR{}].    rlog(x)  =  rlog(y)  supposing  x  =  y


By

---

Latex:
(Auto
  THEN  (Assert  r0  <  rmin(r1;x)  BY
                          EAuto  1)
  THEN  (Assert  \mforall{}t:\mBbbR{}.  ((t  \mmember{}  [rmin(r1;x),  rmax(r1;x)])  {}\mRightarrow{}  t  \mneq{}  r0)  BY
                          (Reduce  0  THEN  Auto)))

---

Home Index