Metamath Proof Explorer

Theorem nneob

Description: A natural number is even iff its successor is odd. (Contributed by NM, 26-Jan-2006) (Revised by Mario Carneiro, 15-Nov-2014)

Ref Expression
Assertion nneob ⊢ A ∈ ω → ∃ x ∈ ω A = 2 𝑜 ⋅ 𝑜 x ↔ ¬ ∃ x ∈ ω suc ⁡ A = 2 𝑜 ⋅ 𝑜 x

Proof

Step Hyp Ref Expression
1 oveq2 ⊢ x = y → 2 𝑜 ⋅ 𝑜 x = 2 𝑜 ⋅ 𝑜 y
2 1 eqeq2d ⊢ x = y → A = 2 𝑜 ⋅ 𝑜 x ↔ A = 2 𝑜 ⋅ 𝑜 y
3 2 cbvrexvw ⊢ ∃ x ∈ ω A = 2 𝑜 ⋅ 𝑜 x ↔ ∃ y ∈ ω A = 2 𝑜 ⋅ 𝑜 y
4 nnneo ⊢ y ∈ ω ∧ x ∈ ω ∧ A = 2 𝑜 ⋅ 𝑜 y → ¬ suc ⁡ A = 2 𝑜 ⋅ 𝑜 x
5 4 3com23 ⊢ y ∈ ω ∧ A = 2 𝑜 ⋅ 𝑜 y ∧ x ∈ ω → ¬ suc ⁡ A = 2 𝑜 ⋅ 𝑜 x
6 5 3expa ⊢ y ∈ ω ∧ A = 2 𝑜 ⋅ 𝑜 y ∧ x ∈ ω → ¬ suc ⁡ A = 2 𝑜 ⋅ 𝑜 x
7 6 nrexdv ⊢ y ∈ ω ∧ A = 2 𝑜 ⋅ 𝑜 y → ¬ ∃ x ∈ ω suc ⁡ A = 2 𝑜 ⋅ 𝑜 x
8 7 rexlimiva ⊢ ∃ y ∈ ω A = 2 𝑜 ⋅ 𝑜 y → ¬ ∃ x ∈ ω suc ⁡ A = 2 𝑜 ⋅ 𝑜 x
9 3 8 sylbi ⊢ ∃ x ∈ ω A = 2 𝑜 ⋅ 𝑜 x → ¬ ∃ x ∈ ω suc ⁡ A = 2 𝑜 ⋅ 𝑜 x
10 suceq ⊢ y = ∅ → suc ⁡ y = suc ⁡ ∅
11 10 eqeq1d ⊢ y = ∅ → suc ⁡ y = 2 𝑜 ⋅ 𝑜 x ↔ suc ⁡ ∅ = 2 𝑜 ⋅ 𝑜 x
12 11 rexbidv ⊢ y = ∅ → ∃ x ∈ ω suc ⁡ y = 2 𝑜 ⋅ 𝑜 x ↔ ∃ x ∈ ω suc ⁡ ∅ = 2 𝑜 ⋅ 𝑜 x
13 12 notbid ⊢ y = ∅ → ¬ ∃ x ∈ ω suc ⁡ y = 2 𝑜 ⋅ 𝑜 x ↔ ¬ ∃ x ∈ ω suc ⁡ ∅ = 2 𝑜 ⋅ 𝑜 x
14 eqeq1 ⊢ y = ∅ → y = 2 𝑜 ⋅ 𝑜 x ↔ ∅ = 2 𝑜 ⋅ 𝑜 x
15 14 rexbidv ⊢ y = ∅ → ∃ x ∈ ω y = 2 𝑜 ⋅ 𝑜 x ↔ ∃ x ∈ ω ∅ = 2 𝑜 ⋅ 𝑜 x
16 13 15 imbi12d ⊢ y = ∅ → ¬ ∃ x ∈ ω suc ⁡ y = 2 𝑜 ⋅ 𝑜 x → ∃ x ∈ ω y = 2 𝑜 ⋅ 𝑜 x ↔ ¬ ∃ x ∈ ω suc ⁡ ∅ = 2 𝑜 ⋅ 𝑜 x → ∃ x ∈ ω ∅ = 2 𝑜 ⋅ 𝑜 x
17 suceq ⊢ y = z → suc ⁡ y = suc ⁡ z
18 17 eqeq1d ⊢ y = z → suc ⁡ y = 2 𝑜 ⋅ 𝑜 x ↔ suc ⁡ z = 2 𝑜 ⋅ 𝑜 x
19 18 rexbidv ⊢ y = z → ∃ x ∈ ω suc ⁡ y = 2 𝑜 ⋅ 𝑜 x ↔ ∃ x ∈ ω suc ⁡ z = 2 𝑜 ⋅ 𝑜 x
20 19 notbid ⊢ y = z → ¬ ∃ x ∈ ω suc ⁡ y = 2 𝑜 ⋅ 𝑜 x ↔ ¬ ∃ x ∈ ω suc ⁡ z = 2 𝑜 ⋅ 𝑜 x
21 eqeq1 ⊢ y = z → y = 2 𝑜 ⋅ 𝑜 x ↔ z = 2 𝑜 ⋅ 𝑜 x
22 21 rexbidv ⊢ y = z → ∃ x ∈ ω y = 2 𝑜 ⋅ 𝑜 x ↔ ∃ x ∈ ω z = 2 𝑜 ⋅ 𝑜 x
23 20 22 imbi12d ⊢ y = z → ¬ ∃ x ∈ ω suc ⁡ y = 2 𝑜 ⋅ 𝑜 x → ∃ x ∈ ω y = 2 𝑜 ⋅ 𝑜 x ↔ ¬ ∃ x ∈ ω suc ⁡ z = 2 𝑜 ⋅ 𝑜 x → ∃ x ∈ ω z = 2 𝑜 ⋅ 𝑜 x
24 suceq ⊢ y = suc ⁡ z → suc ⁡ y = suc ⁡ suc ⁡ z
25 24 eqeq1d ⊢ y = suc ⁡ z → suc ⁡ y = 2 𝑜 ⋅ 𝑜 x ↔ suc ⁡ suc ⁡ z = 2 𝑜 ⋅ 𝑜 x
26 25 rexbidv ⊢ y = suc ⁡ z → ∃ x ∈ ω suc ⁡ y = 2 𝑜 ⋅ 𝑜 x ↔ ∃ x ∈ ω suc ⁡ suc ⁡ z = 2 𝑜 ⋅ 𝑜 x
27 26 notbid ⊢ y = suc ⁡ z → ¬ ∃ x ∈ ω suc ⁡ y = 2 𝑜 ⋅ 𝑜 x ↔ ¬ ∃ x ∈ ω suc ⁡ suc ⁡ z = 2 𝑜 ⋅ 𝑜 x
28 eqeq1 ⊢ y = suc ⁡ z → y = 2 𝑜 ⋅ 𝑜 x ↔ suc ⁡ z = 2 𝑜 ⋅ 𝑜 x
29 28 rexbidv ⊢ y = suc ⁡ z → ∃ x ∈ ω y = 2 𝑜 ⋅ 𝑜 x ↔ ∃ x ∈ ω suc ⁡ z = 2 𝑜 ⋅ 𝑜 x
30 27 29 imbi12d ⊢ y = suc ⁡ z → ¬ ∃ x ∈ ω suc ⁡ y = 2 𝑜 ⋅ 𝑜 x → ∃ x ∈ ω y = 2 𝑜 ⋅ 𝑜 x ↔ ¬ ∃ x ∈ ω suc ⁡ suc ⁡ z = 2 𝑜 ⋅ 𝑜 x → ∃ x ∈ ω suc ⁡ z = 2 𝑜 ⋅ 𝑜 x
31 suceq ⊢ y = A → suc ⁡ y = suc ⁡ A
32 31 eqeq1d ⊢ y = A → suc ⁡ y = 2 𝑜 ⋅ 𝑜 x ↔ suc ⁡ A = 2 𝑜 ⋅ 𝑜 x
33 32 rexbidv ⊢ y = A → ∃ x ∈ ω suc ⁡ y = 2 𝑜 ⋅ 𝑜 x ↔ ∃ x ∈ ω suc ⁡ A = 2 𝑜 ⋅ 𝑜 x
34 33 notbid ⊢ y = A → ¬ ∃ x ∈ ω suc ⁡ y = 2 𝑜 ⋅ 𝑜 x ↔ ¬ ∃ x ∈ ω suc ⁡ A = 2 𝑜 ⋅ 𝑜 x
35 eqeq1 ⊢ y = A → y = 2 𝑜 ⋅ 𝑜 x ↔ A = 2 𝑜 ⋅ 𝑜 x
36 35 rexbidv ⊢ y = A → ∃ x ∈ ω y = 2 𝑜 ⋅ 𝑜 x ↔ ∃ x ∈ ω A = 2 𝑜 ⋅ 𝑜 x
37 34 36 imbi12d ⊢ y = A → ¬ ∃ x ∈ ω suc ⁡ y = 2 𝑜 ⋅ 𝑜 x → ∃ x ∈ ω y = 2 𝑜 ⋅ 𝑜 x ↔ ¬ ∃ x ∈ ω suc ⁡ A = 2 𝑜 ⋅ 𝑜 x → ∃ x ∈ ω A = 2 𝑜 ⋅ 𝑜 x
38 peano1 ⊢ ∅ ∈ ω
39 eqid ⊢ ∅ = ∅
40 oveq2 ⊢ x = ∅ → 2 𝑜 ⋅ 𝑜 x = 2 𝑜 ⋅ 𝑜 ∅
41 2on ⊢ 2 𝑜 ∈ On
42 om0 ⊢ 2 𝑜 ∈ On → 2 𝑜 ⋅ 𝑜 ∅ = ∅
43 41 42 ax-mp ⊢ 2 𝑜 ⋅ 𝑜 ∅ = ∅
44 40 43 eqtrdi ⊢ x = ∅ → 2 𝑜 ⋅ 𝑜 x = ∅
45 44 rspceeqv ⊢ ∅ ∈ ω ∧ ∅ = ∅ → ∃ x ∈ ω ∅ = 2 𝑜 ⋅ 𝑜 x
46 38 39 45 mp2an ⊢ ∃ x ∈ ω ∅ = 2 𝑜 ⋅ 𝑜 x
47 46 a1i ⊢ ¬ ∃ x ∈ ω suc ⁡ ∅ = 2 𝑜 ⋅ 𝑜 x → ∃ x ∈ ω ∅ = 2 𝑜 ⋅ 𝑜 x
48 1 eqeq2d ⊢ x = y → z = 2 𝑜 ⋅ 𝑜 x ↔ z = 2 𝑜 ⋅ 𝑜 y
49 48 cbvrexvw ⊢ ∃ x ∈ ω z = 2 𝑜 ⋅ 𝑜 x ↔ ∃ y ∈ ω z = 2 𝑜 ⋅ 𝑜 y
50 peano2 ⊢ y ∈ ω → suc ⁡ y ∈ ω
51 2onn ⊢ 2 𝑜 ∈ ω
52 nnmsuc ⊢ 2 𝑜 ∈ ω ∧ y ∈ ω → 2 𝑜 ⋅ 𝑜 suc ⁡ y = 2 𝑜 ⋅ 𝑜 y + 𝑜 2 𝑜
53 51 52 mpan ⊢ y ∈ ω → 2 𝑜 ⋅ 𝑜 suc ⁡ y = 2 𝑜 ⋅ 𝑜 y + 𝑜 2 𝑜
54 df-2o ⊢ 2 𝑜 = suc ⁡ 1 𝑜
55 54 oveq2i ⊢ 2 𝑜 ⋅ 𝑜 y + 𝑜 2 𝑜 = 2 𝑜 ⋅ 𝑜 y + 𝑜 suc ⁡ 1 𝑜
56 nnmcl ⊢ 2 𝑜 ∈ ω ∧ y ∈ ω → 2 𝑜 ⋅ 𝑜 y ∈ ω
57 51 56 mpan ⊢ y ∈ ω → 2 𝑜 ⋅ 𝑜 y ∈ ω
58 1onn ⊢ 1 𝑜 ∈ ω
59 nnasuc ⊢ 2 𝑜 ⋅ 𝑜 y ∈ ω ∧ 1 𝑜 ∈ ω → 2 𝑜 ⋅ 𝑜 y + 𝑜 suc ⁡ 1 𝑜 = suc ⁡ 2 𝑜 ⋅ 𝑜 y + 𝑜 1 𝑜
60 57 58 59 sylancl ⊢ y ∈ ω → 2 𝑜 ⋅ 𝑜 y + 𝑜 suc ⁡ 1 𝑜 = suc ⁡ 2 𝑜 ⋅ 𝑜 y + 𝑜 1 𝑜
61 55 60 syl5req ⊢ y ∈ ω → suc ⁡ 2 𝑜 ⋅ 𝑜 y + 𝑜 1 𝑜 = 2 𝑜 ⋅ 𝑜 y + 𝑜 2 𝑜
62 nnon ⊢ 2 𝑜 ⋅ 𝑜 y ∈ ω → 2 𝑜 ⋅ 𝑜 y ∈ On
63 oa1suc ⊢ 2 𝑜 ⋅ 𝑜 y ∈ On → 2 𝑜 ⋅ 𝑜 y + 𝑜 1 𝑜 = suc ⁡ 2 𝑜 ⋅ 𝑜 y
64 suceq ⊢ 2 𝑜 ⋅ 𝑜 y + 𝑜 1 𝑜 = suc ⁡ 2 𝑜 ⋅ 𝑜 y → suc ⁡ 2 𝑜 ⋅ 𝑜 y + 𝑜 1 𝑜 = suc ⁡ suc ⁡ 2 𝑜 ⋅ 𝑜 y
65 57 62 63 64 4syl ⊢ y ∈ ω → suc ⁡ 2 𝑜 ⋅ 𝑜 y + 𝑜 1 𝑜 = suc ⁡ suc ⁡ 2 𝑜 ⋅ 𝑜 y
66 53 61 65 3eqtr2rd ⊢ y ∈ ω → suc ⁡ suc ⁡ 2 𝑜 ⋅ 𝑜 y = 2 𝑜 ⋅ 𝑜 suc ⁡ y
67 oveq2 ⊢ x = suc ⁡ y → 2 𝑜 ⋅ 𝑜 x = 2 𝑜 ⋅ 𝑜 suc ⁡ y
68 67 rspceeqv ⊢ suc ⁡ y ∈ ω ∧ suc ⁡ suc ⁡ 2 𝑜 ⋅ 𝑜 y = 2 𝑜 ⋅ 𝑜 suc ⁡ y → ∃ x ∈ ω suc ⁡ suc ⁡ 2 𝑜 ⋅ 𝑜 y = 2 𝑜 ⋅ 𝑜 x
69 50 66 68 syl2anc ⊢ y ∈ ω → ∃ x ∈ ω suc ⁡ suc ⁡ 2 𝑜 ⋅ 𝑜 y = 2 𝑜 ⋅ 𝑜 x
70 suceq ⊢ z = 2 𝑜 ⋅ 𝑜 y → suc ⁡ z = suc ⁡ 2 𝑜 ⋅ 𝑜 y
71 suceq ⊢ suc ⁡ z = suc ⁡ 2 𝑜 ⋅ 𝑜 y → suc ⁡ suc ⁡ z = suc ⁡ suc ⁡ 2 𝑜 ⋅ 𝑜 y
72 70 71 syl ⊢ z = 2 𝑜 ⋅ 𝑜 y → suc ⁡ suc ⁡ z = suc ⁡ suc ⁡ 2 𝑜 ⋅ 𝑜 y
73 72 eqeq1d ⊢ z = 2 𝑜 ⋅ 𝑜 y → suc ⁡ suc ⁡ z = 2 𝑜 ⋅ 𝑜 x ↔ suc ⁡ suc ⁡ 2 𝑜 ⋅ 𝑜 y = 2 𝑜 ⋅ 𝑜 x
74 73 rexbidv ⊢ z = 2 𝑜 ⋅ 𝑜 y → ∃ x ∈ ω suc ⁡ suc ⁡ z = 2 𝑜 ⋅ 𝑜 x ↔ ∃ x ∈ ω suc ⁡ suc ⁡ 2 𝑜 ⋅ 𝑜 y = 2 𝑜 ⋅ 𝑜 x
75 69 74 syl5ibrcom ⊢ y ∈ ω → z = 2 𝑜 ⋅ 𝑜 y → ∃ x ∈ ω suc ⁡ suc ⁡ z = 2 𝑜 ⋅ 𝑜 x
76 75 rexlimiv ⊢ ∃ y ∈ ω z = 2 𝑜 ⋅ 𝑜 y → ∃ x ∈ ω suc ⁡ suc ⁡ z = 2 𝑜 ⋅ 𝑜 x
77 76 a1i ⊢ z ∈ ω → ∃ y ∈ ω z = 2 𝑜 ⋅ 𝑜 y → ∃ x ∈ ω suc ⁡ suc ⁡ z = 2 𝑜 ⋅ 𝑜 x
78 49 77 syl5bi ⊢ z ∈ ω → ∃ x ∈ ω z = 2 𝑜 ⋅ 𝑜 x → ∃ x ∈ ω suc ⁡ suc ⁡ z = 2 𝑜 ⋅ 𝑜 x
79 78 con3d ⊢ z ∈ ω → ¬ ∃ x ∈ ω suc ⁡ suc ⁡ z = 2 𝑜 ⋅ 𝑜 x → ¬ ∃ x ∈ ω z = 2 𝑜 ⋅ 𝑜 x
80 con1 ⊢ ¬ ∃ x ∈ ω suc ⁡ z = 2 𝑜 ⋅ 𝑜 x → ∃ x ∈ ω z = 2 𝑜 ⋅ 𝑜 x → ¬ ∃ x ∈ ω z = 2 𝑜 ⋅ 𝑜 x → ∃ x ∈ ω suc ⁡ z = 2 𝑜 ⋅ 𝑜 x
81 79 80 syl9 ⊢ z ∈ ω → ¬ ∃ x ∈ ω suc ⁡ z = 2 𝑜 ⋅ 𝑜 x → ∃ x ∈ ω z = 2 𝑜 ⋅ 𝑜 x → ¬ ∃ x ∈ ω suc ⁡ suc ⁡ z = 2 𝑜 ⋅ 𝑜 x → ∃ x ∈ ω suc ⁡ z = 2 𝑜 ⋅ 𝑜 x
82 16 23 30 37 47 81 finds ⊢ A ∈ ω → ¬ ∃ x ∈ ω suc ⁡ A = 2 𝑜 ⋅ 𝑜 x → ∃ x ∈ ω A = 2 𝑜 ⋅ 𝑜 x
83 9 82 impbid2 ⊢ A ∈ ω → ∃ x ∈ ω A = 2 𝑜 ⋅ 𝑜 x ↔ ¬ ∃ x ∈ ω suc ⁡ A = 2 𝑜 ⋅ 𝑜 x