---

Step * of Lemma odd-plus-odd

No Annotations
∀[n,m:ℤ].  ↑isEven(n + m) supposing (↑isOdd(n)) ∧ (↑isOdd(m))
BY
{ ((RWO "isEven-add" 0 THEN Auto)
   THEN Unfold `same-parity` 0
   THEN AutoSplit
   THEN EAuto 1
   THEN RWO "even-iff-not-odd" (-1)
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[n,m:\mBbbZ{}].    \muparrow{}isEven(n  +  m)  supposing  (\muparrow{}isOdd(n))  \mwedge{}  (\muparrow{}isOdd(m))


By

---

Latex:
((RWO  "isEven-add"  0  THEN  Auto)
  THEN  Unfold  `same-parity`  0
  THEN  AutoSplit
  THEN  EAuto  1
  THEN  RWO  "even-iff-not-odd"  (-1)
  THEN  Auto)

---

Home Index