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 𝑥 ) ) )