---

Step * of Lemma rlog_wf

∀[x:{x:ℝ| r0 < x} ]. (rlog(x) ∈ ℝ)
BY
{ ((D 0 THENA 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. r0 < rmin(r1;x)
3. ∀t:ℝ. ((t ∈ [rmin(r1;x), rmax(r1;x)]) ⇒ t ≠ r0)
⊢ rlog(x) ∈ ℝ

---

Latex:

---

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


By

---

Latex:
((D  0  THENA  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