---

Step * of Lemma logseq_wf

∀[a:{a:ℝ| r0 < a} ]. ∀[b:ℝ]. ∀[n:ℕ].  (logseq(a;b;n) ∈ ℝ)
BY
{ (ProveWfLemma THEN RepeatFor 2 ((RWW "exp-fastexp<" 0 THEN Auto))) }

---

Latex:

---

Latex:
\mforall{}[a:\{a:\mBbbR{}|  r0  <  a\}  ].  \mforall{}[b:\mBbbR{}].  \mforall{}[n:\mBbbN{}].    (logseq(a;b;n)  \mmember{}  \mBbbR{})


By

---

Latex:
(ProveWfLemma  THEN  RepeatFor  2  ((RWW  "exp-fastexp<"  0  THEN  Auto)))

---

Home Index