Step
*
2
of Lemma
rlog1
1. r1_∫
-
r1 (r1/t) dt = r0
⊢ rlog(r1) = r0
BY
{ (Fold `rlog` (-1) THEN Auto) }
Latex:
Latex:
1. r1\_\mint{}\msupminus{}r1 (r1/t) dt = r0
\mvdash{} rlog(r1) = r0
By
Latex:
(Fold `rlog` (-1) THEN Auto)
Home
Index