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 ⊢ N ∈ ℤ → N 2 ∈ ℤ ↔ ¬ N + 1 2 ∈ ℤ

Proof

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