Theorem nnesq 6663

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 5943	. . . 4 |- (((N / 2) e. NN /\ (N / 2) e. NN) -> ((N / 2) x. (N / 2)) e. NN)
2	1	anidms 436	. . 3 |- ((N / 2) e. NN -> ((N / 2) x. (N / 2)) e. NN)
3		2nn 6001	. . . . 5 |- 2 e. NN
4		nnmulclt 5943	. . . . 5 |- ((2 e. NN /\ ((N / 2) x. (N / 2)) e. NN) -> (2 x. ((N / 2) x. (N / 2))) e. NN)
5	3, 4	mpan 697	. . . 4 |- (((N / 2) x. (N / 2)) e. NN -> (2 x. ((N / 2) x. (N / 2))) e. NN)
6		2cn 5982	. . . . . 6 |- 2 e. CC
7		nnsqcl.1	. . . . . . . 8 |- N e. NN
8	7	nncn 5934	. . . . . . 7 |- N e. CC
9		2ne0 5992	. . . . . . 7 |- 2 =/= 0
10	8, 6, 9	divcl 5722	. . . . . 6 |- (N / 2) e. CC
11	6, 10, 10	mulass 5337	. . . . 5 |- ((2 x. (N / 2)) x. (N / 2)) = (2 x. ((N / 2) x. (N / 2)))
12	8, 8, 6, 9	divass 5753	. . . . . 6 |- ((N x. N) / 2) = (N x. (N / 2))
13	8	sqval 6615	. . . . . . 7 |- (N^2) = (N x. N)
14	13	opreq1i 3977	. . . . . 6 |- ((N^2) / 2) = ((N x. N) / 2)
15	8, 6, 9	divcan2 5728	. . . . . . 7 |- (2 x. (N / 2)) = N
16	15	opreq1i 3977	. . . . . 6 |- ((2 x. (N / 2)) x. (N / 2)) = (N x. (N / 2))
17	12, 14, 16	3eqtr4r 1509	. . . . 5 |- ((2 x. (N / 2)) x. (N / 2)) = ((N^2) / 2)
18	11, 17	eqtr3 1500	. . . 4 |- (2 x. ((N / 2) x. (N / 2))) = ((N^2) / 2)
19	5, 18	syl5eqelr 1556	. . 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 5943	. . . . . 6 |- ((((N + 1) / 2) e. NN /\ ((N + 1) / 2) e. NN) -> (((N + 1) / 2) x. ((N + 1) / 2)) e. NN)
22	21	anidms 436	. . . . 5 |- (((N + 1) / 2) e. NN -> (((N + 1) / 2) x. ((N + 1) / 2)) e. NN)
23		nnmulclt 5943	. . . . . 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 697	. . . . 5 |- ((((N + 1) / 2) x. ((N + 1) / 2)) e. NN -> (2 x. (((N + 1) / 2) x. ((N + 1) / 2))) e. NN)
25		ax1cn 5281	. . . . . . . . . . 11 |- 1 e. CC
26	8, 25	addcl 5332	. . . . . . . . . 10 |- (N + 1) e. CC
27	26, 6, 9	divcan2 5728	. . . . . . . . 9 |- (2 x. ((N + 1) / 2)) = (N + 1)
28	27	opreq1i 3977	. . . . . . . 8 |- ((2 x. ((N + 1) / 2)) x. ((N + 1) / 2)) = ((N + 1) x. ((N + 1) / 2))
29	26, 6, 9	divcl 5722	. . . . . . . . 9 |- ((N + 1) / 2) e. CC
30	6, 29, 29	mulass 5337	. . . . . . . 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 5753	. . . . . . . . 9 |- (((N + 1) x. (N + 1)) / 2) = ((N + 1) x. ((N + 1) / 2))
32	26	sqval 6615	. . . . . . . . . . . 12 |- ((N + 1)^2) = ((N + 1) x. (N + 1))
33	8, 25	binom2 6645	. . . . . . . . . . . . 13 |- ((N + 1)^2) = (((N^2) + (2 x. (N x. 1))) + (1^2))
34	8	mulid1 5344	. . . . . . . . . . . . . . . 16 |- (N x. 1) = N
35	34	opreq2i 3978	. . . . . . . . . . . . . . 15 |- (2 x. (N x. 1)) = (2 x. N)
36	35	opreq2i 3978	. . . . . . . . . . . . . 14 |- ((N^2) + (2 x. (N x. 1))) = ((N^2) + (2 x. N))
37		sq1 6638	. . . . . . . . . . . . . 14 |- (1^2) = 1
38	36, 37	opreq12i 3979	. . . . . . . . . . . . 13 |- (((N^2) + (2 x. (N x. 1))) + (1^2)) = (((N^2) + (2 x. N)) + 1)
39	7	nnsqcl 6661	. . . . . . . . . . . . . . 15 |- (N^2) e. NN
40	39	nncn 5934	. . . . . . . . . . . . . 14 |- (N^2) e. CC
41	6, 8	mulcl 5333	. . . . . . . . . . . . . 14 |- (2 x. N) e. CC
42	40, 41, 25	add23 5353	. . . . . . . . . . . . 13 |- (((N^2) + (2 x. N)) + 1) = (((N^2) + 1) + (2 x. N))
43	33, 38, 42	3eqtr 1502	. . . . . . . . . . . 12 |- ((N + 1)^2) = (((N^2) + 1) + (2 x. N))
44	32, 43	eqtr3 1500	. . . . . . . . . . 11 |- ((N + 1) x. (N + 1)) = (((N^2) + 1) + (2 x. N))
45	44	opreq1i 3977	. . . . . . . . . 10 |- (((N + 1) x. (N + 1)) / 2) = ((((N^2) + 1) + (2 x. N)) / 2)
46	39	nnre 5933	. . . . . . . . . . . . 13 |- (N^2) e. RR
47		1re 5447	. . . . . . . . . . . . 13 |- 1 e. RR
48	46, 47	readdcl 5346	. . . . . . . . . . . 12 |- ((N^2) + 1) e. RR
49	48	recn 5326	. . . . . . . . . . 11 |- ((N^2) + 1) e. CC
50	49, 41, 6, 9	divdir 5754	. . . . . . . . . 10 |- ((((N^2) + 1) + (2 x. N)) / 2) = ((((N^2) + 1) / 2) + ((2 x. N) / 2))
51	8, 6, 9	divcan3 5759	. . . . . . . . . . 11 |- ((2 x. N) / 2) = N
52	51	opreq2i 3978	. . . . . . . . . 10 |- ((((N^2) + 1) / 2) + ((2 x. N) / 2)) = ((((N^2) + 1) / 2) + N)
53	45, 50, 52	3eqtr 1502	. . . . . . . . 9 |- (((N + 1) x. (N + 1)) / 2) = ((((N^2) + 1) / 2) + N)
54	31, 53	eqtr3 1500	. . . . . . . 8 |- ((N + 1) x. ((N + 1) / 2)) = ((((N^2) + 1) / 2) + N)
55	28, 30, 54	3eqtr3 1506	. . . . . . 7 |- (2 x. (((N + 1) / 2) x. ((N + 1) / 2))) = ((((N^2) + 1) / 2) + N)
56	55	eleq1i 1540	. . . . . 6 |- ((2 x. (((N + 1) / 2) x. ((N + 1) / 2))) e. NN <-> ((((N^2) + 1) / 2) + N) e. NN)
57	8	addid2 5343	. . . . . . . . 9 |- (0 + N) = N
58		2re 5981	. . . . . . . . . . 11 |- 2 e. RR
59	39	nngt0 5952	. . . . . . . . . . . 12 |- 0 < (N^2)
60		lt01 5692	. . . . . . . . . . . 12 |- 0 < 1
61	46, 47, 59, 60	addgt0i 5613	. . . . . . . . . . 11 |- 0 < ((N^2) + 1)
62		2pos 5991	. . . . . . . . . . 11 |- 0 < 2
63	48, 58, 61, 62	divgt0i 5862	. . . . . . . . . 10 |- 0 < (((N^2) + 1) / 2)
64		0re 5452	. . . . . . . . . . 11 |- 0 e. RR
65	48, 58, 9	redivcl 5800	. . . . . . . . . . 11 |- (((N^2) + 1) / 2) e. RR
66	7	nnre 5933	. . . . . . . . . . 11 |- N e. RR
67	64, 65, 66	ltadd1 5603	. . . . . . . . . 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 2641	. . . . . . . 8 |- N < ((((N^2) + 1) / 2) + N)
70		nnsubt 5959	. . . . . . . . 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 697	. . . . . . . 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 5326	. . . . . . . . 9 |- (((N^2) + 1) / 2) e. CC
74	73, 8, 8	addsubass 5399	. . . . . . . 8 |- (((((N^2) + 1) / 2) + N) - N) = ((((N^2) + 1) / 2) + (N - N))
75	8	subid 5403	. . . . . . . . 9 |- (N - N) = 0
76	75	opreq2i 3978	. . . . . . . 8 |- ((((N^2) + 1) / 2) + (N - N)) = ((((N^2) + 1) / 2) + 0)
77	73	addid1 5342	. . . . . . . 8 |- ((((N^2) + 1) / 2) + 0) = (((N^2) + 1) / 2)
78	74, 76, 77	3eqtr 1502	. . . . . . 7 |- (((((N^2) + 1) / 2) + N) - N) = (((N^