Step
*
2
1
of Lemma
rinv1
1. (r1 * rinv(r1)) = r1
⊢ rnonzero(r1)
BY
{ (D 0 With ⌜3⌝ THEN Auto) }
Latex:
Latex:
1. (r1 * rinv(r1)) = r1
\mvdash{} rnonzero(r1)
By
Latex:
(D 0 With \mkleeneopen{}3\mkleeneclose{} THEN Auto)
Home
Index