Metamath Proof Explorer

Theorem nneob

Description: A natural number is even iff its successor is odd. (Contributed by NM, 26-Jan-2006) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nneob 
|- ( A e. _om -> ( E. x e. _om A = ( 2o .o x ) <-> -. E. x e. _om suc A = ( 2o .o x ) ) )

Proof

Step Hyp Ref Expression
1 oveq2 
 |-  ( x = y -> ( 2o .o x ) = ( 2o .o y ) )
2 1 eqeq2d 
 |-  ( x = y -> ( A = ( 2o .o x ) <-> A = ( 2o .o y ) ) )
3 2 cbvrexvw 
 |-  ( E. x e. _om A = ( 2o .o x ) <-> E. y e. _om A = ( 2o .o y ) )
4 nnneo 
 |-  ( ( y e. _om /\ x e. _om /\ A = ( 2o .o y ) ) -> -. suc A = ( 2o .o x ) )
5 4 3com23 
 |-  ( ( y e. _om /\ A = ( 2o .o y ) /\ x e. _om ) -> -. suc A = ( 2o .o x ) )
6 5 3expa 
 |-  ( ( ( y e. _om /\ A = ( 2o .o y ) ) /\ x e. _om ) -> -. suc A = ( 2o .o x ) )
7 6 nrexdv 
 |-  ( ( y e. _om /\ A = ( 2o .o y ) ) -> -. E. x e. _om suc A = ( 2o .o x ) )
8 7 rexlimiva 
 |-  ( E. y e. _om A = ( 2o .o y ) -> -. E. x e. _om suc A = ( 2o .o x ) )
9 3 8 sylbi 
 |-  ( E. x e. _om A = ( 2o .o x ) -> -. E. x e. _om suc A = ( 2o .o x ) )
10 suceq 
 |-  ( y = (/) -> suc y = suc (/) )
11 10 eqeq1d 
 |-  ( y = (/) -> ( suc y = ( 2o .o x ) <-> suc (/) = ( 2o .o x ) ) )
12 11 rexbidv 
 |-  ( y = (/) -> ( E. x e. _om suc y = ( 2o .o x ) <-> E. x e. _om suc (/) = ( 2o .o x ) ) )
13 12 notbid 
 |-  ( y = (/) -> ( -. E. x e. _om suc y = ( 2o .o x ) <-> -. E. x e. _om suc (/) = ( 2o .o x ) ) )
14 eqeq1 
 |-  ( y = (/) -> ( y = ( 2o .o x ) <-> (/) = ( 2o .o x ) ) )
15 14 rexbidv 
 |-  ( y = (/) -> ( E. x e. _om y = ( 2o .o x ) <-> E. x e. _om (/) = ( 2o .o x ) ) )
16 13 15 imbi12d 
 |-  ( y = (/) -> ( ( -. E. x e. _om suc y = ( 2o .o x ) -> E. x e. _om y = ( 2o .o x ) ) <-> ( -. E. x e. _om suc (/) = ( 2o .o x ) -> E. x e. _om (/) = ( 2o .o x ) ) ) )
17 suceq 
 |-  ( y = z -> suc y = suc z )
18 17 eqeq1d 
 |-  ( y = z -> ( suc y = ( 2o .o x ) <-> suc z = ( 2o .o x ) ) )
19 18 rexbidv 
 |-  ( y = z -> ( E. x e. _om suc y = ( 2o .o x ) <-> E. x e. _om suc z = ( 2o .o x ) ) )
20 19 notbid 
 |-  ( y = z -> ( -. E. x e. _om suc y = ( 2o .o x ) <-> -. E. x e. _om suc z = ( 2o .o x ) ) )
21 eqeq1 
 |-  ( y = z -> ( y = ( 2o .o x ) <-> z = ( 2o .o x ) ) )
22 21 rexbidv 
 |-  ( y = z -> ( E. x e. _om y = ( 2o .o x ) <-> E. x e. _om z = ( 2o .o x ) ) )
23 20 22 imbi12d 
 |-  ( y = z -> ( ( -. E. x e. _om suc y = ( 2o .o x ) -> E. x e. _om y = ( 2o .o x ) ) <-> ( -. E. x e. _om suc z = ( 2o .o x ) -> E. x e. _om z = ( 2o .o x ) ) ) )
24 suceq 
 |-  ( y = suc z -> suc y = suc suc z )
25 24 eqeq1d 
 |-  ( y = suc z -> ( suc y = ( 2o .o x ) <-> suc suc z = ( 2o .o x ) ) )
26 25 rexbidv 
 |-  ( y = suc z -> ( E. x e. _om suc y = ( 2o .o x ) <-> E. x e. _om suc suc z = ( 2o .o x ) ) )
27 26 notbid 
 |-  ( y = suc z -> ( -. E. x e. _om suc y = ( 2o .o x ) <-> -. E. x e. _om suc suc z = ( 2o .o x ) ) )
28 eqeq1 
 |-  ( y = suc z -> ( y = ( 2o .o x ) <-> suc z = ( 2o .o x ) ) )
29 28 rexbidv 
 |-  ( y = suc z -> ( E. x e. _om y = ( 2o .o x ) <-> E. x e. _om suc z = ( 2o .o x ) ) )
30 27 29 imbi12d 
 |-  ( y = suc z -> ( ( -. E. x e. _om suc y = ( 2o .o x ) -> E. x e. _om y = ( 2o .o x ) ) <-> ( -. E. x e. _om suc suc z = ( 2o .o x ) -> E. x e. _om suc z = ( 2o .o x ) ) ) )
31 suceq 
 |-  ( y = A -> suc y = suc A )
32 31 eqeq1d 
 |-  ( y = A -> ( suc y = ( 2o .o x ) <-> suc A = ( 2o .o x ) ) )
33 32 rexbidv 
 |-  ( y = A -> ( E. x e. _om suc y = ( 2o .o x ) <-> E. x e. _om suc A = ( 2o .o x ) ) )
34 33 notbid 
 |-  ( y = A -> ( -. E. x e. _om suc y = ( 2o .o x ) <-> -. E. x e. _om suc A = ( 2o .o x ) ) )
35 eqeq1 
 |-  ( y = A -> ( y = ( 2o .o x ) <-> A = ( 2o .o x ) ) )
36 35 rexbidv 
 |-  ( y = A -> ( E. x e. _om y = ( 2o .o x ) <-> E. x e. _om A = ( 2o .o x ) ) )
37 34 36 imbi12d 
 |-  ( y = A -> ( ( -. E. x e. _om suc y = ( 2o .o x ) -> E. x e. _om y = ( 2o .o x ) ) <-> ( -. E. x e. _om suc A = ( 2o .o x ) -> E. x e. _om A = ( 2o .o x ) ) ) )
38 peano1 
 |-  (/) e. _om
39 eqid 
 |-  (/) = (/)
40 oveq2 
 |-  ( x = (/) -> ( 2o .o x ) = ( 2o .o (/) ) )
41 2on 
 |-  2o e. On
42 om0 
 |-  ( 2o e. On -> ( 2o .o (/) ) = (/) )
43 41 42 ax-mp 
 |-  ( 2o .o (/) ) = (/)
44 40 43 eqtrdi 
 |-  ( x = (/) -> ( 2o .o x ) = (/) )
45 44 rspceeqv 
 |-  ( ( (/) e. _om /\ (/) = (/) ) -> E. x e. _om (/) = ( 2o .o x ) )
46 38 39 45 mp2an 
 |-  E. x e. _om (/) = ( 2o .o x )
47 46 a1i 
 |-  ( -. E. x e. _om suc (/) = ( 2o .o x ) -> E. x e. _om (/) = ( 2o .o x ) )
48 1 eqeq2d 
 |-  ( x = y -> ( z = ( 2o .o x ) <-> z = ( 2o .o y ) ) )
49 48 cbvrexvw 
 |-  ( E. x e. _om z = ( 2o .o x ) <-> E. y e. _om z = ( 2o .o y ) )
50 peano2 
 |-  ( y e. _om -> suc y e. _om )
51 2onn 
 |-  2o e. _om
52 nnmsuc 
 |-  ( ( 2o e. _om /\ y e. _om ) -> ( 2o .o suc y ) = ( ( 2o .o y ) +o 2o ) )
53 51 52 mpan 
 |-  ( y e. _om -> ( 2o .o suc y ) = ( ( 2o .o y ) +o 2o ) )
54 df-2o 
 |-  2o = suc 1o
55 54 oveq2i 
 |-  ( ( 2o .o y ) +o 2o ) = ( ( 2o .o y ) +o suc 1o )
56 nnmcl 
 |-  ( ( 2o e. _om /\ y e. _om ) -> ( 2o .o y ) e. _om )
57 51 56 mpan 
 |-  ( y e. _om -> ( 2o .o y ) e. _om )
58 1onn 
 |-  1o e. _om
59 nnasuc 
 |-  ( ( ( 2o .o y ) e. _om /\ 1o e. _om ) -> ( ( 2o .o y ) +o suc 1o ) = suc ( ( 2o .o y ) +o 1o ) )
60 57 58 59 sylancl 
 |-  ( y e. _om -> ( ( 2o .o y ) +o suc 1o ) = suc ( ( 2o .o y ) +o 1o ) )
61 55 60 syl5req 
 |-  ( y e. _om -> suc ( ( 2o .o y ) +o 1o ) = ( ( 2o .o y ) +o 2o ) )
62 nnon 
 |-  ( ( 2o .o y ) e. _om -> ( 2o .o y ) e. On )
63 oa1suc 
 |-  ( ( 2o .o y ) e. On -> ( ( 2o .o y ) +o 1o ) = suc ( 2o .o y ) )
64 suceq 
 |-  ( ( ( 2o .o y ) +o 1o ) = suc ( 2o .o y ) -> suc ( ( 2o .o y ) +o 1o ) = suc suc ( 2o .o y ) )
65 57 62 63 64 4syl 
 |-  ( y e. _om -> suc ( ( 2o .o y ) +o 1o ) = suc suc ( 2o .o y ) )
66 53 61 65 3eqtr2rd 
 |-  ( y e. _om -> suc suc ( 2o .o y ) = ( 2o .o suc y ) )
67 oveq2 
 |-  ( x = suc y -> ( 2o .o x ) = ( 2o .o suc y ) )
68 67 rspceeqv 
 |-  ( ( suc y e. _om /\ suc suc ( 2o .o y ) = ( 2o .o suc y ) ) -> E. x e. _om suc suc ( 2o .o y ) = ( 2o .o x ) )
69 50 66 68 syl2anc 
 |-  ( y e. _om -> E. x e. _om suc suc ( 2o .o y ) = ( 2o .o x ) )
70 suceq 
 |-  ( z = ( 2o .o y ) -> suc z = suc ( 2o .o y ) )
71 suceq 
 |-  ( suc z = suc ( 2o .o y ) -> suc suc z = suc suc ( 2o .o y ) )
72 70 71 syl 
 |-  ( z = ( 2o .o y ) -> suc suc z = suc suc ( 2o .o y ) )
73 72 eqeq1d 
 |-  ( z = ( 2o .o y ) -> ( suc suc z = ( 2o .o x ) <-> suc suc ( 2o .o y ) = ( 2o .o x ) ) )
74 73 rexbidv 
 |-  ( z = ( 2o .o y ) -> ( E. x e. _om suc suc z = ( 2o .o x ) <-> E. x e. _om suc suc ( 2o .o y ) = ( 2o .o x ) ) )
75 69 74 syl5ibrcom 
 |-  ( y e. _om -> ( z = ( 2o .o y ) -> E. x e. _om suc suc z = ( 2o .o x ) ) )
76 75 rexlimiv 
 |-  ( E. y e. _om z = ( 2o .o y ) -> E. x e. _om suc suc z = ( 2o .o x ) )
77 76 a1i 
 |-  ( z e. _om -> ( E. y e. _om z = ( 2o .o y ) -> E. x e. _om suc suc z = ( 2o .o x ) ) )
78 49 77 syl5bi 
 |-  ( z e. _om -> ( E. x e. _om z = ( 2o .o x ) -> E. x e. _om suc suc z = ( 2o .o x ) ) )
79 78 con3d 
 |-  ( z e. _om -> ( -. E. x e. _om suc suc z = ( 2o .o x ) -> -. E. x e. _om z = ( 2o .o x ) ) )
80 con1 
 |-  ( ( -. E. x e. _om suc z = ( 2o .o x ) -> E. x e. _om z = ( 2o .o x ) ) -> ( -. E. x e. _om z = ( 2o .o x ) -> E. x e. _om suc z = ( 2o .o x ) ) )
81 79 80 syl9 
 |-  ( z e. _om -> ( ( -. E. x e. _om suc z = ( 2o .o x ) -> E. x e. _om z = ( 2o .o x ) ) -> ( -. E. x e. _om suc suc z = ( 2o .o x ) -> E. x e. _om suc z = ( 2o .o x ) ) ) )
82 16 23 30 37 47 81 finds 
 |-  ( A e. _om -> ( -. E. x e. _om suc A = ( 2o .o x ) -> E. x e. _om A = ( 2o .o x ) ) )
83 9 82 impbid2 
 |-  ( A e. _om -> ( E. x e. _om A = ( 2o .o x ) <-> -. E. x e. _om suc A = ( 2o .o x ) ) )