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∈ω∧B∈ω∧C=2𝑜⋅𝑜A→¬suc⁡C=2𝑜⋅𝑜B

Proof

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