Metamath Proof Explorer

Theorem oddm1even

Description: An integer is odd iff its predecessor is even. (Contributed by Mario Carneiro, 5-Sep-2016)

Ref Expression
Assertion oddm1even ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ 2 ∥ N − 1

Proof

Step Hyp Ref Expression
1 simpl ⊢ N ∈ ℤ ∧ n ∈ ℤ → N ∈ ℤ
2 1 zcnd ⊢ N ∈ ℤ ∧ n ∈ ℤ → N ∈ ℂ
3 1cnd ⊢ N ∈ ℤ ∧ n ∈ ℤ → 1 ∈ ℂ
4 2cnd ⊢ N ∈ ℤ ∧ n ∈ ℤ → 2 ∈ ℂ
5 simpr ⊢ N ∈ ℤ ∧ n ∈ ℤ → n ∈ ℤ
6 5 zcnd ⊢ N ∈ ℤ ∧ n ∈ ℤ → n ∈ ℂ
7 4 6 mulcld ⊢ N ∈ ℤ ∧ n ∈ ℤ → 2 ⁢ n ∈ ℂ
8 2 3 7 subadd2d ⊢ N ∈ ℤ ∧ n ∈ ℤ → N − 1 = 2 ⁢ n ↔ 2 ⁢ n + 1 = N
9 eqcom ⊢ N − 1 = 2 ⁢ n ↔ 2 ⁢ n = N − 1
10 4 6 mulcomd ⊢ N ∈ ℤ ∧ n ∈ ℤ → 2 ⁢ n = n ⋅ 2
11 10 eqeq1d ⊢ N ∈ ℤ ∧ n ∈ ℤ → 2 ⁢ n = N − 1 ↔ n ⋅ 2 = N − 1
12 9 11 bitrid ⊢ N ∈ ℤ ∧ n ∈ ℤ → N − 1 = 2 ⁢ n ↔ n ⋅ 2 = N − 1
13 8 12 bitr3d ⊢ N ∈ ℤ ∧ n ∈ ℤ → 2 ⁢ n + 1 = N ↔ n ⋅ 2 = N − 1
14 13 rexbidva ⊢ N ∈ ℤ → ∃ n ∈ ℤ 2 ⁢ n + 1 = N ↔ ∃ n ∈ ℤ n ⋅ 2 = N − 1
15 odd2np1 ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ ∃ n ∈ ℤ 2 ⁢ n + 1 = N
16 2z ⊢ 2 ∈ ℤ
17 peano2zm ⊢ N ∈ ℤ → N − 1 ∈ ℤ
18 divides ⊢ 2 ∈ ℤ ∧ N − 1 ∈ ℤ → 2 ∥ N − 1 ↔ ∃ n ∈ ℤ n ⋅ 2 = N − 1
19 16 17 18 sylancr ⊢ N ∈ ℤ → 2 ∥ N − 1 ↔ ∃ n ∈ ℤ n ⋅ 2 = N − 1
20 14 15 19 3bitr4d ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ 2 ∥ N − 1