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 ( 𝐴 ∈ ω → ( ∃ 𝑥 ∈ ω 𝐴 = ( 2o ·o 𝑥 ) ↔ ¬ ∃ 𝑥 ∈ ω suc 𝐴 = ( 2o ·o 𝑥 ) ) )

Proof

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