Step
*
of Lemma
int_nzero-rational
∀[z:ℤ-o]. (¬(z = 0 ∈ ℚ))
BY
{ (Auto THEN RWO "int-equal-in-rationals" 0 THEN Auto) }
Latex:
Latex:
\mforall{}[z:\mBbbZ{}\msupminus{}\msupzero{}].  (\mneg{}(z  =  0))
By
Latex:
(Auto  THEN  RWO  "int-equal-in-rationals"  0  THEN  Auto)
Home
Index