---

Step * of Lemma rlog-inv

∀y:{t:ℝ| r0 < t} . (rlog((r1/y)) = -(rlog(y)))
BY
{ (Auto THEN (RWW "rlog-rdiv rlog1" 0 THENM nRNorm 0) THEN Auto) }

1
1. y : {t:ℝ| r0 < t} 
⊢ (r1/y) ∈ {x:ℝ| r0 < x} 

---

Latex:

---

Latex:
\mforall{}y:\{t:\mBbbR{}|  r0  <  t\}  .  (rlog((r1/y))  =  -(rlog(y)))


By

---

Latex:
(Auto  THEN  (RWW  "rlog-rdiv  rlog1"  0  THENM  nRNorm  0)  THEN  Auto)

---

Home Index