Theorem nnesq 4720

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

Hypothesis

Ref	Expression
nnsqcl.1	|- A e. NN

Assertion

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

Proof of Theorem nnesq

Step	Hyp	Ref	Expression
1		nnmulclt 4437	. . . 4 |- (((A / 2) e. NN /\ (A / 2) e. NN) -> ((A / 2) x. (A / 2)) e. NN)
2	1	anidms 332	. . 3 |- ((A / 2) e. NN -> ((A / 2) x. (A / 2)) e. NN)
3		2nn 4487	. . . . 5 |- 2 e. NN
4		nnmulclt 4437	. . . . 5 |- ((2 e. NN /\ ((A / 2) x. (A / 2)) e. NN) -> (2 x. ((A / 2) x. (A / 2))) e. NN)
5	3, 4	mpan 518	. . . 4 |- (((A / 2) x. (A / 2)) e. NN -> (2 x. ((A / 2) x. (A / 2))) e. NN)
6		2cn 4471	. . . . . . 7 |- 2 e. CC
7		nnsqcl.1	. . . . . . . . 9 |- A e. NN
8	7	nncn 4430	. . . . . . . 8 |- A e. CC
9		2re 4470	. . . . . . . . 9 |- 2 e. RR
10		2pos 4479	. . . . . . . . 9 |- 0 < 2
11	9, 10	gt0ne0i 4345	. . . . . . . 8 |- 2 =/= 0
12	8, 6, 11	divcl 4221	. . . . . . 7 |- (A / 2) e. CC
13	6, 12, 12	mulass 4109	. . . . . 6 |- ((2 x. (A / 2)) x. (A / 2)) = (2 x. ((A / 2) x. (A / 2)))
14	8, 8, 6, 11	divass 4242	. . . . . . 7 |- ((A x. A) / 2) = (A x. (A / 2))
15	8	sqval 4685	. . . . . . . 8 |- (A^2) = (A x. A)
16	15	opreq1i 3009	. . . . . . 7 |- ((A^2) / 2) = ((A x. A) / 2)
17	6, 8, 11	divcan2 4224	. . . . . . . 8 |- (2 x. (A / 2)) = A
18	17	opreq1i 3009	. . . . . . 7 |- ((2 x. (A / 2)) x. (A / 2)) = (A x. (A / 2))
19	14, 16, 18	3eqtr4r 1127	. . . . . 6 |- ((2 x. (A / 2)) x. (A / 2)) = ((A^2) / 2)
20	13, 19	eqtr3 1121	. . . . 5 |- (2 x. ((A / 2) x. (A / 2))) = ((A^2) / 2)
21	20	eleq1i 1152	. . . 4 |- ((2 x. ((A / 2) x. (A / 2))) e. NN <-> ((A^2) / 2) e. NN)
22	5, 21	sylib 173	. . 3 |- (((A / 2) x. (A / 2)) e. NN -> ((A^2) / 2) e. NN)
23	2, 22	syl 12	. 2 |- ((A / 2) e. NN -> ((A^2) / 2) e. NN)
24		nnmulclt 4437	. . . . . 6 |- ((((A + 1) / 2) e. NN /\ ((A + 1) / 2) e. NN) -> (((A + 1) / 2) x. ((A + 1) / 2)) e. NN)
25	24	anidms 332	. . . . 5 |- (((A + 1) / 2) e. NN -> (((A + 1) / 2) x. ((A + 1) / 2)) e. NN)
26		nnmulclt 4437	. . . . . 6 |- ((2 e. NN /\ (((A + 1) / 2) x. ((A + 1) / 2)) e. NN) -> (2 x. (((A + 1) / 2) x. ((A + 1) / 2))) e. NN)
27	3, 26	mpan 518	. . . . 5 |- ((((A + 1) / 2) x. ((A + 1) / 2)) e. NN -> (2 x. (((A + 1) / 2) x. ((A + 1) / 2))) e. NN)
28		1cn 4101	. . . . . . . . . . 11 |- 1 e. CC
29	8, 28	addcl 4104	. . . . . . . . . 10 |- (A + 1) e. CC
30	6, 29, 11	divcan2 4224	. . . . . . . . 9 |- (2 x. ((A + 1) / 2)) = (A + 1)
31	30	opreq1i 3009	. . . . . . . 8 |- ((2 x. ((A + 1) / 2)) x. ((A + 1) / 2)) = ((A + 1) x. ((A + 1) / 2))
32	29, 6, 11	divcl 4221	. . . . . . . . 9 |- ((A + 1) / 2) e. CC
33	6, 32, 32	mulass 4109	. . . . . . . 8 |- ((2 x. ((A + 1) / 2)) x. ((A + 1) / 2)) = (2 x. (((A + 1) / 2) x. ((A + 1) / 2)))
34	29, 29, 6, 11	divass 4242	. . . . . . . . 9 |- (((A + 1) x. (A + 1)) / 2) = ((A + 1) x. ((A + 1) / 2))
35	29	sqval 4685	. . . . . . . . . . . 12 |- ((A + 1)^2) = ((A + 1) x. (A + 1))
36	8, 28	binom 4712	. . . . . . . . . . . . 13 |- ((A + 1)^2) = (((A^2) + (2 x. (A x. 1))) + (1^2))
37	8	mulid1 4114	. . . . . . . . . . . . . . . 16 |- (A x. 1) = A
38	37	opreq2i 3010	. . . . . . . . . . . . . . 15 |- (2 x. (A x. 1)) = (2 x. A)
39	38	opreq2i 3010	. . . . . . . . . . . . . 14 |- ((A^2) + (2 x. (A x. 1))) = ((A^2) + (2 x. A))
40		sq1 4709	. . . . . . . . . . . . . 14 |- (1^2) = 1
41	39, 40	opreq12i 3011	. . . . . . . . . . . . 13 |- (((A^2) + (2 x. (A x. 1))) + (1^2)) = (((A^2) + (2 x. A)) + 1)
42	7	nnsqcl 4717	. . . . . . . . . . . . . . 15 |- (A^2) e. NN
43	42	nncn 4430	. . . . . . . . . . . . . 14 |- (A^2) e. CC
44	6, 8	mulcl 4105	. . . . . . . . . . . . . 14 |- (2 x. A) e. CC
45	43, 44, 28	add23 4129	. . . . . . . . . . . . 13 |- (((A^2) + (2 x. A)) + 1) = (((A^2) + 1) + (2 x. A))
46	36, 41, 45	3eqtr 1123	. . . . . . . . . . . 12 |- ((A + 1)^2) = (((A^2) + 1) + (2 x. A))
47	35, 46	eqtr3 1121	. . . . . . . . . . 11 |- ((A + 1) x. (A + 1)) = (((A^2) + 1) + (2 x. A))
48	47	opreq1i 3009	. . . . . . . . . 10 |- (((A + 1) x. (A + 1)) / 2) = ((((A^2) + 1) + (2 x. A)) / 2)
49	43, 28	addcl 4104	. . . . . . . . . . 11 |- ((A^2) + 1) e. CC
50	49, 44, 6, 11	divdistr 4243	. . . . . . . . . 10 |- ((((A^2) + 1) + (2 x. A)) / 2) = ((((A^2) + 1) / 2) + ((2 x. A) / 2))
51	6, 8, 11	divcan3 4247	. . . . . . . . . . 11 |- ((2 x. A) / 2) = A
52	51	opreq2i 3010	. . . . . . . . . 10 |- ((((A^2) + 1) / 2) + ((2 x. A) / 2)) = ((((A^2) + 1) / 2) + A)
53	48, 50, 52	3eqtr 1123	. . . . . . . . 9 |- (((A + 1) x. (A + 1)) / 2) = ((((A^2) + 1) / 2) + A)
54	34, 53	eqtr3 1121	. . . . . . . 8 |- ((A + 1) x. ((A + 1) / 2)) = ((((A^2) + 1) / 2) + A)
55	31, 33, 54	3eqtr3 1124	. . . . . . 7 |- (2 x. (((A + 1) / 2) x. ((A + 1) / 2))) = ((((A^2) + 1) / 2) + A)
56	55	eleq1i 1152	. . . . . 6 |- ((2 x. (((A + 1) / 2) x. ((A + 1) / 2))) e. NN <-> ((((A^2) + 1) / 2) + A) e. NN)
57	8	addid2 4113	. . . . . . . . 9 |- (0 + A) = A
58	42	nnre 4429	. . . . . . . . . . . 12 |- (A^2) e. RR
59		ax1re 4064	. . . . . . . . . . . 12 |- 1 e. RR
60	58, 59	readdcl 4118	. . . . . . . . . . 11 |- ((A^2) + 1) e. RR
61	42	nngt0 4445	. . . . . . . . . . . 12 |- 0 < (A^2)
62		lt01 4377	. . . . . . . . . . . 12 |- 0 < 1
63	58, 59, 61, 62	addgt0i 4326	. . . . . . . . . . 11 |- 0 < ((A^2) + 1)
64	60, 9, 63, 10	divgt0i 4391	. . . . . . . . . 10 |- 0 < (((A^2) + 1) / 2)
65		ax0re 4063	. . . . . . . . . . 11 |- 0 e. RR
66	60, 9, 11	redivcl 4274	. . . . . . . . . . 11 |- (((A^2) + 1) / 2) e. RR
67	7	nnre 4429	. . . . . . . . . . 11 |- A e. RR
68	65, 66, 67	ltadd1 4313	. . . . . . . . . 10 |- (0 < (((A^2) + 1) / 2) <-> (0 + A) < ((((A^2) + 1) / 2) + A))
69	64, 68	mpbi 164	. . . . . . . . 9 |- (0 + A) < ((((A^2) + 1) / 2) + A)
70	57, 69	eqbrtrr 2078	. . . . . . . 8 |- A < ((((A^2) + 1) / 2) + A)
71		nnsubt 4451	. . . . . . . . 9 |- ((A e. NN /\ ((((A^2) + 1) / 2) + A) e. NN) -> (A < ((((A^2) + 1) / 2) + A) <-> (((((A^2) + 1) / 2) + A) - A) e. NN))
72	7, 71	mpan 518	. . . . . . . 8 |- (((((A^2) + 1) / 2) + A) e. NN -> (A < ((((A^2) + 1) / 2) + A) <-> (((((A^2) + 1) / 2) + A) - A) e. NN))
73	70, 72	mpbii 168	. . . . . . 7 |- (((((A^2) + 1) / 2) + A) e. NN -> (((((A^2) + 1) / 2) + A) - A) e. NN)
74	66	recn 4098	. . . . . . . . . 10 |- (((A^2) + 1) / 2) e. CC
75	74, 8, 8	addsubass 4152	. . . . . . . . 9 |- (((((A^2) + 1) / 2) + A) - A) = ((((A^2) + 1) / 2) + (A - A))
76	8	subid 4155	. . . . . . . . . 10 |- (A - A) = 0
77	76	opreq2i 3010	. . . . . . . . 9 |- ((((A^2) + 1) / 2) + (A - A)) = ((((A^2) + 1) / 2) + 0)
78	74	addid1 4112	. . . . . . . . 9 |- ((((A^2) + 1) / 2) + 0) = (((A^2) + 1) / 2)
79	75, 77, 78	3eqtr 1123	. . . . . . . 8 |- (((((A^2) + 1) / 2) + A) - A) = (((A^2) + 1) / 2)
80	79	eleq1i 1152	. . . . . . 7 |- ((((((A^2) + 1) / 2) + A) -