Theorem zeot 6154

Description: An integer is even or odd.

Assertion

Ref	Expression
zeot	|- (N e. ZZ -> ((N / 2) e. ZZ \/ ((N + 1) / 2) e. ZZ))

Proof of Theorem zeot

Step	Hyp	Ref	Expression
1		elz 6092	. . 3 |- (N e. ZZ <-> (N e. RR /\ (N = 0 \/ N e. NN \/ -uN e. NN)))
2		opreq1 3959	. . . . . . 7 |- (N = 0 -> (N / 2) = (0 / 2))
3		2cn 5935	. . . . . . . . 9 |- 2 e. CC
4		2ne0 5945	. . . . . . . . 9 |- 2 =/= 0
5	3, 4	div0 5735	. . . . . . . 8 |- (0 / 2) = 0
6		0z 6101	. . . . . . . 8 |- 0 e. ZZ
7	5, 6	eqeltr 1541	. . . . . . 7 |- (0 / 2) e. ZZ
8	2, 7	syl6eqel 1553	. . . . . 6 |- (N = 0 -> (N / 2) e. ZZ)
9	8	pm2.24d 105	. . . . 5 |- (N = 0 -> (-. (N / 2) e. ZZ -> ((N + 1) / 2) e. ZZ))
10	9	adantl 388	. . . 4 |- ((N e. RR /\ N = 0) -> (-. (N / 2) e. ZZ -> ((N + 1) / 2) e. ZZ))
11		nneot 6153	. . . . . . . . 9 |- (N e. NN -> ((N / 2) e. NN <-> -. ((N + 1) / 2) e. NN))
12	11	biimprd 154	. . . . . . . 8 |- (N e. NN -> (-. ((N + 1) / 2) e. NN -> (N / 2) e. NN))
13	12	con1d 93	. . . . . . 7 |- (N e. NN -> (-. (N / 2) e. NN -> ((N + 1) / 2) e. NN))
14		nnzt 6108	. . . . . . . 8 |- ((N / 2) e. NN -> (N / 2) e. ZZ)
15	14	con3i 98	. . . . . . 7 |- (-. (N / 2) e. ZZ -> -. (N / 2) e. NN)
16	13, 15	syl5 21	. . . . . 6 |- (N e. NN -> (-. (N / 2) e. ZZ -> ((N + 1) / 2) e. NN))
17		nnzt 6108	. . . . . 6 |- (((N + 1) / 2) e. NN -> ((N + 1) / 2) e. ZZ)
18	16, 17	syl6 22	. . . . 5 |- (N e. NN -> (-. (N / 2) e. ZZ -> ((N + 1) / 2) e. ZZ))
19	18	adantl 388	. . . 4 |- ((N e. RR /\ N e. NN) -> (-. (N / 2) e. ZZ -> ((N + 1) / 2) e. ZZ))
20		recnt 5293	. . . . . . . . . . 11 |- (N e. RR -> N e. CC)
21		divnegt 5738	. . . . . . . . . . . 12 |- ((N e. CC /\ 2 e. CC /\ 2 =/= 0) -> -u(N / 2) = (-uN / 2))
22	3, 4, 21	mp3an23 906	. . . . . . . . . . 11 |- (N e. CC -> -u(N / 2) = (-uN / 2))
23	20, 22	syl 10	. . . . . . . . . 10 |- (N e. RR -> -u(N / 2) = (-uN / 2))
24	23	eleq1d 1537	. . . . . . . . 9 |- (N e. RR -> (-u(N / 2) e. NN <-> (-uN / 2) e. NN))
25		nnnegz 6093	. . . . . . . . 9 |- (-u(N / 2) e. NN -> -u-u(N / 2) e. ZZ)
26	24, 25	syl6bir 215	. . . . . . . 8 |- (N e. RR -> ((-uN / 2) e. NN -> -u-u(N / 2) e. ZZ))
27		halfclt 5988	. . . . . . . . . 10 |- (N e. CC -> (N / 2) e. CC)
28		negnegt 5373	. . . . . . . . . 10 |- ((N / 2) e. CC -> -u-u(N / 2) = (N / 2))
29	20, 27, 28	3syl 20	. . . . . . . . 9 |- (N e. RR -> -u-u(N / 2) = (N / 2))
30	29	eleq1d 1537	. . . . . . . 8 |- (N e. RR -> (-u-u(N / 2) e. ZZ <-> (N / 2) e. ZZ))
31	26, 30	sylibd 202	. . . . . . 7 |- (N e. RR -> ((-uN / 2) e. NN -> (N / 2) e. ZZ))
32	31	adantr 389	. . . . . 6 |- ((N e. RR /\ -uN e. NN) -> ((-uN / 2) e. NN -> (N / 2) e. ZZ))
33	32	con3d 95	. . . . 5 |- ((N e. RR /\ -uN e. NN) -> (-. (N / 2) e. ZZ -> -. (-uN / 2) e. NN))
34		nneot 6153	. . . . . . . 8 |- (-uN e. NN -> ((-uN / 2) e. NN <-> -. ((-uN + 1) / 2) e. NN))
35	34	biimprd 154	. . . . . . 7 |- (-uN e. NN -> (-. ((-uN + 1) / 2) e. NN -> (-uN / 2) e. NN))
36	35	con1d 93	. . . . . 6 |- (-uN e. NN -> (-. (-uN / 2) e. NN -> ((-uN + 1) / 2) e. NN))
37		ax1cn 5249	. . . . . . . . . . . . . . . . . . 19 |- 1 e. CC
38	37, 3	negsubdi2 5430	. . . . . . . . . . . . . . . . . 18 |- -u(1 - 2) = (2 - 1)
39		df-2 5925	. . . . . . . . . . . . . . . . . . . 20 |- 2 = (1 + 1)
40	39	eqcomi 1476	. . . . . . . . . . . . . . . . . . 19 |- (1 + 1) = 2
41	3, 37, 37, 40	subaddri 5352	. . . . . . . . . . . . . . . . . 18 |- (2 - 1) = 1
42	38, 41	eqtr2 1493	. . . . . . . . . . . . . . . . 17 |- 1 = -u(1 - 2)
43	37, 3	subcl 5346	. . . . . . . . . . . . . . . . . 18 |- (1 - 2) e. CC
44	37, 43	negcon2 5388	. . . . . . . . . . . . . . . . 17 |- (1 = -u(1 - 2) <-> (1 - 2) = -u1)
45	42, 44	mpbi 189	. . . . . . . . . . . . . . . 16 |- (1 - 2) = -u1
46	45	opreq2i 3963	. . . . . . . . . . . . . . 15 |- (-uN + (1 - 2)) = (-uN + -u1)
47		negclt 5348	. . . . . . . . . . . . . . . 16 |- (N e. CC -> -uN e. CC)
48		addsubasst 5363	. . . . . . . . . . . . . . . . 17 |- ((-uN e. CC /\ 1 e. CC /\ 2 e. CC) -> ((-uN + 1) - 2) = (-uN + (1 - 2)))
49	37, 3, 48	mp3an23 906	. . . . . . . . . . . . . . . 16 |- (-uN e. CC -> ((-uN + 1) - 2) = (-uN + (1 - 2)))
50	47, 49	syl 10	. . . . . . . . . . . . . . 15 |- (N e. CC -> ((-uN + 1) - 2) = (-uN + (1 - 2)))
51		negdit 5435	. . . . . . . . . . . . . . . 16 |- ((N e. CC /\ 1 e. CC) -> -u(N + 1) = (-uN + -u1))
52	37, 51	mpan2 695	. . . . . . . . . . . . . . 15 |- (N e. CC -> -u(N + 1) = (-uN + -u1))
53	46, 50, 52	3eqtr4a 1529	. . . . . . . . . . . . . 14 |- (N e. CC -> ((-uN + 1) - 2) = -u(N + 1))
54	53	opreq1d 3966	. . . . . . . . . . . . 13 |- (N e. CC -> (((-uN + 1) - 2) / 2) = (-u(N + 1) / 2))
55		peano2cn 5324	. . . . . . . . . . . . . . 15 |- (-uN e. CC -> (-uN + 1) e. CC)
56		divsubdirt 5739	. . . . . . . . . . . . . . . . 17 |- ((((-uN + 1) e. CC /\ 2 e. CC /\ 2 e. CC) /\ 2 =/= 0) -> (((-uN + 1) - 2) / 2) = (((-uN + 1) / 2) - (2 / 2)))
57	4, 56	mpan2 695	. . . . . . . . . . . . . . . 16 |- (((-uN + 1) e. CC /\ 2 e. CC /\ 2 e. CC) -> (((-uN + 1) - 2) / 2) = (((-uN + 1) / 2) - (2 / 2)))
58	3, 3, 57	mp3an23 906	. . . . . . . . . . . . . . 15 |- ((-uN + 1) e. CC -> (((-uN + 1) - 2) / 2) = (((-uN + 1) / 2) - (2 / 2)))
59	47, 55, 58	3syl 20	. . . . . . . . . . . . . 14 |- (N e. CC -> (((-uN + 1) - 2) / 2) = (((-uN + 1) / 2) - (2 / 2)))
60	3, 4	divid 5734	. . . . . . . . . . . . . . . 16 |- (2 / 2) = 1
61	60	eqcomi 1476	. . . . . . . . . . . . . . 15 |- 1 = (2 / 2)
62	61	opreq2i 3963	. . . . . . . . . . . . . 14 |- (((-uN + 1) / 2) - 1) = (((-uN + 1) / 2) - (2 / 2))
63	59, 62	syl6reqr 1523	. . . . . . . . . . . . 13 |- (N e. CC -> (((-uN + 1) / 2) - 1) = (((-uN + 1) - 2) / 2))
64		peano2cn 5324	. . . . . . . . . . . . . 14 |- (N e. CC -> (N + 1) e. CC)
65		divnegt 5738	. . . . . . . . . . . . . . 15 |- (((N + 1) e. CC /\ 2 e. CC /\ 2 =/= 0) -> -u((N + 1) / 2) = (-u(N + 1) / 2))
66	3, 4, 65	mp3an23 906	. . . . . . . . . . . . . 14 |- ((N + 1) e. CC -> -u((N + 1) / 2) = (-u(N + 1) / 2))
67	64, 66	syl 10	. . . . . . . . . . . . 13 |- (N e. CC -> -u((N + 1) / 2) = (-u(N + 1) / 2))
68	54, 63, 67	3eqtr4d 1514	. . . . . . . . . . . 12 |- (N e. CC -> (((-uN + 1) / 2) - 1) = -u((N + 1) / 2))
69	20, 68	syl 10	. . . . . . . . . . 11 |- (N e. RR -> (((-uN + 1) / 2) - 1) = -u((N + 1) / 2))
70	69	eleq1d 1537	. . . . . . . . . 10 |- (N e. RR -> ((((-uN + 1) / 2) - 1) e. ZZ <-> -u((N + 1) / 2) e. ZZ))
71		peano2zm 6124	. . . . . . . . . 10 |- (((-uN + 1) / 2) e. ZZ -> (((-uN + 1) / 2) - 1) e. ZZ)
72	70, 71	syl5bi 208	. . . . . . . . 9 |- (N e. RR -> (((-uN + 1) / 2) e. ZZ -> -u((N + 1) / 2) e. ZZ))
73		znegclt 6118	. . . . . . . . 9 |- (-u((N + 1) / 2) e. ZZ -> -u-u((N + 1) / 2) e. ZZ)
74	72, 73	syl6 22	. . . . . . . 8 |- (N e. RR -> (((-uN + 1) / 2) e. ZZ -> -u-u((N + 1) / 2) e. ZZ))
75		peano2re 5416	. . . . . . . . . . 11 |- (N e. RR -> (N + 1) e. RR)
76	75	recnd 5295	. . . . . . . . . 10 |- (N e. RR -> (N + 1) e. CC)
77		halfclt 5988	. . . . . . . . . 10 |- ((N + 1) e. CC -> ((N + 1) / 2) e. CC)
78		negnegt 5373	. . . . . . . . . 10 |- (((N + 1) / 2) e. CC -> -u-u((N + 1) / 2) = ((N + 1) / 2))
79	76, 77, 78	3syl 20	. . . . . . . . 9 |- (N e. RR -> -u-u((N + 1) / 2) = ((N + 1) / 2