Step
*
of Lemma
same-parity-implies
∀[n,m:ℤ]. ((↑same-parity(n;m))
⇒ {(¬↑same-parity(n;m - 1)) ∧ (¬↑same-parity(n;m + 1))})
BY
{ (Auto THEN D 0 THEN Auto THEN All (RepUR ``same-parity``) THEN OldAutoSplit THEN SplitOnHypITE (-2) THEN Auto) }
1
.....truecase.....
1. n : ℤ
2. m : ℤ
3. ↑isEven(m)
4. ↑isEven(n)
5. ↑isEven(n)
⊢ ¬↑isEven(m - 1)
2
.....falsecase.....
1. n : ℤ
2. m : ℤ
3. ↑isOdd(m)
4. ¬↑isEven(n)
5. ¬↑isEven(n)
⊢ ¬↑isOdd(m - 1)
3
.....truecase.....
1. n : ℤ
2. m : ℤ
3. ↑isEven(m)
4. ↑isEven(n)
5. ↑isEven(n)
⊢ ¬↑isEven(m + 1)
4
.....falsecase.....
1. n : ℤ
2. m : ℤ
3. ↑isOdd(m)
4. ¬↑isEven(n)
5. ¬↑isEven(n)
⊢ ¬↑isOdd(m + 1)
Latex:
Latex:
\mforall{}[n,m:\mBbbZ{}]. ((\muparrow{}same-parity(n;m)) {}\mRightarrow{} \{(\mneg{}\muparrow{}same-parity(n;m - 1)) \mwedge{} (\mneg{}\muparrow{}same-parity(n;m + 1))\})
By
Latex:
(Auto
THEN D 0
THEN Auto
THEN All (RepUR ``same-parity``)
THEN OldAutoSplit
THEN SplitOnHypITE (-2)
THEN Auto)
Home
Index