---

Step * of Lemma even-succ-implies-not-even

∀n:ℤ. ((↑isEven(n + 1)) ⇒ (¬↑isEven(n)))
BY
{ (Unfold `isEven` 0
   THEN (UnivCD THENA Auto)
   THEN All (RW assert_pushdownC)
   THEN Auto
   THEN RWO "add-one-mod-2" (-1)
   THEN Auto
   THEN (InstLemma `mod_bounds` [⌜n⌝;⌜2⌝]⋅ THEN Auto')⋅) }

---

Latex:

---

Latex:
\mforall{}n:\mBbbZ{}.  ((\muparrow{}isEven(n  +  1))  {}\mRightarrow{}  (\mneg{}\muparrow{}isEven(n)))


By

---

Latex:
(Unfold  `isEven`  0
  THEN  (UnivCD  THENA  Auto)
  THEN  All  (RW  assert\_pushdownC)
  THEN  Auto
  THEN  RWO  "add-one-mod-2"  (-1)
  THEN  Auto
  THEN  (InstLemma  `mod\_bounds`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}2\mkleeneclose{}]\mcdot{}  THEN  Auto')\mcdot{})

---

Home Index