Step
*
of Lemma
even-implies
∀n:ℤ. ((↑isEven(n))
⇒ {((↑isOdd(n - 1)) ∧ (¬↑isOdd(n))) ∧ (↑isOdd(n + 1))})
BY
{ (Auto THEN D 0 THEN Auto) }
1
1. n : ℤ@i
2. ↑isEven(n)@i
⊢ ↑isOdd(n - 1)
2
1. n : ℤ@i
2. ↑isEven(n)@i
3. ↑isOdd(n - 1)
⊢ ¬↑isOdd(n)
3
1. n : ℤ@i
2. ↑isEven(n)@i
⊢ ↑isOdd(n + 1)
Latex:
Latex:
\mforall{}n:\mBbbZ{}. ((\muparrow{}isEven(n)) {}\mRightarrow{} \{((\muparrow{}isOdd(n - 1)) \mwedge{} (\mneg{}\muparrow{}isOdd(n))) \mwedge{} (\muparrow{}isOdd(n + 1))\})
By
Latex:
(Auto THEN D 0 THEN Auto)
Home
Index