Theorem nneo 4719

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

Hypothesis

Ref	Expression
nnsqcl.1	|- A e. NN

Assertion

Ref	Expression
nneo	|- ((A / 2) e. NN <-> -. ((A + 1) / 2) e. NN)

Proof of Theorem nneo

Step	Hyp	Ref	Expression
1		ax1re 4064	. . . . . . . . . 10 |- 1 e. RR
2	1	ltplus1 4384	. . . . . . . . 9 |- 1 < (1 + 1)
3		df-2 4462	. . . . . . . . 9 |- 2 = (1 + 1)
4	2, 3	breqtrr 2082	. . . . . . . 8 |- 1 < 2
5		2re 4470	. . . . . . . . 9 |- 2 e. RR
6		nnsqcl.1	. . . . . . . . . 10 |- A e. NN
7	6	nnre 4429	. . . . . . . . 9 |- A e. RR
8	1, 5, 7	ltadd2 4312	. . . . . . . 8 |- (1 < 2 <-> (A + 1) < (A + 2))
9	4, 8	mpbi 164	. . . . . . 7 |- (A + 1) < (A + 2)
10		2cn 4471	. . . . . . . 8 |- 2 e. CC
11	7, 1	readdcl 4118	. . . . . . . . 9 |- (A + 1) e. RR
12	11	recn 4098	. . . . . . . 8 |- (A + 1) e. CC
13		2pos 4479	. . . . . . . . 9 |- 0 < 2
14	5, 13	gt0ne0i 4345	. . . . . . . 8 |- 2 =/= 0
15	10, 12, 14	divcan2 4224	. . . . . . 7 |- (2 x. ((A + 1) / 2)) = (A + 1)
16	6	nncn 4430	. . . . . . . . . 10 |- A e. CC
17	16, 10, 14	divcl 4221	. . . . . . . . 9 |- (A / 2) e. CC
18		1cn 4101	. . . . . . . . 9 |- 1 e. CC
19	10, 17, 18	adddi 4110	. . . . . . . 8 |- (2 x. ((A / 2) + 1)) = ((2 x. (A / 2)) + (2 x. 1))
20	10, 16, 14	divcan2 4224	. . . . . . . . 9 |- (2 x. (A / 2)) = A
21	10	mulid1 4114	. . . . . . . . 9 |- (2 x. 1) = 2
22	20, 21	opreq12i 3011	. . . . . . . 8 |- ((2 x. (A / 2)) + (2 x. 1)) = (A + 2)
23	19, 22	eqtr 1119	. . . . . . 7 |- (2 x. ((A / 2) + 1)) = (A + 2)
24	9, 15, 23	3brtr4 2085	. . . . . 6 |- (2 x. ((A + 1) / 2)) < (2 x. ((A / 2) + 1))
25	11, 5, 14	redivcl 4274	. . . . . . . 8 |- ((A + 1) / 2) e. RR
26	7, 5, 14	redivcl 4274	. . . . . . . . 9 |- (A / 2) e. RR
27	26, 1	readdcl 4118	. . . . . . . 8 |- ((A / 2) + 1) e. RR
28	25, 27, 5	ltmul2 4395	. . . . . . 7 |- (0 < 2 -> (((A + 1) / 2) < ((A / 2) + 1) <-> (2 x. ((A + 1) / 2)) < (2 x. ((A / 2) + 1))))
29	13, 28	ax-mp 6	. . . . . 6 |- (((A + 1) / 2) < ((A / 2) + 1) <-> (2 x. ((A + 1) / 2)) < (2 x. ((A / 2) + 1)))
30	24, 29	mpbir 165	. . . . 5 |- ((A + 1) / 2) < ((A / 2) + 1)
31	27, 25	lelt 4301	. . . . . 6 |- (((A / 2) + 1) <_ ((A + 1) / 2) <-> -. ((A + 1) / 2) < ((A / 2) + 1))
32	31	bicon2i 194	. . . . 5 |- (((A + 1) / 2) < ((A / 2) + 1) <-> -. ((A / 2) + 1) <_ ((A + 1) / 2))
33	30, 32	mpbi 164	. . . 4 |- -. ((A / 2) + 1) <_ ((A + 1) / 2)
34	7	ltplus1 4384	. . . . . 6 |- A < (A + 1)
35	7, 11, 5, 13	ltdivi 4398	. . . . . 6 |- (A < (A + 1) <-> (A / 2) < ((A + 1) / 2))
36	34, 35	mpbi 164	. . . . 5 |- (A / 2) < ((A + 1) / 2)
37		nnltp1let 4449	. . . . 5 |- (((A / 2) e. NN /\ ((A + 1) / 2) e. NN) -> ((A / 2) < ((A + 1) / 2) <-> ((A / 2) + 1) <_ ((A + 1) / 2)))
38	36, 37	mpbii 168	. . . 4 |- (((A / 2) e. NN /\ ((A + 1) / 2) e. NN) -> ((A / 2) + 1) <_ ((A + 1) / 2))
39	33, 38	mto 93	. . 3 |- -. ((A / 2) e. NN /\ ((A + 1) / 2) e. NN)
40		imnan 207	. . 3 |- (((A / 2) e. NN -> -. ((A + 1) / 2) e. NN) <-> -. ((A / 2) e. NN /\ ((A + 1) / 2) e. NN))
41	39, 40	mpbir 165	. 2 |- ((A / 2) e. NN -> -. ((A + 1) / 2) e. NN)
42		opreq1 3006	. . . . . . . 8 |- (x = 1 -> (x + 1) = (1 + 1))
43	42	opreq1d 3012	. . . . . . 7 |- (x = 1 -> ((x + 1) / 2) = ((1 + 1) / 2))
44	43	eleq1d 1155	. . . . . 6 |- (x = 1 -> (((x + 1) / 2) e. NN <-> ((1 + 1) / 2) e. NN))
45		opreq1 3006	. . . . . . 7 |- (x = 1 -> (x / 2) = (1 / 2))
46	45	eleq1d 1155	. . . . . 6 |- (x = 1 -> ((x / 2) e. NN <-> (1 / 2) e. NN))
47	44, 46	orbi12d 475	. . . . 5 |- (x = 1 -> ((((x + 1) / 2) e. NN \/ (x / 2) e. NN) <-> (((1 + 1) / 2) e. NN \/ (1 / 2) e. NN)))
48		opreq1 3006	. . . . . . . 8 |- (x = y -> (x + 1) = (y + 1))
49	48	opreq1d 3012	. . . . . . 7 |- (x = y -> ((x + 1) / 2) = ((y + 1) / 2))
50	49	eleq1d 1155	. . . . . 6 |- (x = y -> (((x + 1) / 2) e. NN <-> ((y + 1) / 2) e. NN))
51		opreq1 3006	. . . . . . 7 |- (x = y -> (x / 2) = (y / 2))
52	51	eleq1d 1155	. . . . . 6 |- (x = y -> ((x / 2) e. NN <-> (y / 2) e. NN))
53	50, 52	orbi12d 475	. . . . 5 |- (x = y -> ((((x + 1) / 2) e. NN \/ (x / 2) e. NN) <-> (((y + 1) / 2) e. NN \/ (y / 2) e. NN)))
54		opreq1 3006	. . . . . . . 8 |- (x = (y + 1) -> (x + 1) = ((y + 1) + 1))
55	54	opreq1d 3012	. . . . . . 7 |- (x = (y + 1) -> ((x + 1) / 2) = (((y + 1) + 1) / 2))
56	55	eleq1d 1155	. . . . . 6 |- (x = (y + 1) -> (((x + 1) / 2) e. NN <-> (((y + 1) + 1) / 2) e. NN))
57		opreq1 3006	. . . . . . 7 |- (x = (y + 1) -> (x / 2) = ((y + 1) / 2))
58	57	eleq1d 1155	. . . . . 6 |- (x = (y + 1) -> ((x / 2) e. NN <-> ((y + 1) / 2) e. NN))
59	56, 58	orbi12d 475	. . . . 5 |- (x = (y + 1) -> ((((x + 1) / 2) e. NN \/ (x / 2) e. NN) <-> ((((y + 1) + 1) / 2) e. NN \/ ((y + 1) / 2) e. NN)))
60		opreq1 3006	. . . . . . . 8 |- (x = A -> (x + 1) = (A + 1))
61	60	opreq1d 3012	. . . . . . 7 |- (x = A -> ((x + 1) / 2) = ((A + 1) / 2))
62	61	eleq1d 1155	. . . . . 6 |- (x = A -> (((x + 1) / 2) e. NN <-> ((A + 1) / 2) e. NN))
63		opreq1 3006	. . . . . . 7 |- (x = A -> (x / 2) = (A / 2))
64	63	eleq1d 1155	. . . . . 6 |- (x = A -> ((x / 2) e. NN <-> (A / 2) e. NN))
65	62, 64	orbi12d 475	. . . . 5 |- (x = A -> ((((x + 1) / 2) e. NN \/ (x / 2) e. NN) <-> (((A + 1) / 2) e. NN \/ (A / 2) e. NN)))
66	3	opreq1i 3009	. . . . . . . . 9 |- (2 / 2) = ((1 + 1) / 2)
67	10, 14	divid 4254	. . . . . . . . 9 |- (2 / 2) = 1
68	66, 67	eqtr3 1121	. . . . . . . 8 |- ((1 + 1) / 2) = 1
69		1nn 4432	. . . . . . . 8 |- 1 e. NN
70	68, 69	eqeltr 1159	. . . . . . 7 |- ((1 + 1) / 2) e. NN
71	70	pm2.21ni 92	. . . . . 6 |- (-. ((1 + 1) / 2) e. NN -> (1 / 2) e. NN)
72	71	orri 201	. . . . 5 |- (((1 + 1) / 2) e. NN \/ (1 / 2) e. NN)
73		nncnt 4428	. . . . . . . . . 10 |- (y e. NN -> y e. CC)
74		axaddass 4072	. . . . . . . . . . . . . . 15 |- ((y e. CC /\ 1 e. CC /\ 1 e. CC) -> ((y + 1) + 1) = (y + (1 + 1)))
75	18, 74	mp3an3 641	. . . . . . . . . . . . . 14 |- ((y e. CC /\ 1 e. CC) -> ((y + 1) + 1) = (y + (1 + 1)))
76	18, 75	mpan2 519	. . . . . . . . . . . . 13 |- (y e. CC -> ((y + 1) + 1) = (y + (1 + 1)))
77	3	opreq2i 3010	. . . . . . . . . . . . 13 |- (y + 2) = (y + (1 + 1))
78	76, 77	syl6eqr 1142	. . . . . . . . . . . 12 |- (y e. CC -> ((y + 1) + 1) = (y + 2))
79	78	opreq1d 3012	. . . . . . . . . . 11 |- (y e. CC -> (((y + 1) + 1) / 2) = ((y + 2) / 2))
80		opreq1 3006	. . . . . . . . . . . . . . 15 |- (y = if(y e. CC, y, 2) -> (y + 2) = (if(y e. CC, y, 2) + 2))
81	80	opreq1d 3012	. . . . . . . . . . . . . 14 |- (y = if(y e. CC, y, 2) -> ((y + 2) / 2) = ((if(y e. CC, y, 2) + 2) / 2))
82		opreq1 3006	. . . . . . . . . . . . . . 15 |- (y = if(y e. CC, y, 2) -> (y / 2) = (if(y e. CC, y, 2) / 2))
83	82	opreq1d 3012	. . . . . . . . . . . . . 14 |- (y = if(y e. CC, y, 2) -> ((y / 2) + (2 / 2)) = ((if(y e. CC, y, 2) / 2) + (2 / 2)))
84	81, 83	cleq12d 1115	. . . . . . . . . . . . 13 |- (y = if(y e. CC, y, 2) -> (((y + 2) / 2) = ((y / 2) + (2 / 2)) <-> ((if(y e. CC, y, 2