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

Metamath Proof Explorer

Theorem zeo2

Description: An integer is even or odd but not both. (Contributed by Mario Carneiro, 12-Sep-2015)

Ref Expression
Assertion zeo2 ( 𝑁 ∈ ℤ → ( ( 𝑁 / 2 ) ∈ ℤ ↔ ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )

Proof

Step Hyp Ref Expression
1 zcn ⊢ ( 𝑁 ∈ ℤ → 𝑁 ∈ ℂ )
2 peano2cn ⊢ ( 𝑁 ∈ ℂ → ( 𝑁 + 1 ) ∈ ℂ )
3 1 2 syl ⊢ ( 𝑁 ∈ ℤ → ( 𝑁 + 1 ) ∈ ℂ )
4 2cnd ⊢ ( 𝑁 ∈ ℤ → 2 ∈ ℂ )
5 2ne0 ⊢ 2 ≠ 0
6 5 a1i ⊢ ( 𝑁 ∈ ℤ → 2 ≠ 0 )
7 3 4 6 divcan2d ⊢ ( 𝑁 ∈ ℤ → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) = ( 𝑁 + 1 ) )
8 1 4 6 divcan2d ⊢ ( 𝑁 ∈ ℤ → ( 2 · ( 𝑁 / 2 ) ) = 𝑁 )
9 8 oveq1d ⊢ ( 𝑁 ∈ ℤ → ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) = ( 𝑁 + 1 ) )
10 7 9 eqtr4d ⊢ ( 𝑁 ∈ ℤ → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) = ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) )
11 zneo ⊢ ( ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ∧ ( 𝑁 / 2 ) ∈ ℤ ) → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) ≠ ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) )
12 11 expcom ⊢ ( ( 𝑁 / 2 ) ∈ ℤ → ( ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ → ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) ≠ ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) ) )
13 12 necon2bd ⊢ ( ( 𝑁 / 2 ) ∈ ℤ → ( ( 2 · ( ( 𝑁 + 1 ) / 2 ) ) = ( ( 2 · ( 𝑁 / 2 ) ) + 1 ) → ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
14 10 13 syl5com ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 / 2 ) ∈ ℤ → ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
15 zeo ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 / 2 ) ∈ ℤ ∨ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
16 15 ord ⊢ ( 𝑁 ∈ ℤ → ( ¬ ( 𝑁 / 2 ) ∈ ℤ → ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )
17 16 con1d ⊢ ( 𝑁 ∈ ℤ → ( ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ → ( 𝑁 / 2 ) ∈ ℤ ) )
18 14 17 impbid ⊢ ( 𝑁 ∈ ℤ → ( ( 𝑁 / 2 ) ∈ ℤ ↔ ¬ ( ( 𝑁 + 1 ) / 2 ) ∈ ℤ ) )