---

Step * of Lemma mod2-is-zero

∀x:ℤ. ((x mod 2) = 0 ∈ ℤ ⇐⇒ ∃n:ℤ. (x = (2 * n) ∈ ℤ))
BY
{ ((D 0 THENA Auto)
   THEN Unfold `modulus` 0
   THEN (CallByValueReduce 0 THENA Auto)
   THEN (InstLemma `div_rem_sum` [⌜x⌝;⌜2⌝]⋅ THENA Auto)
   THEN (InstLemma `rem_bounds_absval` [⌜2⌝;⌜x⌝]⋅ THENA Auto)
   THEN (RWO "absval_strict_ubound" (-1) THENA Auto)
   THEN (Subst' |2| ~ 2 -1 THENA Auto)
   THEN (RW (AddrC [2;2;2] (HypC 2)) 0 THENA Auto)
   THEN (GenConcl ⌜(x rem 2) = r ∈ {-1..2-}⌝⋅ THENA Auto)
   THEN Thin (-1)
   THEN IntSegCases (-1)
   THEN Reduce 0
   THEN Auto
   THEN Try ((D 0 With ⌜x ÷ 2⌝  THEN Auto))
   THEN ExRepD) }

1
1. x : ℤ
2. x = (((x ÷ 2) * 2) + (x rem 2)) ∈ ℤ
3. -2 < x rem 2
4. x rem 2 < 2
5. r : ℤ
6. r = (-1) ∈ ℤ
7. n : ℤ
8. (((x ÷ 2) * 2) + (-1)) = (2 * n) ∈ ℤ
⊢ 1 = 0 ∈ ℤ

2
1. x : ℤ
2. x = (((x ÷ 2) * 2) + (x rem 2)) ∈ ℤ
3. -2 < x rem 2
4. x rem 2 < 2
5. r : ℤ
6. r = 1 ∈ ℤ
7. n : ℤ
8. (((x ÷ 2) * 2) + 1) = (2 * n) ∈ ℤ
⊢ 1 = 0 ∈ ℤ

---

Latex:

---

Latex:
\mforall{}x:\mBbbZ{}.  ((x  mod  2)  =  0  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbZ{}.  (x  =  (2  *  n)))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  Unfold  `modulus`  0
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  (InstLemma  `div\_rem\_sum`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (InstLemma  `rem\_bounds\_absval`  [\mkleeneopen{}2\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  (RWO  "absval\_strict\_ubound"  (-1)  THENA  Auto)
  THEN  (Subst'  |2|  \msim{}  2  -1  THENA  Auto)
  THEN  (RW  (AddrC  [2;2;2]  (HypC  2))  0  THENA  Auto)
  THEN  (GenConcl  \mkleeneopen{}(x  rem  2)  =  r\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Thin  (-1)
  THEN  IntSegCases  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((D  0  With  \mkleeneopen{}x  \mdiv{}  2\mkleeneclose{}    THEN  Auto))
  THEN  ExRepD)

---

Home Index