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

Proof

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