Metamath Proof Explorer

Theorem zneo

Description: No even integer equals an odd integer (i.e. no integer can be both even and odd). Exercise 10(a) of Apostol p. 28. (Contributed by NM, 31-Jul-2004) (Proof shortened by Mario Carneiro, 18-May-2014)

Ref Expression
Assertion zneo ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ⁢ A ≠ 2 ⁢ B + 1

Proof

Step Hyp Ref Expression
1 halfnz ⊢ ¬ 1 2 ∈ ℤ
2 2cn ⊢ 2 ∈ ℂ
3 zcn ⊢ A ∈ ℤ → A ∈ ℂ
4 3 adantr ⊢ A ∈ ℤ ∧ B ∈ ℤ → A ∈ ℂ
5 mulcl ⊢ 2 ∈ ℂ ∧ A ∈ ℂ → 2 ⁢ A ∈ ℂ
6 2 4 5 sylancr ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ⁢ A ∈ ℂ
7 zcn ⊢ B ∈ ℤ → B ∈ ℂ
8 7 adantl ⊢ A ∈ ℤ ∧ B ∈ ℤ → B ∈ ℂ
9 mulcl ⊢ 2 ∈ ℂ ∧ B ∈ ℂ → 2 ⁢ B ∈ ℂ
10 2 8 9 sylancr ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ⁢ B ∈ ℂ
11 1cnd ⊢ A ∈ ℤ ∧ B ∈ ℤ → 1 ∈ ℂ
12 6 10 11 subaddd ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ⁢ A − 2 ⁢ B = 1 ↔ 2 ⁢ B + 1 = 2 ⁢ A
13 2 a1i ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ∈ ℂ
14 13 4 8 subdid ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ⁢ A − B = 2 ⁢ A − 2 ⁢ B
15 14 oveq1d ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ⁢ A − B 2 = 2 ⁢ A − 2 ⁢ B 2
16 zsubcl ⊢ A ∈ ℤ ∧ B ∈ ℤ → A − B ∈ ℤ
17 zcn ⊢ A − B ∈ ℤ → A − B ∈ ℂ
18 16 17 syl ⊢ A ∈ ℤ ∧ B ∈ ℤ → A − B ∈ ℂ
19 2ne0 ⊢ 2 ≠ 0
20 19 a1i ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ≠ 0
21 18 13 20 divcan3d ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ⁢ A − B 2 = A − B
22 15 21 eqtr3d ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ⁢ A − 2 ⁢ B 2 = A − B
23 22 16 eqeltrd ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ⁢ A − 2 ⁢ B 2 ∈ ℤ
24 oveq1 ⊢ 2 ⁢ A − 2 ⁢ B = 1 → 2 ⁢ A − 2 ⁢ B 2 = 1 2
25 24 eleq1d ⊢ 2 ⁢ A − 2 ⁢ B = 1 → 2 ⁢ A − 2 ⁢ B 2 ∈ ℤ ↔ 1 2 ∈ ℤ
26 23 25 syl5ibcom ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ⁢ A − 2 ⁢ B = 1 → 1 2 ∈ ℤ
27 12 26 sylbird ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ⁢ B + 1 = 2 ⁢ A → 1 2 ∈ ℤ
28 27 necon3bd ⊢ A ∈ ℤ ∧ B ∈ ℤ → ¬ 1 2 ∈ ℤ → 2 ⁢ B + 1 ≠ 2 ⁢ A
29 1 28 mpi ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ⁢ B + 1 ≠ 2 ⁢ A
30 29 necomd ⊢ A ∈ ℤ ∧ B ∈ ℤ → 2 ⁢ A ≠ 2 ⁢ B + 1