Metamath Proof Explorer


Theorem zeo

Description: An integer is even or odd. (Contributed by NM, 1-Jan-2006)

Ref Expression
Assertion zeo NN2N+12

Proof

Step Hyp Ref Expression
1 elz NNN=0NN
2 oveq1 N=0N2=02
3 2cn 2
4 2ne0 20
5 3 4 div0i 02=0
6 0z 0
7 5 6 eqeltri 02
8 2 7 eqeltrdi N=0N2
9 8 pm2.24d N=0¬N2N+12
10 9 adantl NN=0¬N2N+12
11 nnz N2N2
12 11 con3i ¬N2¬N2
13 nneo NN2¬N+12
14 13 biimprd N¬N+12N2
15 14 con1d N¬N2N+12
16 nnz N+12N+12
17 12 15 16 syl56 N¬N2N+12
18 17 adantl NN¬N2N+12
19 recn NN
20 divneg N220N2=N2
21 3 4 20 mp3an23 NN2=N2
22 19 21 syl NN2=N2
23 22 eleq1d NN2N2
24 nnnegz N2N2
25 23 24 syl6bir NN2N2
26 19 halfcld NN2
27 26 negnegd NN2=N2
28 27 eleq1d NN2N2
29 25 28 sylibd NN2N2
30 29 adantr NNN2N2
31 30 con3d NN¬N2¬N2
32 nneo NN2¬-N+12
33 32 biimprd N¬-N+12N2
34 33 con1d N¬N2-N+12
35 nnz -N+12-N+12
36 peano2zm -N+12-N+121
37 ax-1cn 1
38 37 3 negsubdi2i 12=21
39 2m1e1 21=1
40 38 39 eqtr2i 1=12
41 37 3 subcli 12
42 37 41 negcon2i 1=1212=1
43 40 42 mpbi 12=1
44 43 oveq2i - N+1-2=-N+-1
45 negcl NN
46 addsubass N12- N+1-2=- N+1-2
47 37 3 46 mp3an23 N- N+1-2=- N+1-2
48 45 47 syl N- N+1-2=- N+1-2
49 negdi N1N+1=-N+-1
50 37 49 mpan2 NN+1=-N+-1
51 44 48 50 3eqtr4a N- N+1-2=N+1
52 51 oveq1d N- N+1-22=N+12
53 2div2e1 22=1
54 53 eqcomi 1=22
55 54 oveq2i -N+121=-N+1222
56 peano2cn N-N+1
57 45 56 syl N-N+1
58 2cnne0 220
59 divsubdir -N+12220- N+1-22=-N+1222
60 3 58 59 mp3an23 -N+1- N+1-22=-N+1222
61 57 60 syl N- N+1-22=-N+1222
62 55 61 eqtr4id N-N+121=- N+1-22
63 peano2cn NN+1
64 divneg N+1220N+12=N+12
65 3 4 64 mp3an23 N+1N+12=N+12
66 63 65 syl NN+12=N+12
67 52 62 66 3eqtr4d N-N+121=N+12
68 19 67 syl N-N+121=N+12
69 68 eleq1d N-N+121N+12
70 36 69 syl5ib N-N+12N+12
71 znegcl N+12N+12
72 70 71 syl6 N-N+12N+12
73 peano2re NN+1
74 73 recnd NN+1
75 74 halfcld NN+12
76 75 negnegd NN+12=N+12
77 76 eleq1d NN+12N+12
78 72 77 sylibd N-N+12N+12
79 35 78 syl5 N-N+12N+12
80 34 79 sylan9r NN¬N2N+12
81 31 80 syld NN¬N2N+12
82 10 18 81 3jaodan NN=0NN¬N2N+12
83 1 82 sylbi N¬N2N+12
84 83 orrd NN2N+12