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 ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ∧ 𝐶 = ( 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 biimtrrdi ⊢ ( ( 𝐴 ∈ ω ∧ 𝐵 ∈ ω ) → ( ( 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 𝐵 ) )