Theorem nneob 4239

Description: A natural number is even iff its successor is odd.

Assertion

Ref	Expression
nneob	|- (A e. om -> (E.x e. om A = (2o .o x) <-> -. E.x e. om suc A = (2o .o x)))

Distinct variable group:   x,A

Proof of Theorem nneob

Step	Hyp	Ref	Expression
1		opreq2 3954	. . . . 5 |- (x = y -> (2o .o x) = (2o .o y))
2	1	eqeq2d 1478	. . . 4 |- (x = y -> (A = (2o .o x) <-> A = (2o .o y)))
3	2	cbvrexv 1792	. . 3 |- (E.x e. om A = (2o .o x) <-> E.y e. om A = (2o .o y))
4		oneo 4196	. . . . . . . 8 |- ((y e. On /\ x e. On /\ A = (2o .o y)) -> -. suc A = (2o .o x))
5		nnont 3128	. . . . . . . 8 |- (y e. om -> y e. On)
6		nnont 3128	. . . . . . . 8 |- (x e. om -> x e. On)
7		id 59	. . . . . . . 8 |- (A = (2o .o y) -> A = (2o .o y))
8	4, 5, 6, 7	syl3an 866	. . . . . . 7 |- ((y e. om /\ x e. om /\ A = (2o .o y)) -> -. suc A = (2o .o x))
9	8	3com23 837	. . . . . 6 |- ((y e. om /\ A = (2o .o y) /\ x e. om) -> -. suc A = (2o .o x))
10	9	3expa 831	. . . . 5 |- (((y e. om /\ A = (2o .o y)) /\ x e. om) -> -. suc A = (2o .o x))
11	10	nrexdv 1722	. . . 4 |- ((y e. om /\ A = (2o .o y)) -> -. E.x e. om suc A = (2o .o x))
12	11	r19.23aiva 1736	. . 3 |- (E.y e. om A = (2o .o y) -> -. E.x e. om suc A = (2o .o x))
13	3, 12	sylbi 199	. 2 |- (E.x e. om A = (2o .o x) -> -. E.x e. om suc A = (2o .o x))
14		suceq 3024	. . . . . . 7 |- (y = (/) -> suc y = suc (/))
15	14	eqeq1d 1475	. . . . . 6 |- (y = (/) -> (suc y = (2o .o x) <-> suc (/) = (2o .o x)))
16	15	rexbidv 1656	. . . . 5 |- (y = (/) -> (E.x e. om suc y = (2o .o x) <-> E.x e. om suc (/) = (2o .o x)))
17	16	negbid 609	. . . 4 |- (y = (/) -> (-. E.x e. om suc y = (2o .o x) <-> -. E.x e. om suc (/) = (2o .o x)))
18		eqeq1 1473	. . . . 5 |- (y = (/) -> (y = (2o .o x) <-> (/) = (2o .o x)))
19	18	rexbidv 1656	. . . 4 |- (y = (/) -> (E.x e. om y = (2o .o x) <-> E.x e. om (/) = (2o .o x)))
20	17, 19	imbi12d 624	. . 3 |- (y = (/) -> ((-. E.x e. om suc y = (2o .o x) -> E.x e. om y = (2o .o x)) <-> (-. E.x e. om suc (/) = (2o .o x) -> E.x e. om (/) = (2o .o x))))
21		suceq 3024	. . . . . . 7 |- (y = z -> suc y = suc z)
22	21	eqeq1d 1475	. . . . . 6 |- (y = z -> (suc y = (2o .o x) <-> suc z = (2o .o x)))
23	22	rexbidv 1656	. . . . 5 |- (y = z -> (E.x e. om suc y = (2o .o x) <-> E.x e. om suc z = (2o .o x)))
24	23	negbid 609	. . . 4 |- (y = z -> (-. E.x e. om suc y = (2o .o x) <-> -. E.x e. om suc z = (2o .o x)))
25		eqeq1 1473	. . . . 5 |- (y = z -> (y = (2o .o x) <-> z = (2o .o x)))
26	25	rexbidv 1656	. . . 4 |- (y = z -> (E.x e. om y = (2o .o x) <-> E.x e. om z = (2o .o x)))
27	24, 26	imbi12d 624	. . 3 |- (y = z -> ((-. E.x e. om suc y = (2o .o x) -> E.x e. om y = (2o .o x)) <-> (-. E.x e. om suc z = (2o .o x) -> E.x e. om z = (2o .o x))))
28		suceq 3024	. . . . . . 7 |- (y = suc z -> suc y = suc suc z)
29	28	eqeq1d 1475	. . . . . 6 |- (y = suc z -> (suc y = (2o .o x) <-> suc suc z = (2o .o x)))
30	29	rexbidv 1656	. . . . 5 |- (y = suc z -> (E.x e. om suc y = (2o .o x) <-> E.x e. om suc suc z = (2o .o x)))
31	30	negbid 609	. . . 4 |- (y = suc z -> (-. E.x e. om suc y = (2o .o x) <-> -. E.x e. om suc suc z = (2o .o x)))
32		eqeq1 1473	. . . . 5 |- (y = suc z -> (y = (2o .o x) <-> suc z = (2o .o x)))
33	32	rexbidv 1656	. . . 4 |- (y = suc z -> (E.x e. om y = (2o .o x) <-> E.x e. om suc z = (2o .o x)))
34	31, 33	imbi12d 624	. . 3 |- (y = suc z -> ((-. E.x e. om suc y = (2o .o x) -> E.x e. om y = (2o .o x)) <-> (-. E.x e. om suc suc z = (2o .o x) -> E.x e. om suc z = (2o .o x))))
35		suceq 3024	. . . . . . 7 |- (y = A -> suc y = suc A)
36	35	eqeq1d 1475	. . . . . 6 |- (y = A -> (suc y = (2o .o x) <-> suc A = (2o .o x)))
37	36	rexbidv 1656	. . . . 5 |- (y = A -> (E.x e. om suc y = (2o .o x) <-> E.x e. om suc A = (2o .o x)))
38	37	negbid 609	. . . 4 |- (y = A -> (-. E.x e. om suc y = (2o .o x) <-> -. E.x e. om suc A = (2o .o x)))
39		eqeq1 1473	. . . . 5 |- (y = A -> (y = (2o .o x) <-> A = (2o .o x)))
40	39	rexbidv 1656	. . . 4 |- (y = A -> (E.x e. om y = (2o .o x) <-> E.x e. om A = (2o .o x)))
41	38, 40	imbi12d 624	. . 3 |- (y = A -> ((-. E.x e. om suc y = (2o .o x) -> E.x e. om y = (2o .o x)) <-> (-. E.x e. om suc A = (2o .o x) -> E.x e. om A = (2o .o x))))
42		peano1 3139	. . . . 5 |- (/) e. om
43		eqid 1468	. . . . 5 |- (/) = (/)
44		opreq2 3954	. . . . . . . 8 |- (x = (/) -> (2o .o x) = (2o .o (/)))
45		2on 4123	. . . . . . . . 9 |- 2o e. On
46		om0 4140	. . . . . . . . 9 |- (2o e. On -> (2o .o (/)) = (/))
47	45, 46	ax-mp 7	. . . . . . . 8 |- (2o .o (/)) = (/)
48	44, 47	syl6eq 1515	. . . . . . 7 |- (x = (/) -> (2o .o x) = (/))
49	48	eqeq2d 1478	. . . . . 6 |- (x = (/) -> ((/) = (2o .o x) <-> (/) = (/)))
50	49	rcla4ev 1868	. . . . 5 |- (((/) e. om /\ (/) = (/)) -> E.x e. om (/) = (2o .o x))
51	42, 43, 50	mp2an 695	. . . 4 |- E.x e. om (/) = (2o .o x)
52	51	a1i 8	. . 3 |- (-. E.x e. om suc (/) = (2o .o x) -> E.x e. om (/) = (2o .o x))
53		nnont 3128	. . . . . . . . . . . . . 14 |- (z e. om -> z e. On)
54		1on 4122	. . . . . . . . . . . . . . . . 17 |- 1o e. On
55		oaass 4179	. . . . . . . . . . . . . . . . 17 |- ((z e. On /\ 1o e. On /\ 1o e. On) -> ((z +o 1o) +o 1o) = (z +o (1o +o 1o)))
56	54, 54, 55	mp3an23 905	. . . . . . . . . . . . . . . 16 |- (z e. On -> ((z +o 1o) +o 1o) = (z +o (1o +o 1o)))
57		o1p1e2 4159	. . . . . . . . . . . . . . . . 17 |- (1o +o 1o) = 2o
58	57	opreq2i 3957	. . . . . . . . . . . . . . . 16 |- (z +o (1o +o 1o)) = (z +o 2o)
59	56, 58	syl6req 1516	. . . . . . . . . . . . . . 15 |- (z e. On -> (z +o 2o) = ((z +o 1o) +o 1o))
60		oa1suc 4148	. . . . . . . . . . . . . . . 16 |- (z e. On -> (z +o 1o) = suc z)
61	60	opreq1d 3960	. . . . . . . . . . . . . . 15 |- (z e. On -> ((z +o 1o) +o 1o) = (suc z +o 1o))
62		suceloni 3052	. . . . . . . . . . . . . . . 16 |- (z e. On -> suc z e. On)
63		oa1suc 4148	. . . . . . . . . . . . . . . 16 |- (suc z e. On -> (suc z +o 1o) = suc suc z)
64	62, 63	syl 10	. . . . . . . . . . . . . . 15 |- (z e. On -> (suc z +o 1o) = suc suc z)
65	59, 61, 64	3eqtrd 1503	. . . . . . . . . . . . . 14 |- (z e. On -> (z +o 2o) = suc suc z)
66	53, 65	syl 10	. . . . . . . . . . . . 13 |- (z e. om -> (z +o 2o) = suc suc z)
67	66	eqcomd 1472	. . . . . . . . . . . 12 |- (z e. om -> suc suc z = (z +o 2o))
68	67	ad2antrr 404	. . . . . . . . . . 11 |- (((z e. om /\ y e. om) /\ z = (2o .o y)) -> suc suc z = (z +o 2o))
69		opreq1 3953	. . . . . . . . . . . . 13 |- (z = (2o .o y) -> (z +o 2o) = ((2o .o y) +o 2o))
70		2onn 4238	. . . . . . . . . . . . . . 15 |- 2o e. om
71		1onn 4237	. . . . . . . . . . . . . . 15 |- 1o e. om
72		nndi 4222	. . . . . . . . . . . . . . 15 |- ((2o e. om /\ y e. om /\ 1o e. om) -> (2o .o (y +o 1o)) = ((2o .o y) +o (2o .o 1o)))
73	70, 71, 72	mp3an13 904	. . . . . . . . . . . . . 14 |- (y e. om -> (2o .o (y +o 1o)) = ((2o .o y) +o (2o .o 1o)))
74		om1 4160	. . . . . . . . . . . . . . . 16 |- (2o e. On -> (2o .o 1o) = 2o)
75	45, 74	ax-mp 7	. . . . . . . . . . . . . . 15 |- (2o .o 1o) = 2o
76	75	opreq2i 3957	. . . . . . . . . . . . . 14 |- ((2o .o y) +o (2o .o 1o)) = ((2o .o y) +o 2o)
77	73, 76	syl6req 1516	. . . . . . . . . . . . 13 |- (y e. om -> ((2o .o y) +o 2o) = (2o .o (y +o 1o)))
78	69, 77	sylan9eqr 1521	. . . . . . . . . . . 12 |- ((y e. om /\ z = (2o .o y)) -> (z +o