Step
*
1
1
1
of Lemma
mod2-add1
1. n : ℤ
2. (n + 1) = ((((n + 1) ÷↓ 2) * 2) + ((n + 1) mod 2)) ∈ ℤ
3. n = (((n ÷↓ 2) * 2) + (n mod 2)) ∈ ℤ
⊢ ∃k:ℤ. (((n + 1) mod 2) = ((2 * k) + (n mod 2) + 1) ∈ ℤ)
BY
{ (D 0 With ⌜(n ÷↓ 2) - (n + 1) ÷↓ 2⌝ THEN Auto) }
1
1. n : ℤ
2. (n + 1) = ((((n + 1) ÷↓ 2) * 2) + ((n + 1) mod 2)) ∈ ℤ
3. n = (((n ÷↓ 2) * 2) + (n mod 2)) ∈ ℤ
⊢ ((n + 1) mod 2) = ((2 * ((n ÷↓ 2) - (n + 1) ÷↓ 2)) + (n mod 2) + 1) ∈ ℤ
Latex:
Latex:
1. n : \mBbbZ{}
2. (n + 1) = ((((n + 1) \mdiv{}\mdownarrow{} 2) * 2) + ((n + 1) mod 2))
3. n = (((n \mdiv{}\mdownarrow{} 2) * 2) + (n mod 2))
\mvdash{} \mexists{}k:\mBbbZ{}. (((n + 1) mod 2) = ((2 * k) + (n mod 2) + 1))
By
Latex:
(D 0 With \mkleeneopen{}(n \mdiv{}\mdownarrow{} 2) - (n + 1) \mdiv{}\mdownarrow{} 2\mkleeneclose{} THEN Auto)
Home
Index