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 ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 + 1 ) ) )

Proof

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