This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem nnneo

Description: If a natural number is even, its successor is odd. (Contributed by Mario Carneiro, 16-Nov-2014)

Ref Expression
Assertion nnneo 
|- ( ( A e. _om /\ B e. _om /\ C = ( 2o .o A ) ) -> -. suc C = ( 2o .o B ) )

Proof

Step Hyp Ref Expression
1 nnon 
 |-  ( A e. _om -> A e. On )
2 onnbtwn 
 |-  ( A e. On -> -. ( A e. B /\ B e. suc A ) )
3 1 2 syl 
 |-  ( A e. _om -> -. ( A e. B /\ B e. suc A ) )
4 3 3ad2ant1 
 |-  ( ( A e. _om /\ B e. _om /\ C = ( 2o .o A ) ) -> -. ( A e. B /\ B e. suc A ) )
5 suceq 
 |-  ( C = ( 2o .o A ) -> suc C = suc ( 2o .o A ) )
6 5 eqeq1d 
 |-  ( C = ( 2o .o A ) -> ( suc C = ( 2o .o B ) <-> suc ( 2o .o A ) = ( 2o .o B ) ) )
7 6 3ad2ant3 
 |-  ( ( A e. _om /\ B e. _om /\ C = ( 2o .o A ) ) -> ( suc C = ( 2o .o B ) <-> suc ( 2o .o A ) = ( 2o .o B ) ) )
8 ovex 
 |-  ( 2o .o A ) e. _V
9 8 sucid 
 |-  ( 2o .o A ) e. suc ( 2o .o A )
10 eleq2 
 |-  ( suc ( 2o .o A ) = ( 2o .o B ) -> ( ( 2o .o A ) e. suc ( 2o .o A ) <-> ( 2o .o A ) e. ( 2o .o B ) ) )
11 9 10 mpbii 
 |-  ( suc ( 2o .o A ) = ( 2o .o B ) -> ( 2o .o A ) e. ( 2o .o B ) )
12 2onn 
 |-  2o e. _om
13 nnmord 
 |-  ( ( A e. _om /\ B e. _om /\ 2o e. _om ) -> ( ( A e. B /\ (/) e. 2o ) <-> ( 2o .o A ) e. ( 2o .o B ) ) )
14 12 13 mp3an3 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( A e. B /\ (/) e. 2o ) <-> ( 2o .o A ) e. ( 2o .o B ) ) )
15 simpl 
 |-  ( ( A e. B /\ (/) e. 2o ) -> A e. B )
16 14 15 biimtrrdi 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( 2o .o A ) e. ( 2o .o B ) -> A e. B ) )
17 11 16 syl5 
 |-  ( ( A e. _om /\ B e. _om ) -> ( suc ( 2o .o A ) = ( 2o .o B ) -> A e. B ) )
18 simpr 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ suc ( 2o .o A ) = ( 2o .o B ) ) -> suc ( 2o .o A ) = ( 2o .o B ) )
19 nnmcl 
 |-  ( ( 2o e. _om /\ A e. _om ) -> ( 2o .o A ) e. _om )
20 12 19 mpan 
 |-  ( A e. _om -> ( 2o .o A ) e. _om )
21 nnon 
 |-  ( ( 2o .o A ) e. _om -> ( 2o .o A ) e. On )
22 oa1suc 
 |-  ( ( 2o .o A ) e. On -> ( ( 2o .o A ) +o 1o ) = suc ( 2o .o A ) )
23 20 21 22 3syl 
 |-  ( A e. _om -> ( ( 2o .o A ) +o 1o ) = suc ( 2o .o A ) )
24 1oex 
 |-  1o e. _V
25 24 sucid 
 |-  1o e. suc 1o
26 df-2o 
 |-  2o = suc 1o
27 25 26 eleqtrri 
 |-  1o e. 2o
28 1onn 
 |-  1o e. _om
29 nnaord 
 |-  ( ( 1o e. _om /\ 2o e. _om /\ ( 2o .o A ) e. _om ) -> ( 1o e. 2o <-> ( ( 2o .o A ) +o 1o ) e. ( ( 2o .o A ) +o 2o ) ) )
30 28 12 20 29 mp3an12i 
 |-  ( A e. _om -> ( 1o e. 2o <-> ( ( 2o .o A ) +o 1o ) e. ( ( 2o .o A ) +o 2o ) ) )
31 27 30 mpbii 
 |-  ( A e. _om -> ( ( 2o .o A ) +o 1o ) e. ( ( 2o .o A ) +o 2o ) )
32 nnmsuc 
 |-  ( ( 2o e. _om /\ A e. _om ) -> ( 2o .o suc A ) = ( ( 2o .o A ) +o 2o ) )
33 12 32 mpan 
 |-  ( A e. _om -> ( 2o .o suc A ) = ( ( 2o .o A ) +o 2o ) )
34 31 33 eleqtrrd 
 |-  ( A e. _om -> ( ( 2o .o A ) +o 1o ) e. ( 2o .o suc A ) )
35 23 34 eqeltrrd 
 |-  ( A e. _om -> suc ( 2o .o A ) e. ( 2o .o suc A ) )
36 35 ad2antrr 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ suc ( 2o .o A ) = ( 2o .o B ) ) -> suc ( 2o .o A ) e. ( 2o .o suc A ) )
37 18 36 eqeltrrd 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ suc ( 2o .o A ) = ( 2o .o B ) ) -> ( 2o .o B ) e. ( 2o .o suc A ) )
38 peano2 
 |-  ( A e. _om -> suc A e. _om )
39 nnmord 
 |-  ( ( B e. _om /\ suc A e. _om /\ 2o e. _om ) -> ( ( B e. suc A /\ (/) e. 2o ) <-> ( 2o .o B ) e. ( 2o .o suc A ) ) )
40 12 39 mp3an3 
 |-  ( ( B e. _om /\ suc A e. _om ) -> ( ( B e. suc A /\ (/) e. 2o ) <-> ( 2o .o B ) e. ( 2o .o suc A ) ) )
41 38 40 sylan2 
 |-  ( ( B e. _om /\ A e. _om ) -> ( ( B e. suc A /\ (/) e. 2o ) <-> ( 2o .o B ) e. ( 2o .o suc A ) ) )
42 41 ancoms 
 |-  ( ( A e. _om /\ B e. _om ) -> ( ( B e. suc A /\ (/) e. 2o ) <-> ( 2o .o B ) e. ( 2o .o suc A ) ) )
43 42 adantr 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ suc ( 2o .o A ) = ( 2o .o B ) ) -> ( ( B e. suc A /\ (/) e. 2o ) <-> ( 2o .o B ) e. ( 2o .o suc A ) ) )
44 37 43 mpbird 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ suc ( 2o .o A ) = ( 2o .o B ) ) -> ( B e. suc A /\ (/) e. 2o ) )
45 44 simpld 
 |-  ( ( ( A e. _om /\ B e. _om ) /\ suc ( 2o .o A ) = ( 2o .o B ) ) -> B e. suc A )
46 45 ex 
 |-  ( ( A e. _om /\ B e. _om ) -> ( suc ( 2o .o A ) = ( 2o .o B ) -> B e. suc A ) )
47 17 46 jcad 
 |-  ( ( A e. _om /\ B e. _om ) -> ( suc ( 2o .o A ) = ( 2o .o B ) -> ( A e. B /\ B e. suc A ) ) )
48 47 3adant3 
 |-  ( ( A e. _om /\ B e. _om /\ C = ( 2o .o A ) ) -> ( suc ( 2o .o A ) = ( 2o .o B ) -> ( A e. B /\ B e. suc A ) ) )
49 7 48 sylbid 
 |-  ( ( A e. _om /\ B e. _om /\ C = ( 2o .o A ) ) -> ( suc C = ( 2o .o B ) -> ( A e. B /\ B e. suc A ) ) )
50 4 49 mtod 
 |-  ( ( A e. _om /\ B e. _om /\ C = ( 2o .o A ) ) -> -. suc C = ( 2o .o B ) )