Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem nneob 4239

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

Assertion

Ref	Expression
nneob

Distinct variable group:   ,

---

Proof of Theorem nneob

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