---

Step * of Lemma rlog-rmul

∀x,y:{t:ℝ| r0 < t} .  (rlog(x * y) = (rlog(x) + rlog(y)))
BY
{ (Intros
   THEN DSetVars
   THEN (Assert ⌜r0 < (x * y)⌝⋅ THENA (Unhide THEN EAuto 1))
   THEN Unhide
   THEN Auto
   THEN (Assert λx.(rlog(x * y) - rlog(y)) ∈ (r0, ∞) ⟶ℝ BY
               (Unfold `rfun` 0
                THEN (MemCD THENA Auto)
                THEN DSetVars
                THEN All Reduce
                THEN Auto
                THEN MemTypeCD
                THEN EAuto 1))) }

1
1. x : ℝ
2. r0 < x
3. y : ℝ
4. r0 < y
5. r0 < (x * y)
6. λx.(rlog(x * y) - rlog(y)) ∈ (r0, ∞) ⟶ℝ
⊢ rlog(x * y) = (rlog(x) + rlog(y))

---

Latex:

---

Latex:
\mforall{}x,y:\{t:\mBbbR{}|  r0  <  t\}  .    (rlog(x  *  y)  =  (rlog(x)  +  rlog(y)))


By

---

Latex:
(Intros
  THEN  DSetVars
  THEN  (Assert  \mkleeneopen{}r0  <  (x  *  y)\mkleeneclose{}\mcdot{}  THENA  (Unhide  THEN  EAuto  1))
  THEN  Unhide
  THEN  Auto
  THEN  (Assert  \mlambda{}x.(rlog(x  *  y)  -  rlog(y))  \mmember{}  (r0,  \minfty{})  {}\mrightarrow{}\mBbbR{}  BY
                          (Unfold  `rfun`  0
                            THEN  (MemCD  THENA  Auto)
                            THEN  DSetVars
                            THEN  All  Reduce
                            THEN  Auto
                            THEN  MemTypeCD
                            THEN  EAuto  1)))

---

Home Index