---

Step * of Lemma mod2-add2

∀n:ℤ. (((n + 2) mod 2) = (n mod 2) ∈ ℤ)
BY
{ ((Auto THEN (Subst' n + 2 ~ (n + 1) + 1 0 THENA Auto))
   THEN (RWW "mod2-add1" 0 THENA Auto)
   THEN (InstLemma `mod2-cases` [⌜n⌝]⋅ THENA Auto)
   THEN D -1
   THEN HypSubst' (-1) 0
   THEN Computation) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbZ{}.  (((n  +  2)  mod  2)  =  (n  mod  2))


By

---

Latex:
((Auto  THEN  (Subst'  n  +  2  \msim{}  (n  +  1)  +  1  0  THENA  Auto))
  THEN  (RWW  "mod2-add1"  0  THENA  Auto)
  THEN  (InstLemma  `mod2-cases`  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  D  -1
  THEN  HypSubst'  (-1)  0
  THEN  Computation)

---

Home Index