Step
*
1
1
of Lemma
not-same-parity-implies-even-odd
1. n : ℤ
2. m : ℤ
3. ¬↑isEven(m)
4. ↑isEven(n)
5. ↑isEven(n)
6. True
⊢ ↑isOdd(m)
BY
{ (RWO "odd-iff-not-even<" (-4) THEN Auto)⋅ }
Latex:
Latex:
1. n : \mBbbZ{}
2. m : \mBbbZ{}
3. \mneg{}\muparrow{}isEven(m)
4. \muparrow{}isEven(n)
5. \muparrow{}isEven(n)
6. True
\mvdash{} \muparrow{}isOdd(m)
By
Latex:
(RWO "odd-iff-not-even<" (-4) THEN Auto)\mcdot{}
Home
Index