Theorem nnesq 6662

Description: A natural number is even iff its square is even.

Hypothesis

Ref	Expression
nnsqcl.1	|- N e. NN

Assertion

Ref	Expression
nnesq	|- ((N / 2) e. NN <-> ((N^2) / 2) e. NN)

Proof of Theorem nnesq

Step	Hyp	Ref	Expression
1		nnmulclt 5941	. . . 4 |- (((N / 2) e. NN /\ (N / 2) e. NN) -> ((N / 2) x. (N / 2)) e. NN)
2	1	anidms 434	. . 3 |- ((N / 2) e. NN -> ((N / 2) x. (N / 2)) e. NN)
3		2nn 5999	. . . . 5 |- 2 e. NN
4		nnmulclt 5941	. . . . 5 |- ((2 e. NN /\ ((N / 2) x. (N / 2)) e. NN) -> (2 x. ((N / 2) x. (N / 2))) e. NN)
5	3, 4	mpan 695	. . . 4 |- (((N / 2) x. (N / 2)) e. NN -> (2 x. ((N / 2) x. (N / 2))) e. NN)
6		2cn 5980	. . . . . 6 |- 2 e. CC
7		nnsqcl.1	. . . . . . . 8 |- N e. NN
8	7	nncn 5932	. . . . . . 7 |- N e. CC
9		2ne0 5990	. . . . . . 7 |- 2 =/= 0
10	8, 6, 9	divcl 5710	. . . . . 6 |- (N / 2) e. CC
11	6, 10, 10	mulass 5325	. . . . 5 |- ((2 x. (N / 2)) x. (N / 2)) = (2 x. ((N / 2) x. (N / 2)))
12	8, 8, 6, 9	divass 5746	. . . . . 6 |- ((N x. N) / 2) = (N x. (N / 2))
13	8	sqval 6614	. . . . . . 7 |- (N^2) = (N x. N)
14	13	opreq1i 3971	. . . . . 6 |- ((N^2) / 2) = ((N x. N) / 2)
15	8, 6, 9	divcan2 5716	. . . . . . 7 |- (2 x. (N / 2)) = N
16	15	opreq1i 3971	. . . . . 6 |- ((2 x. (N / 2)) x. (N / 2)) = (N x. (N / 2))
17	12, 14, 16	3eqtr4r 1506	. . . . 5 |- ((2 x. (N / 2)) x. (N / 2)) = ((N^2) / 2)
18	11, 17	eqtr3 1497	. . . 4 |- (2 x. ((N / 2) x. (N / 2))) = ((N^2) / 2)
19	5, 18	syl5eqelr 1553	. . 3 |- (((N / 2) x. (N / 2)) e. NN -> ((N^2) / 2) e. NN)
20	2, 19	syl 10	. 2 |- ((N / 2) e. NN -> ((N^2) / 2) e. NN)
21		nnmulclt 5941	. . . . . 6 |- ((((N + 1) / 2) e. NN /\ ((N + 1) / 2) e. NN) -> (((N + 1) / 2) x. ((N + 1) / 2)) e. NN)
22	21	anidms 434	. . . . 5 |- (((N + 1) / 2) e. NN -> (((N + 1) / 2) x. ((N + 1) / 2)) e. NN)
23		nnmulclt 5941	. . . . . 6 |- ((2 e. NN /\ (((N + 1) / 2) x. ((N + 1) / 2)) e. NN) -> (2 x. (((N + 1) / 2) x. ((N + 1) / 2))) e. NN)
24	3, 23	mpan 695	. . . . 5 |- ((((N + 1) / 2) x. ((N + 1) / 2)) e. NN -> (2 x. (((N + 1) / 2) x. ((N + 1) / 2))) e. NN)
25		ax1cn 5269	. . . . . . . . . . 11 |- 1 e. CC
26	8, 25	addcl 5320	. . . . . . . . . 10 |- (N + 1) e. CC
27	26, 6, 9	divcan2 5716	. . . . . . . . 9 |- (2 x. ((N + 1) / 2)) = (N + 1)
28	27	opreq1i 3971	. . . . . . . 8 |- ((2 x. ((N + 1) / 2)) x. ((N + 1) / 2)) = ((N + 1) x. ((N + 1) / 2))
29	26, 6, 9	divcl 5710	. . . . . . . . 9 |- ((N + 1) / 2) e. CC
30	6, 29, 29	mulass 5325	. . . . . . . 8 |- ((2 x. ((N + 1) / 2)) x. ((N + 1) / 2)) = (2 x. (((N + 1) / 2) x. ((N + 1) / 2)))
31	26, 26, 6, 9	divass 5746	. . . . . . . . 9 |- (((N + 1) x. (N + 1)) / 2) = ((N + 1) x. ((N + 1) / 2))
32	26	sqval 6614	. . . . . . . . . . . 12 |- ((N + 1)^2) = ((N + 1) x. (N + 1))
33	8, 25	binom2 6644	. . . . . . . . . . . . 13 |- ((N + 1)^2) = (((N^2) + (2 x. (N x. 1))) + (1^2))
34	8	mulid1 5332	. . . . . . . . . . . . . . . 16 |- (N x. 1) = N
35	34	opreq2i 3972	. . . . . . . . . . . . . . 15 |- (2 x. (N x. 1)) = (2 x. N)
36	35	opreq2i 3972	. . . . . . . . . . . . . 14 |- ((N^2) + (2 x. (N x. 1))) = ((N^2) + (2 x. N))
37		sq1 6637	. . . . . . . . . . . . . 14 |- (1^2) = 1
38	36, 37	opreq12i 3973	. . . . . . . . . . . . 13 |- (((N^2) + (2 x. (N x. 1))) + (1^2)) = (((N^2) + (2 x. N)) + 1)
39	7	nnsqcl 6660	. . . . . . . . . . . . . . 15 |- (N^2) e. NN
40	39	nncn 5932	. . . . . . . . . . . . . 14 |- (N^2) e. CC
41	6, 8	mulcl 5321	. . . . . . . . . . . . . 14 |- (2 x. N) e. CC
42	40, 41, 25	add23 5341	. . . . . . . . . . . . 13 |- (((N^2) + (2 x. N)) + 1) = (((N^2) + 1) + (2 x. N))
43	33, 38, 42	3eqtr 1499	. . . . . . . . . . . 12 |- ((N + 1)^2) = (((N^2) + 1) + (2 x. N))
44	32, 43	eqtr3 1497	. . . . . . . . . . 11 |- ((N + 1) x. (N + 1)) = (((N^2) + 1) + (2 x. N))
45	44	opreq1i 3971	. . . . . . . . . 10 |- (((N + 1) x. (N + 1)) / 2) = ((((N^2) + 1) + (2 x. N)) / 2)
46	39	nnre 5931	. . . . . . . . . . . . 13 |- (N^2) e. RR
47		1re 5435	. . . . . . . . . . . . 13 |- 1 e. RR
48	46, 47	readdcl 5334	. . . . . . . . . . . 12 |- ((N^2) + 1) e. RR
49	48	recn 5314	. . . . . . . . . . 11 |- ((N^2) + 1) e. CC
50	49, 41, 6, 9	divdir 5747	. . . . . . . . . 10 |- ((((N^2) + 1) + (2 x. N)) / 2) = ((((N^2) + 1) / 2) + ((2 x. N) / 2))
51	8, 6, 9	divcan3 5752	. . . . . . . . . . 11 |- ((2 x. N) / 2) = N
52	51	opreq2i 3972	. . . . . . . . . 10 |- ((((N^2) + 1) / 2) + ((2 x. N) / 2)) = ((((N^2) + 1) / 2) + N)
53	45, 50, 52	3eqtr 1499	. . . . . . . . 9 |- (((N + 1) x. (N + 1)) / 2) = ((((N^2) + 1) / 2) + N)
54	31, 53	eqtr3 1497	. . . . . . . 8 |- ((N + 1) x. ((N + 1) / 2)) = ((((N^2) + 1) / 2) + N)
55	28, 30, 54	3eqtr3 1503	. . . . . . 7 |- (2 x. (((N + 1) / 2) x. ((N + 1) / 2))) = ((((N^2) + 1) / 2) + N)
56	55	eleq1i 1537	. . . . . 6 |- ((2 x. (((N + 1) / 2) x. ((N + 1) / 2))) e. NN <-> ((((N^2) + 1) / 2) + N) e. NN)
57	8	addid2 5331	. . . . . . . . 9 |- (0 + N) = N
58		2re 5979	. . . . . . . . . . 11 |- 2 e. RR
59	39	nngt0 5950	. . . . . . . . . . . 12 |- 0 < (N^2)
60		lt01 5680	. . . . . . . . . . . 12 |- 0 < 1
61	46, 47, 59, 60	addgt0i 5601	. . . . . . . . . . 11 |- 0 < ((N^2) + 1)
62		2pos 5989	. . . . . . . . . . 11 |- 0 < 2
63	48, 58, 61, 62	divgt0i 5860	. . . . . . . . . 10 |- 0 < (((N^2) + 1) / 2)
64		0re 5440	. . . . . . . . . . 11 |- 0 e. RR
65	48, 58, 9	redivcl 5798	. . . . . . . . . . 11 |- (((N^2) + 1) / 2) e. RR
66	7	nnre 5931	. . . . . . . . . . 11 |- N e. RR
67	64, 65, 66	ltadd1 5591	. . . . . . . . . 10 |- (0 < (((N^2) + 1) / 2) <-> (0 + N) < ((((N^2) + 1) / 2) + N))
68	63, 67	mpbi 189	. . . . . . . . 9 |- (0 + N) < ((((N^2) + 1) / 2) + N)
69	57, 68	eqbrtrr 2636	. . . . . . . 8 |- N < ((((N^2) + 1) / 2) + N)
70		nnsubt 5957	. . . . . . . . 9 |- ((N e. NN /\ ((((N^2) + 1) / 2) + N) e. NN) -> (N < ((((N^2) + 1) / 2) + N) <-> (((((N^2) + 1) / 2) + N) - N) e. NN))
71	7, 70	mpan 695	. . . . . . . 8 |- (((((N^2) + 1) / 2) + N) e. NN -> (N < ((((N^2) + 1) / 2) + N) <-> (((((N^2) + 1) / 2) + N) - N) e. NN))
72	69, 71	mpbii 193	. . . . . . 7 |- (((((N^2) + 1) / 2) + N) e. NN -> (((((N^2) + 1) / 2) + N) - N) e. NN)
73	65	recn 5314	. . . . . . . . 9 |- (((N^2) + 1) / 2) e. CC
74	73, 8, 8	addsubass 5387	. . . . . . . 8 |- (((((N^2) + 1) / 2) + N) - N) = ((((N^2) + 1) / 2) + (N - N))
75	8	subid 5391	. . . . . . . . 9 |- (N - N) = 0
76	75	opreq2i 3972	. . . . . . . 8 |- ((((N^2) + 1) / 2) + (N - N)) = ((((N^2) + 1) / 2) + 0)
77	73	addid1 5330	. . . . . . . 8 |- ((((N^2) + 1) / 2) + 0) = (((N^2) + 1) / 2)
78	74, 76, 77	3eqtr 1499	. . . . . . 7 |- (((((N^2) + 1) / 2) + N) - N) = (((N^2