---

Step * of Lemma rem-zero-implies-minus

∀x:ℤ. ∀y:ℤ-o.  (((x rem y) = 0 ∈ ℤ) ⇒ ((-x rem y) = 0 ∈ ℤ))
BY
{ (Auto
   THEN InstLemma `div_rem_sum` [⌜x⌝;⌜y⌝]⋅
   THEN Auto
   THEN Subst' x = ((x ÷ y) * y) ∈ ℤ 0
   THEN Auto'
   THEN (GenConcl ⌜(x ÷ y) = z ∈ ℤ⌝⋅ THENA Auto)
   THEN All Thin
   THEN BLemma `divides_iff_rem_zero`
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}x:\mBbbZ{}.  \mforall{}y:\mBbbZ{}\msupminus{}\msupzero{}.    (((x  rem  y)  =  0)  {}\mRightarrow{}  ((-x  rem  y)  =  0))


By

---

Latex:
(Auto
  THEN  InstLemma  `div\_rem\_sum`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  Subst'  x  =  ((x  \mdiv{}  y)  *  y)  0
  THEN  Auto'
  THEN  (GenConcl  \mkleeneopen{}(x  \mdiv{}  y)  =  z\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  All  Thin
  THEN  BLemma  `divides\_iff\_rem\_zero`
  THEN  Auto)

---

Home Index