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 ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ โˆง ๐ถ = ( 2o ยทo ๐ด ) ) โ†’ ยฌ suc ๐ถ = ( 2o ยทo ๐ต ) )

Proof

Step Hyp Ref Expression
1 nnon โŠข ( ๐ด โˆˆ ฯ‰ โ†’ ๐ด โˆˆ On )
2 onnbtwn โŠข ( ๐ด โˆˆ On โ†’ ยฌ ( ๐ด โˆˆ ๐ต โˆง ๐ต โˆˆ suc ๐ด ) )
3 1 2 syl โŠข ( ๐ด โˆˆ ฯ‰ โ†’ ยฌ ( ๐ด โˆˆ ๐ต โˆง ๐ต โˆˆ suc ๐ด ) )
4 3 3ad2ant1 โŠข ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ โˆง ๐ถ = ( 2o ยทo ๐ด ) ) โ†’ ยฌ ( ๐ด โˆˆ ๐ต โˆง ๐ต โˆˆ suc ๐ด ) )
5 suceq โŠข ( ๐ถ = ( 2o ยทo ๐ด ) โ†’ suc ๐ถ = suc ( 2o ยทo ๐ด ) )
6 5 eqeq1d โŠข ( ๐ถ = ( 2o ยทo ๐ด ) โ†’ ( suc ๐ถ = ( 2o ยทo ๐ต ) โ†” suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) )
7 6 3ad2ant3 โŠข ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ โˆง ๐ถ = ( 2o ยทo ๐ด ) ) โ†’ ( suc ๐ถ = ( 2o ยทo ๐ต ) โ†” suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) )
8 ovex โŠข ( 2o ยทo ๐ด ) โˆˆ V
9 8 sucid โŠข ( 2o ยทo ๐ด ) โˆˆ suc ( 2o ยทo ๐ด )
10 eleq2 โŠข ( suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) โ†’ ( ( 2o ยทo ๐ด ) โˆˆ suc ( 2o ยทo ๐ด ) โ†” ( 2o ยทo ๐ด ) โˆˆ ( 2o ยทo ๐ต ) ) )
11 9 10 mpbii โŠข ( suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) โ†’ ( 2o ยทo ๐ด ) โˆˆ ( 2o ยทo ๐ต ) )
12 2onn โŠข 2o โˆˆ ฯ‰
13 nnmord โŠข ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ โˆง 2o โˆˆ ฯ‰ ) โ†’ ( ( ๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ 2o ) โ†” ( 2o ยทo ๐ด ) โˆˆ ( 2o ยทo ๐ต ) ) )
14 12 13 mp3an3 โŠข ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( ( ๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ 2o ) โ†” ( 2o ยทo ๐ด ) โˆˆ ( 2o ยทo ๐ต ) ) )
15 simpl โŠข ( ( ๐ด โˆˆ ๐ต โˆง โˆ… โˆˆ 2o ) โ†’ ๐ด โˆˆ ๐ต )
16 14 15 syl6bir โŠข ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( ( 2o ยทo ๐ด ) โˆˆ ( 2o ยทo ๐ต ) โ†’ ๐ด โˆˆ ๐ต ) )
17 11 16 syl5 โŠข ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) โ†’ ๐ด โˆˆ ๐ต ) )
18 simpr โŠข ( ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ ) โˆง suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) โ†’ suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) )
19 nnmcl โŠข ( ( 2o โˆˆ ฯ‰ โˆง ๐ด โˆˆ ฯ‰ ) โ†’ ( 2o ยทo ๐ด ) โˆˆ ฯ‰ )
20 12 19 mpan โŠข ( ๐ด โˆˆ ฯ‰ โ†’ ( 2o ยทo ๐ด ) โˆˆ ฯ‰ )
21 nnon โŠข ( ( 2o ยทo ๐ด ) โˆˆ ฯ‰ โ†’ ( 2o ยทo ๐ด ) โˆˆ On )
22 oa1suc โŠข ( ( 2o ยทo ๐ด ) โˆˆ On โ†’ ( ( 2o ยทo ๐ด ) +o 1o ) = suc ( 2o ยทo ๐ด ) )
23 20 21 22 3syl โŠข ( ๐ด โˆˆ ฯ‰ โ†’ ( ( 2o ยทo ๐ด ) +o 1o ) = suc ( 2o ยทo ๐ด ) )
24 1oex โŠข 1o โˆˆ V
25 24 sucid โŠข 1o โˆˆ suc 1o
26 df-2o โŠข 2o = suc 1o
27 25 26 eleqtrri โŠข 1o โˆˆ 2o
28 1onn โŠข 1o โˆˆ ฯ‰
29 nnaord โŠข ( ( 1o โˆˆ ฯ‰ โˆง 2o โˆˆ ฯ‰ โˆง ( 2o ยทo ๐ด ) โˆˆ ฯ‰ ) โ†’ ( 1o โˆˆ 2o โ†” ( ( 2o ยทo ๐ด ) +o 1o ) โˆˆ ( ( 2o ยทo ๐ด ) +o 2o ) ) )
30 28 12 20 29 mp3an12i โŠข ( ๐ด โˆˆ ฯ‰ โ†’ ( 1o โˆˆ 2o โ†” ( ( 2o ยทo ๐ด ) +o 1o ) โˆˆ ( ( 2o ยทo ๐ด ) +o 2o ) ) )
31 27 30 mpbii โŠข ( ๐ด โˆˆ ฯ‰ โ†’ ( ( 2o ยทo ๐ด ) +o 1o ) โˆˆ ( ( 2o ยทo ๐ด ) +o 2o ) )
32 nnmsuc โŠข ( ( 2o โˆˆ ฯ‰ โˆง ๐ด โˆˆ ฯ‰ ) โ†’ ( 2o ยทo suc ๐ด ) = ( ( 2o ยทo ๐ด ) +o 2o ) )
33 12 32 mpan โŠข ( ๐ด โˆˆ ฯ‰ โ†’ ( 2o ยทo suc ๐ด ) = ( ( 2o ยทo ๐ด ) +o 2o ) )
34 31 33 eleqtrrd โŠข ( ๐ด โˆˆ ฯ‰ โ†’ ( ( 2o ยทo ๐ด ) +o 1o ) โˆˆ ( 2o ยทo suc ๐ด ) )
35 23 34 eqeltrrd โŠข ( ๐ด โˆˆ ฯ‰ โ†’ suc ( 2o ยทo ๐ด ) โˆˆ ( 2o ยทo suc ๐ด ) )
36 35 ad2antrr โŠข ( ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ ) โˆง suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) โ†’ suc ( 2o ยทo ๐ด ) โˆˆ ( 2o ยทo suc ๐ด ) )
37 18 36 eqeltrrd โŠข ( ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ ) โˆง suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) โ†’ ( 2o ยทo ๐ต ) โˆˆ ( 2o ยทo suc ๐ด ) )
38 peano2 โŠข ( ๐ด โˆˆ ฯ‰ โ†’ suc ๐ด โˆˆ ฯ‰ )
39 nnmord โŠข ( ( ๐ต โˆˆ ฯ‰ โˆง suc ๐ด โˆˆ ฯ‰ โˆง 2o โˆˆ ฯ‰ ) โ†’ ( ( ๐ต โˆˆ suc ๐ด โˆง โˆ… โˆˆ 2o ) โ†” ( 2o ยทo ๐ต ) โˆˆ ( 2o ยทo suc ๐ด ) ) )
40 12 39 mp3an3 โŠข ( ( ๐ต โˆˆ ฯ‰ โˆง suc ๐ด โˆˆ ฯ‰ ) โ†’ ( ( ๐ต โˆˆ suc ๐ด โˆง โˆ… โˆˆ 2o ) โ†” ( 2o ยทo ๐ต ) โˆˆ ( 2o ยทo suc ๐ด ) ) )
41 38 40 sylan2 โŠข ( ( ๐ต โˆˆ ฯ‰ โˆง ๐ด โˆˆ ฯ‰ ) โ†’ ( ( ๐ต โˆˆ suc ๐ด โˆง โˆ… โˆˆ 2o ) โ†” ( 2o ยทo ๐ต ) โˆˆ ( 2o ยทo suc ๐ด ) ) )
42 41 ancoms โŠข ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( ( ๐ต โˆˆ suc ๐ด โˆง โˆ… โˆˆ 2o ) โ†” ( 2o ยทo ๐ต ) โˆˆ ( 2o ยทo suc ๐ด ) ) )
43 42 adantr โŠข ( ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ ) โˆง suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) โ†’ ( ( ๐ต โˆˆ suc ๐ด โˆง โˆ… โˆˆ 2o ) โ†” ( 2o ยทo ๐ต ) โˆˆ ( 2o ยทo suc ๐ด ) ) )
44 37 43 mpbird โŠข ( ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ ) โˆง suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) โ†’ ( ๐ต โˆˆ suc ๐ด โˆง โˆ… โˆˆ 2o ) )
45 44 simpld โŠข ( ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ ) โˆง suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) ) โ†’ ๐ต โˆˆ suc ๐ด )
46 45 ex โŠข ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) โ†’ ๐ต โˆˆ suc ๐ด ) )
47 17 46 jcad โŠข ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ ) โ†’ ( suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) โ†’ ( ๐ด โˆˆ ๐ต โˆง ๐ต โˆˆ suc ๐ด ) ) )
48 47 3adant3 โŠข ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ โˆง ๐ถ = ( 2o ยทo ๐ด ) ) โ†’ ( suc ( 2o ยทo ๐ด ) = ( 2o ยทo ๐ต ) โ†’ ( ๐ด โˆˆ ๐ต โˆง ๐ต โˆˆ suc ๐ด ) ) )
49 7 48 sylbid โŠข ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ โˆง ๐ถ = ( 2o ยทo ๐ด ) ) โ†’ ( suc ๐ถ = ( 2o ยทo ๐ต ) โ†’ ( ๐ด โˆˆ ๐ต โˆง ๐ต โˆˆ suc ๐ด ) ) )
50 4 49 mtod โŠข ( ( ๐ด โˆˆ ฯ‰ โˆง ๐ต โˆˆ ฯ‰ โˆง ๐ถ = ( 2o ยทo ๐ด ) ) โ†’ ยฌ suc ๐ถ = ( 2o ยทo ๐ต ) )