Home

Metamath Proof Explorer

< Previous   Next > Related theorems Unicode version

---

Theorem nneo 6144

Description: A natural number is even or odd but not both.

Hypothesis

Ref	Expression
nneo.1

Assertion

Ref	Expression
nneo

---

Proof of Theorem nneo

Step	Hyp	Ref	Expression
1		1lt2 5975	. . . . . . . 8
2		1re 5407	. . . . . . . . 9
3		2re 5926	. . . . . . . . 9
4		nneo.1	. . . . . . . . . 10
5	4	nnre 5879	. . . . . . . . 9
6	2, 3, 5	ltadd2 5564	. . . . . . . 8
7	1, 6	mpbi 189	. . . . . . 7
8		2cn 5927	. . . . . . . 8
9	5, 2	readdcl 5306	. . . . . . . . 9
10	9	recn 5286	. . . . . . . 8
11		2ne0 5937	. . . . . . . 8
12	8, 10, 11	divcan2 5685	. . . . . . 7
13	5, 3, 11	redivcl 5754	. . . . . . . . . 10
14	13	recn 5286	. . . . . . . . 9
15		ax1cn 5241	. . . . . . . . 9
16	8, 14, 15	adddi 5298	. . . . . . . 8
17	4	nncn 5880	. . . . . . . . . 10
18	8, 17, 11	divcan2 5685	. . . . . . . . 9
19	8	mulid1 5304	. . . . . . . . 9
20	18, 19	opreq12i 3958	. . . . . . . 8
21	16, 20	eqtr 1487	. . . . . . 7
22	7, 12, 21	3brtr4 2633	. . . . . 6
23		2pos 5936	. . . . . . 7
24	9, 3, 11	redivcl 5754	. . . . . . . 8
25	13, 2	readdcl 5306	. . . . . . . 8
26	24, 25, 3	ltmul2 5790	. . . . . . 7
27	23, 26	ax-mp 7	. . . . . 6
28	22, 27	mpbir 190	. . . . 5
29	24, 25	ltnle 5552	. . . . 5
30	28, 29	mpbi 189	. . . 4
31	5	ltp1 5769	. . . . . 6
32	5, 9, 3, 23	ltdiv1i 5779	. . . . . 6
33	31, 32	mpbi 189	. . . . 5
34		nnltp1let 5902	. . . . 5
35	33, 34	mpbii 193	. . . 4
36	30, 35	mto 106	. . 3
37		imnan 242	. . 3
38	36, 37	mpbir 190	. 2
39		opreq1 3953	. . . . . . . 8
40	39	opreq1d 3960	. . . . . . 7
41	40	eleq1d 1532	. . . . . 6
42		opreq1 3953	. . . . . . 7
43	42	eleq1d 1532	. . . . . 6
44	41, 43	orbi12d 625	. . . . 5
45		opreq1 3953	. . . . . . . 8
46	45	opreq1d 3960	. . . . . . 7
47	46	eleq1d 1532	. . . . . 6
48		opreq1 3953	. . . . . . 7
49	48	eleq1d 1532	. . . . . 6
50	47, 49	orbi12d 625	. . . . 5
51		opreq1 3953	. . . . . . . 8
52	51	opreq1d 3960	. . . . . . 7
53	52	eleq1d 1532	. . . . . 6
54		opreq1 3953	. . . . . . 7
55	54	eleq1d 1532	. . . . . 6
56	53, 55	orbi12d 625	. . . . 5
57		opreq1 3953	. . . . . . . 8
58	57	opreq1d 3960	. . . . . . 7
59	58	eleq1d 1532	. . . . . 6
60		opreq1 3953	. . . . . . 7
61	60	eleq1d 1532	. . . . . 6
62	59, 61	orbi12d 625	. . . . 5
63		df-2 5917	. . . . . . . . 9
64	63	opreq1i 3956	. . . . . . . 8
65	8, 11	divid 5726	. . . . . . . 8
66	64, 65	eqtr3 1489	. . . . . . 7
67		1nn 5882	. . . . . . 7
68	66, 67	eqeltr 1536	. . . . . 6
69	68	orci 270	. . . . 5
70		nncnt 5878	. . . . . . . . . 10
71		axaddass 5249	. . . . . . . . . . . . . 14
72	15, 15, 71	mp3an23 905	. . . . . . . . . . . . 13
73	63	opreq2i 3957	. . . . . . . . . . . . 13
74	72, 73	syl6eqr 1517	. . . . . . . . . . . 12
75	74	opreq1d 3960	. . . . . . . . . . 11
76		divdirt 5713	. . . . . . . . . . . . . 14
77	11, 76	mpan2 694	. . . . . . . . . . . . 13
78	8, 8, 77	mp3an23 905	. . . . . . . . . . . 12
79	65	opreq2i 3957	. . . . . . . . . . . 12
80	78, 79	syl6eq 1515	. . . . . . . . . . 11
81	75, 80	eqtrd 1499	. . . . . . . . . 10
82	70, 81	syl 10	. . . . . . . . 9
83	82	eleq1d 1532	. . . . . . . 8