# 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 ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to 2{A}\ne 2{B}+1$

### Proof

Step Hyp Ref Expression
1 halfnz ${⊢}¬\frac{1}{2}\in ℤ$
2 2cn ${⊢}2\in ℂ$
3 zcn ${⊢}{A}\in ℤ\to {A}\in ℂ$
4 3 adantr ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}\in ℂ$
5 mulcl ${⊢}\left(2\in ℂ\wedge {A}\in ℂ\right)\to 2{A}\in ℂ$
6 2 4 5 sylancr ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to 2{A}\in ℂ$
7 zcn ${⊢}{B}\in ℤ\to {B}\in ℂ$
8 7 adantl ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {B}\in ℂ$
9 mulcl ${⊢}\left(2\in ℂ\wedge {B}\in ℂ\right)\to 2{B}\in ℂ$
10 2 8 9 sylancr ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to 2{B}\in ℂ$
11 1cnd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to 1\in ℂ$
12 6 10 11 subaddd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(2{A}-2{B}=1↔2{B}+1=2{A}\right)$
13 2 a1i ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to 2\in ℂ$
14 13 4 8 subdid ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to 2\left({A}-{B}\right)=2{A}-2{B}$
15 14 oveq1d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \frac{2\left({A}-{B}\right)}{2}=\frac{2{A}-2{B}}{2}$
16 zsubcl ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}-{B}\in ℤ$
17 zcn ${⊢}{A}-{B}\in ℤ\to {A}-{B}\in ℂ$
18 16 17 syl ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to {A}-{B}\in ℂ$
19 2ne0 ${⊢}2\ne 0$
20 19 a1i ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to 2\ne 0$
21 18 13 20 divcan3d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \frac{2\left({A}-{B}\right)}{2}={A}-{B}$
22 15 21 eqtr3d ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \frac{2{A}-2{B}}{2}={A}-{B}$
23 22 16 eqeltrd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \frac{2{A}-2{B}}{2}\in ℤ$
24 oveq1 ${⊢}2{A}-2{B}=1\to \frac{2{A}-2{B}}{2}=\frac{1}{2}$
25 24 eleq1d ${⊢}2{A}-2{B}=1\to \left(\frac{2{A}-2{B}}{2}\in ℤ↔\frac{1}{2}\in ℤ\right)$
26 23 25 syl5ibcom ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(2{A}-2{B}=1\to \frac{1}{2}\in ℤ\right)$
27 12 26 sylbird ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(2{B}+1=2{A}\to \frac{1}{2}\in ℤ\right)$
28 27 necon3bd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to \left(¬\frac{1}{2}\in ℤ\to 2{B}+1\ne 2{A}\right)$
29 1 28 mpi ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to 2{B}+1\ne 2{A}$
30 29 necomd ${⊢}\left({A}\in ℤ\wedge {B}\in ℤ\right)\to 2{A}\ne 2{B}+1$