---

Step * of Lemma same-parity-implies-even-odd

∀n,m:ℤ.  ((↑same-parity(n;m)) ⇒ (((↑isEven(n)) ∧ (↑isEven(m))) ∨ ((↑isOdd(n)) ∧ (↑isOdd(m)))))
BY
{ (Auto
   THEN RepUR ``same-parity`` (-1)
   THEN BoolCase ⌜isEven(n)⌝⋅
   THEN Auto
   THEN Try (Complete ((OrLeft THEN Auto)))
   THEN (RWO "odd-iff-not-even<" (-3) THEN Auto)⋅) }

---

Latex:

---

Latex:
\mforall{}n,m:\mBbbZ{}.    ((\muparrow{}same-parity(n;m))  {}\mRightarrow{}  (((\muparrow{}isEven(n))  \mwedge{}  (\muparrow{}isEven(m)))  \mvee{}  ((\muparrow{}isOdd(n))  \mwedge{}  (\muparrow{}isOdd(m)))))


By

---

Latex:
(Auto
  THEN  RepUR  ``same-parity``  (-1)
  THEN  BoolCase  \mkleeneopen{}isEven(n)\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  Try  (Complete  ((OrLeft  THEN  Auto)))
  THEN  (RWO  "odd-iff-not-even<"  (-3)  THEN  Auto)\mcdot{})

---

Home Index