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 syl5bi ( 𝑧 ∈ ω → ( ∃ 𝑥 ∈ ω 𝑧 = ( 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 𝑥 ) ) )