Step * of Lemma odd-plus-odd

No Annotations
[n,m:ℤ].  ↑isEven(n m) supposing (↑isOdd(n)) ∧ (↑isOdd(m))
BY
((RWO "isEven-add" 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