---

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

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

1
1. n : ℤ
2. m : ℤ
3. ¬↑if isEven(n) then isEven(m) else isOdd(m) fi 
4. ↑isEven(n)
⊢ (True ∧ (↑isOdd(m))) ∨ ((↑isOdd(n)) ∧ (↑isEven(m)))

---

Latex:

---

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


By

---

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

---

Home Index