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