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 AB2A2B+1

Proof

Step Hyp Ref Expression
1 halfnz ¬12
2 2cn 2
3 zcn AA
4 3 adantr ABA
5 mulcl 2A2A
6 2 4 5 sylancr AB2A
7 zcn BB
8 7 adantl ABB
9 mulcl 2B2B
10 2 8 9 sylancr AB2B
11 1cnd AB1
12 6 10 11 subaddd AB2A2B=12B+1=2A
13 2 a1i AB2
14 13 4 8 subdid AB2AB=2A2B
15 14 oveq1d AB2AB2=2A2B2
16 zsubcl ABAB
17 zcn ABAB
18 16 17 syl ABAB
19 2ne0 20
20 19 a1i AB20
21 18 13 20 divcan3d AB2AB2=AB
22 15 21 eqtr3d AB2A2B2=AB
23 22 16 eqeltrd AB2A2B2
24 oveq1 2A2B=12A2B2=12
25 24 eleq1d 2A2B=12A2B212
26 23 25 syl5ibcom AB2A2B=112
27 12 26 sylbird AB2B+1=2A12
28 27 necon3bd AB¬122B+12A
29 1 28 mpi AB2B+12A
30 29 necomd AB2A2B+1