Metamath Proof Explorer

Theorem oddp1even

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

Ref Expression
Assertion oddp1even ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ 2 ∥ N + 1

Proof

Step Hyp Ref Expression
1 oddm1even ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ 2 ∥ N − 1
2 2z ⊢ 2 ∈ ℤ
3 peano2zm ⊢ N ∈ ℤ → N − 1 ∈ ℤ
4 dvdsadd ⊢ 2 ∈ ℤ ∧ N − 1 ∈ ℤ → 2 ∥ N − 1 ↔ 2 ∥ 2 + N - 1
5 2 3 4 sylancr ⊢ N ∈ ℤ → 2 ∥ N − 1 ↔ 2 ∥ 2 + N - 1
6 2cnd ⊢ N ∈ ℤ → 2 ∈ ℂ
7 zcn ⊢ N ∈ ℤ → N ∈ ℂ
8 1cnd ⊢ N ∈ ℤ → 1 ∈ ℂ
9 6 7 8 addsub12d ⊢ N ∈ ℤ → 2 + N - 1 = N + 2 - 1
10 2m1e1 ⊢ 2 − 1 = 1
11 10 oveq2i ⊢ N + 2 - 1 = N + 1
12 9 11 eqtrdi ⊢ N ∈ ℤ → 2 + N - 1 = N + 1
13 12 breq2d ⊢ N ∈ ℤ → 2 ∥ 2 + N - 1 ↔ 2 ∥ N + 1
14 1 5 13 3bitrd ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ 2 ∥ N + 1