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

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 ( ( 𝐴 ∈ ℤ ∧ 𝐵 ∈ ℤ ) → ( 2 · 𝐴 ) ≠ ( ( 2 · 𝐵 ) + 1 ) )

Proof

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