Theorem nneob 5473

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 4987	. . . . 5 |- (x = y -> (2o .o x) = (2o .o y))
2	1	eqeq2d 2152	. . . 4 |- (x = y -> (A = (2o .o x) <-> A = (2o .o y)))
3	2	cbvrexv 2527	. . 3 |- (E.x e. om A = (2o .o x) <-> E.y e. om A = (2o .o y))
4		nnon 4092	. . . . . . . 8 |- (y e. om -> y e. On)
5		nnon 4092	. . . . . . . 8 |- (x e. om -> x e. On)
6		id 15	. . . . . . . 8 |- (A = (2o .o y) -> A = (2o .o y))
7		oneo 5423	. . . . . . . 8 |- ((y e. On /\ x e. On /\ A = (2o .o y)) -> -. suc A = (2o .o x))
8	4, 5, 6, 7	syl3an 1391	. . . . . . 7 |- ((y e. om /\ x e. om /\ A = (2o .o y)) -> -. suc A = (2o .o x))
9	8	3com23 1323	. . . . . 6 |- ((y e. om /\ A = (2o .o y) /\ x e. om) -> -. suc A = (2o .o x))
10	9	3expa 1317	. . . . 5 |- (((y e. om /\ A = (2o .o y)) /\ x e. om) -> -. suc A = (2o .o x))
11	10	nrexdv 2444	. . . 4 |- ((y e. om /\ A = (2o .o y)) -> -. E.x e. om suc A = (2o .o x))
12	11	r19.23aiva 2460	. . 3 |- (E.y e. om A = (2o .o y) -> -. E.x e. om suc A = (2o .o x))
13	3, 12	sylbi 225	. 2 |- (E.x e. om A = (2o .o x) -> -. E.x e. om suc A = (2o .o x))
14		suceq 3875	. . . . . . 7 |- (y = (/) -> suc y = suc (/))
15	14	eqeq1d 2149	. . . . . 6 |- (y = (/) -> (suc y = (2o .o x) <-> suc (/) = (2o .o x)))
16	15	rexbidv 2374	. . . . 5 |- (y = (/) -> (E.x e. om suc y = (2o .o x) <-> E.x e. om suc (/) = (2o .o x)))
17	16	notbid 746	. . . 4 |- (y = (/) -> (-. E.x e. om suc y = (2o .o x) <-> -. E.x e. om suc (/) = (2o .o x)))
18		eqeq1 2147	. . . . 5 |- (y = (/) -> (y = (2o .o x) <-> (/) = (2o .o x)))
19	18	rexbidv 2374	. . . 4 |- (y = (/) -> (E.x e. om y = (2o .o x) <-> E.x e. om (/) = (2o .o x)))
20	17, 19	imbi12d 761	. . 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 3875	. . . . . . 7 |- (y = z -> suc y = suc z)
22	21	eqeq1d 2149	. . . . . 6 |- (y = z -> (suc y = (2o .o x) <-> suc z = (2o .o x)))
23	22	rexbidv 2374	. . . . 5 |- (y = z -> (E.x e. om suc y = (2o .o x) <-> E.x e. om suc z = (2o .o x)))
24	23	notbid 746	. . . 4 |- (y = z -> (-. E.x e. om suc y = (2o .o x) <-> -. E.x e. om suc z = (2o .o x)))
25		eqeq1 2147	. . . . 5 |- (y = z -> (y = (2o .o x) <-> z = (2o .o x)))
26	25	rexbidv 2374	. . . 4 |- (y = z -> (E.x e. om y = (2o .o x) <-> E.x e. om z = (2o .o x)))
27	24, 26	imbi12d 761	. . 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 3875	. . . . . . 7 |- (y = suc z -> suc y = suc suc z)
29	28	eqeq1d 2149	. . . . . 6 |- (y = suc z -> (suc y = (2o .o x) <-> suc suc z = (2o .o x)))
30	29	rexbidv 2374	. . . . 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	notbid 746	. . . 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 2147	. . . . 5 |- (y = suc z -> (y = (2o .o x) <-> suc z = (2o .o x)))
33	32	rexbidv 2374	. . . 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 761	. . 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 3875	. . . . . . 7 |- (y = A -> suc y = suc A)
36	35	eqeq1d 2149	. . . . . 6 |- (y = A -> (suc y = (2o .o x) <-> suc A = (2o .o x)))
37	36	rexbidv 2374	. . . . 5 |- (y = A -> (E.x e. om suc y = (2o .o x) <-> E.x e. om suc A = (2o .o x)))
38	37	notbid 746	. . . 4 |- (y = A -> (-. E.x e. om suc y = (2o .o x) <-> -. E.x e. om suc A = (2o .o x)))
39		eqeq1 2147	. . . . 5 |- (y = A -> (y = (2o .o x) <-> A = (2o .o x)))
40	39	rexbidv 2374	. . . 4 |- (y = A -> (E.x e. om y = (2o .o x) <-> E.x e. om A = (2o .o x)))
41	38, 40	imbi12d 761	. . 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 4105	. . . . 5 |- (/) e. om
43		eqid 2141	. . . . 5 |- (/) = (/)
44		opreq2 4987	. . . . . . . 8 |- (x = (/) -> (2o .o x) = (2o .o (/)))
45		2on 5350	. . . . . . . . 9 |- 2o e. On
46		om0 5367	. . . . . . . . 9 |- (2o e. On -> (2o .o (/)) = (/))
47	45, 46	ax-mp 7	. . . . . . . 8 |- (2o .o (/)) = (/)
48	44, 47	syl6eq 2193	. . . . . . 7 |- (x = (/) -> (2o .o x) = (/))
49	48	eqeq2d 2152	. . . . . 6 |- (x = (/) -> ((/) = (2o .o x) <-> (/) = (/)))
50	49	rcla4ev 2620	. . . . 5 |- (((/) e. om /\ (/) = (/)) -> E.x e. om (/) = (2o .o x))
51	42, 43, 50	mp2an 681	. . . 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	1	eqeq2d 2152	. . . . . . 7 |- (x = y -> (z = (2o .o x) <-> z = (2o .o y)))
54	53	cbvrexv 2527	. . . . . 6 |- (E.x e. om z = (2o .o x) <-> E.y e. om z = (2o .o y))
55		nnon 4092	. . . . . . . . . . . . . 14 |- (z e. om -> z e. On)
56		1on 5349	. . . . . . . . . . . . . . . . 17 |- 1o e. On
57		oaass 5406	. . . . . . . . . . . . . . . . 17 |- ((z e. On /\ 1o e. On /\ 1o e. On) -> ((z +o 1o) +o 1o) = (z +o (1o +o 1o)))
58	56, 56, 57	mp3an23 1458	. . . . . . . . . . . . . . . 16 |- (z e. On -> ((z +o 1o) +o 1o) = (z +o (1o +o 1o)))
59		o1p1e2 5386	. . . . . . . . . . . . . . . . 17 |- (1o +o 1o) = 2o
60	59	opreq2i 4990	. . . . . . . . . . . . . . . 16 |- (z +o (1o +o 1o)) = (z +o 2o)
61	58, 60	syl6req 2194	. . . . . . . . . . . . . . 15 |- (z e. On -> (z +o 2o) = ((z +o 1o) +o 1o))
62		oa1suc 5375	. . . . . . . . . . . . . . . 16 |- (z e. On -> (z +o 1o) = suc z)
63	62	opreq1d 4993	. . . . . . . . . . . . . . 15 |- (z e. On -> ((z +o 1o) +o 1o) = (suc z +o 1o))
64		suceloni 4037	. . . . . . . . . . . . . . . 16 |- (z e. On -> suc z e. On)
65		oa1suc 5375	. . . . . . . . . . . . . . . 16 |- (suc z e. On -> (suc z +o 1o) = suc suc z)
66	64, 65	syl 13	. . . . . . . . . . . . . . 15 |- (z e. On -> (suc z +o 1o) = suc suc z)
67	61, 63, 66	3eqtrd 2177	. . . . . . . . . . . . . 14 |- (z e. On -> (z +o 2o) = suc suc z)
68	55, 67	syl 13	. . . . . . . . . . . . 13 |- (z e. om -> (z +o 2o) = suc suc z)
69	68	eqcomd 2146	. . . . . . . . . . . 12 |- (z e. om -> suc suc z = (z +o 2o))
70	69	ad2antrr 799	. . . . . . . . . . 11 |- (((z e. om /\ y e. om) /\ z = (2o .o y)) -> suc suc z = (z +o 2o))
71		opreq1 4986	. . . . . . . . . . . . 13 |- (z = (2o .o y) -> (z +o 2o) = ((2o .o y) +o 2o))
72		2onn 5472	. . . . . . . . . . . . . . 15 |- 2o e. om
73		1onn 5471	. . . . . . . . . . . . . . 15 |- 1o e. om
74		nndi 5456	. . . . . . . . . . . . . . 15 |- ((2o e. om /\ y e. om /\ 1o e. om) -> (2o .o (y +o 1o)) = ((2o .o y) +o (2o .o 1o)))
75	72, 73, 74	mp3an13 1457	. . . . . . . . . . . . . 14 |- (y e. om -> (2o .o (y +o 1o)) = ((2o .o y) +o (2o .o 1o)))
76		om1 5387	. . . . . . . . . . . . . . . 16 |- (2o e. On -> (2o .o 1o) = 2o)
77	45, 76	ax-mp 7	. . . . . . . . . . . . . . 15 |- (2o .o 1o) = 2o
78	77	opreq2i 4990	. . . . . . . . . . . . . 14 |- ((2o .o y) +o (2o .o 1o)) = ((2o .o y) +o 2o)
79	75, 78	syl6req 2194	. . . . . . . . . . . . 13 |- (y e. om -> ((2o .o y) +o 2o) = (2o .o (y +o 1o)))
80	71, 79	sylan9eqr 2199	. . . . . . . . . . . 12 |- ((y e. om /\ z = (2o .o y)) -> (z +o 2o) = (2o .o (y +o 1o)))
81	80	adantll 775	. . . . . . . . . . 11 |- (((z e. om /\ y e. om) /\ z = (2o .o y)) -> (z +o 2o) = (2o .o (y +o 1o)))
82	70, 81	eqtrd 2173	. . . . . . . . . 10 |- (((z e. om /\ y e. om) /\ z = (2o .o y)) -> suc suc z = (2o .o (y +o 1o)))
83	82	ex 398	. . . . . . . . 9 |- ((z e. om /\ y e. om) -> (z = (2o .o y) -> suc suc z = (2o .o (y +o 1o))))
84		nnacl 5447	. . . . . . . . . . 11 |- ((y e. om /\ 1o e. om) -> (y +o 1o) e. om)
85	73, 84	mpan2 679	. . . . . . . . . 10 |- (y e. om -> (y +o 1o) e. om)
86	85	adantl 448	. . . . . . . . 9 |- ((z e. om /\ y e. om) -> (y +o 1o) e. om)
87	83, 86	jctild 507	. . . . . . . 8 |- ((z e. om /\ y e. om) -> (z = (2o .o y) -> ((y +o 1o) e. om /\ suc suc z = (2o .o (y +o 1o)))))
88		opreq2 4987	. . . . . . . . . 10 |- (x = (y +o 1o) -> (2o .o x) = (2o .o (y +o 1o)))
89	88	eqeq2d 2152	. . . . . . . . 9 |- (x = (y +o 1o) -> (suc suc z = (2o .o x) <-> suc suc z = (2o .o (y +o 1o))))
90	89	rcla4ev 2620	. . . . . . . 8 |- (((y +o 1o) e. om /\ suc suc z = (2o .o (y +o 1o))) -> E.x e. om suc suc z = (2o .o x))
91	87, 90	syl6 42	. . . . . . 7 |- ((z e. om /\ y e. om) -> (z = (2o .o y) -> E.x e. om suc suc z = (2o .o x)))
92	91	r19.23adva 2464	. . . . . 6 |- (z e. om -> (E.y e. om z = (2o .o y) -> E.x e. om suc suc z = (2o .o x)))
93	54, 92	syl5bi 249	. . . . 5 |- (z e. om -> (E.x e. om z = (2o .o x) -> E.x e. om suc suc z = (2o .o x)))
94	93	con3d 145	. . . 4 |- (z e. om -> (-. E.x e. om suc suc z = (2o .o x) -> -. E.x e. om z = (2o .o x)))
95		con1 141	. . . 4 |- ((-. E.x e. om suc z = (2o .o x) -> E.x e. om z = (2o .o x)) -> (-. E.x e. om z = (2o .o x) -> E.x e. om suc z = (2o .o x)))
96	94, 95	syl9 57	. . 3 |- (z e. om -> ((-. E.x e. om suc z = (2o .o x) -> E.x e. om z = (2o .o x)) -> (-. E.x e. om suc suc z = (2o .o x) -> E.x e. om suc z = (2o .o x))))
97	20, 27, 34, 41, 52, 96	finds 4112	. 2 |- (A e. om -> (-. E.x e. om suc A = (2o .o x) -> E.x e. om A = (2o .o x)))
98	13, 97	impbid2 237	1 |- (A e. om -> (E.x e. om A = (2o .o x) <-> -. E.x e. om suc A = (2o .o x)))

Syntax hints:  -. wn 2   -> wi 3   <-> wb 219   /\ wa 337   = wceq 1586   e. wcel 1588  E.wrex 2356  (/)c0 3082  Oncon0 3811  suc csuc 3813  omcom 4085  (class class class)co 4981  1oc1o 5339  2oc2o 5340   +o coa 5341   .o comu 5342

This theorem was proved from axioms:  ax-1 4  ax-2 5  ax-3 6  ax-mp 7  ax-7 1592  ax-gen 1593  ax-8 1594  ax-9 1595  ax-10 1596  ax-11 1597  ax-12 1598  ax-13 1599  ax-14 1600  ax-17 1605  ax-4 1608  ax-5o 1610  ax-6o 1613  ax-9o 1763  ax-10o 1781  ax-16 1854  ax-11o 1864  ax-ext 2123  ax-rep 3596  ax-sep 3606  ax-nul 3613  ax-pow 3649  ax-pr 3687  ax-un 3929

This theorem depends on definitions:  df-bi 220  df-or 338  df-an 339  df-3or 1103  df-3an 1104  df-ex 1616  df-sb 1816  df-eu 2041  df-mo 2042  df-clab 2129  df-cleq 2134  df-clel 2137  df-ne 2268  df-ral 2359  df-rex 2360  df-reu 2361  df-rab 2362  df-v 2540  df-sbc 2700  df-csb 2774  df-dif 2830  df-un 2832  df-in 2834  df-ss 2836  df-pss 2838  df-nul 3083  df-if 3181  df-pw 3229  df-sn 3242  df-pr 3243  df-tp 3245  df-op 3246  df-uni 3367  df-int 3401  df-iun 3438  df-br 3508  df-opab 3566  df-tr 3580  df-eprel 3744  df-id 3747  df-po 3752  df-so 3764  df-fr 3782  df-we 3798  df-ord 3814  df-on 3815  df-lim 3816  df-suc 3817  df-om 4086  df-xp 4133  df-rel 4134  df-cnv 4135  df-co 4136  df-dm 4137  df-rn 4138  df-res 4139  df-ima 4140  df-fun 4141  df-fn 4142  df-fv 4147  df-opr 4983  df-oprab 4984  df-rdg 5304  df-1o 5344  df-2o 5345  df-oadd 5346  df-omul 5347

Copyright terms: Public domain