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 eqtr2id
 |-  ( 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 ) ) )