Step
*
of Lemma
rat-to-real-req
∀[a:ℤ]. ∀[b:ℤ-o]. (r(a/b) = (r(a)/r(b)))
BY
{ (Intros THEN Unfold `rat-to-real` 0 THEN BLemma `int-rdiv-req` THEN Auto) }
Latex:
Latex:
\mforall{}[a:\mBbbZ{}]. \mforall{}[b:\mBbbZ{}\msupminus{}\msupzero{}]. (r(a/b) = (r(a)/r(b)))
By
Latex:
(Intros THEN Unfold `rat-to-real` 0 THEN BLemma `int-rdiv-req` THEN Auto)
Home
Index