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

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 bitrid ⊢ ( ( 𝑁 ∈ ℤ ∧ 𝑛 ∈ ℤ ) → ( ( 𝑁 − 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 ) ) )