This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 ) ) )