---

Step * of Lemma rlog1

rlog(r1) = r0
BY
{ (InstLemma `integral-same-endpoints` [⌜(r0, ∞)⌝;⌜λ2t.(r1/t)⌝;⌜r1⌝]⋅ THENA Auto) }

1
λt.(r1/t) ∈ {f:(r0, ∞) ⟶ℝ| ∀x,y:{a:ℝ| r0 < a} .  ((x = y) ⇒ ((f x) = (f y)))} 

2
1. r1_∫-r1 (r1/t) dt = r0
⊢ rlog(r1) = r0

---

Latex:

---

Latex:
rlog(r1)  =  r0


By

---

Latex:
(InstLemma  `integral-same-endpoints`  [\mkleeneopen{}(r0,  \minfty{})\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}t.(r1/t)\mkleeneclose{};\mkleeneopen{}r1\mkleeneclose{}]\mcdot{}  THENA  Auto)

---

Home Index