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 eqtr2id ⊢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 biimtrid ⊢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