4sqlem15

Description: Lemma for 4sq . (Contributed by Mario Carneiro, 16-Jul-2014) (Revised by AV, 14-Sep-2020)

	Ref	Expression
Hypotheses	4sq.1	\|- S = { n \| E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }
	4sq.2	\|- ( ph -> N e. NN )
	4sq.3	\|- ( ph -> P = ( ( 2 x. N ) + 1 ) )
	4sq.4	\|- ( ph -> P e. Prime )
	4sq.5	\|- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )
	4sq.6	\|- T = { i e. NN \| ( i x. P ) e. S }
	4sq.7	\|- M = inf ( T , RR , < )
	4sq.m	\|- ( ph -> M e. ( ZZ>= ` 2 ) )
	4sq.a	\|- ( ph -> A e. ZZ )
	4sq.b	\|- ( ph -> B e. ZZ )
	4sq.c	\|- ( ph -> C e. ZZ )
	4sq.d	\|- ( ph -> D e. ZZ )
	4sq.e	\|- E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )
	4sq.f	\|- F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )
	4sq.g	\|- G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )
	4sq.h	\|- H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )
	4sq.r	\|- R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )
	4sq.p	\|- ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
Assertion	4sqlem15	\|- ( ( ph /\ R = M ) -> ( ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) = 0 ) /\ ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) = 0 ) ) )

Proof

Step	Hyp	Ref	Expression
1		4sq.1	\|- S = { n \| E. x e. ZZ E. y e. ZZ E. z e. ZZ E. w e. ZZ n = ( ( ( x ^ 2 ) + ( y ^ 2 ) ) + ( ( z ^ 2 ) + ( w ^ 2 ) ) ) }
2		4sq.2	\|- ( ph -> N e. NN )
3		4sq.3	\|- ( ph -> P = ( ( 2 x. N ) + 1 ) )
4		4sq.4	\|- ( ph -> P e. Prime )
5		4sq.5	\|- ( ph -> ( 0 ... ( 2 x. N ) ) C_ S )
6		4sq.6	\|- T = { i e. NN \| ( i x. P ) e. S }
7		4sq.7	\|- M = inf ( T , RR , < )
8		4sq.m	\|- ( ph -> M e. ( ZZ>= ` 2 ) )
9		4sq.a	\|- ( ph -> A e. ZZ )
10		4sq.b	\|- ( ph -> B e. ZZ )
11		4sq.c	\|- ( ph -> C e. ZZ )
12		4sq.d	\|- ( ph -> D e. ZZ )
13		4sq.e	\|- E = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )
14		4sq.f	\|- F = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )
15		4sq.g	\|- G = ( ( ( C + ( M / 2 ) ) mod M ) - ( M / 2 ) )
16		4sq.h	\|- H = ( ( ( D + ( M / 2 ) ) mod M ) - ( M / 2 ) )
17		4sq.r	\|- R = ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M )
18		4sq.p	\|- ( ph -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
19		eluz2nn	\|- ( M e. ( ZZ>= ` 2 ) -> M e. NN )
20	8 19	syl	\|- ( ph -> M e. NN )
21	20	nnred	\|- ( ph -> M e. RR )
22	21	resqcld	\|- ( ph -> ( M ^ 2 ) e. RR )
23	22	rehalfcld	\|- ( ph -> ( ( M ^ 2 ) / 2 ) e. RR )
24	23	rehalfcld	\|- ( ph -> ( ( ( M ^ 2 ) / 2 ) / 2 ) e. RR )
25	24	recnd	\|- ( ph -> ( ( ( M ^ 2 ) / 2 ) / 2 ) e. CC )
26	9 20 13	4sqlem5	\|- ( ph -> ( E e. ZZ /\ ( ( A - E ) / M ) e. ZZ ) )
27	26	simpld	\|- ( ph -> E e. ZZ )
28		zsqcl	\|- ( E e. ZZ -> ( E ^ 2 ) e. ZZ )
29	27 28	syl	\|- ( ph -> ( E ^ 2 ) e. ZZ )
30	29	zred	\|- ( ph -> ( E ^ 2 ) e. RR )
31	30	recnd	\|- ( ph -> ( E ^ 2 ) e. CC )
32	10 20 14	4sqlem5	\|- ( ph -> ( F e. ZZ /\ ( ( B - F ) / M ) e. ZZ ) )
33	32	simpld	\|- ( ph -> F e. ZZ )
34		zsqcl	\|- ( F e. ZZ -> ( F ^ 2 ) e. ZZ )
35	33 34	syl	\|- ( ph -> ( F ^ 2 ) e. ZZ )
36	35	zred	\|- ( ph -> ( F ^ 2 ) e. RR )
37	36	recnd	\|- ( ph -> ( F ^ 2 ) e. CC )
38	25 25 31 37	addsub4d	\|- ( ph -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) = ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) + ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) ) )
39	23	recnd	\|- ( ph -> ( ( M ^ 2 ) / 2 ) e. CC )
40	39	2halvesd	\|- ( ph -> ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) = ( ( M ^ 2 ) / 2 ) )
41	40	oveq1d	\|- ( ph -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) = ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
42	38 41	eqtr3d	\|- ( ph -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) + ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) ) = ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
43	42	adantr	\|- ( ( ph /\ R = M ) -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) + ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) ) = ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
44	22	recnd	\|- ( ph -> ( M ^ 2 ) e. CC )
45	44	2halvesd	\|- ( ph -> ( ( ( M ^ 2 ) / 2 ) + ( ( M ^ 2 ) / 2 ) ) = ( M ^ 2 ) )
46	45	adantr	\|- ( ( ph /\ R = M ) -> ( ( ( M ^ 2 ) / 2 ) + ( ( M ^ 2 ) / 2 ) ) = ( M ^ 2 ) )
47	21	recnd	\|- ( ph -> M e. CC )
48	47	sqvald	\|- ( ph -> ( M ^ 2 ) = ( M x. M ) )
49	48	adantr	\|- ( ( ph /\ R = M ) -> ( M ^ 2 ) = ( M x. M ) )
50		simpr	\|- ( ( ph /\ R = M ) -> R = M )
51	17 50	eqtr3id	\|- ( ( ph /\ R = M ) -> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) = M )
52	51	oveq1d	\|- ( ( ph /\ R = M ) -> ( ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) x. M ) = ( M x. M ) )
53	30 36	readdcld	\|- ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. RR )
54	11 20 15	4sqlem5	\|- ( ph -> ( G e. ZZ /\ ( ( C - G ) / M ) e. ZZ ) )
55	54	simpld	\|- ( ph -> G e. ZZ )
56		zsqcl	\|- ( G e. ZZ -> ( G ^ 2 ) e. ZZ )
57	55 56	syl	\|- ( ph -> ( G ^ 2 ) e. ZZ )
58	57	zred	\|- ( ph -> ( G ^ 2 ) e. RR )
59	12 20 16	4sqlem5	\|- ( ph -> ( H e. ZZ /\ ( ( D - H ) / M ) e. ZZ ) )
60	59	simpld	\|- ( ph -> H e. ZZ )
61		zsqcl	\|- ( H e. ZZ -> ( H ^ 2 ) e. ZZ )
62	60 61	syl	\|- ( ph -> ( H ^ 2 ) e. ZZ )
63	62	zred	\|- ( ph -> ( H ^ 2 ) e. RR )
64	58 63	readdcld	\|- ( ph -> ( ( G ^ 2 ) + ( H ^ 2 ) ) e. RR )
65	53 64	readdcld	\|- ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) e. RR )
66	65	recnd	\|- ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) e. CC )
67	20	nnne0d	\|- ( ph -> M =/= 0 )
68	66 47 67	divcan1d	\|- ( ph -> ( ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) x. M ) = ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) )
69	68	adantr	\|- ( ( ph /\ R = M ) -> ( ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) x. M ) = ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) )
70	49 52 69	3eqtr2rd	\|- ( ( ph /\ R = M ) -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) = ( M ^ 2 ) )
71	46 70	oveq12d	\|- ( ( ph /\ R = M ) -> ( ( ( ( M ^ 2 ) / 2 ) + ( ( M ^ 2 ) / 2 ) ) - ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) = ( ( M ^ 2 ) - ( M ^ 2 ) ) )
72	53	recnd	\|- ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. CC )
73	64	recnd	\|- ( ph -> ( ( G ^ 2 ) + ( H ^ 2 ) ) e. CC )
74	39 39 72 73	addsub4d	\|- ( ph -> ( ( ( ( M ^ 2 ) / 2 ) + ( ( M ^ 2 ) / 2 ) ) - ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) = ( ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) + ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) )
75	74	adantr	\|- ( ( ph /\ R = M ) -> ( ( ( ( M ^ 2 ) / 2 ) + ( ( M ^ 2 ) / 2 ) ) - ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) = ( ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) + ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) )
76	44	subidd	\|- ( ph -> ( ( M ^ 2 ) - ( M ^ 2 ) ) = 0 )
77	76	adantr	\|- ( ( ph /\ R = M ) -> ( ( M ^ 2 ) - ( M ^ 2 ) ) = 0 )
78	71 75 77	3eqtr3d	\|- ( ( ph /\ R = M ) -> ( ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) + ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) = 0 )
79	23 53	resubcld	\|- ( ph -> ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) e. RR )
80	9 20 13	4sqlem7	\|- ( ph -> ( E ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) )
81	10 20 14	4sqlem7	\|- ( ph -> ( F ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) )
82	30 36 24 24 80 81	le2addd	\|- ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) )
83	82 40	breqtrd	\|- ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) <_ ( ( M ^ 2 ) / 2 ) )
84	23 53	subge0d	\|- ( ph -> ( 0 <_ ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) <-> ( ( E ^ 2 ) + ( F ^ 2 ) ) <_ ( ( M ^ 2 ) / 2 ) ) )
85	83 84	mpbird	\|- ( ph -> 0 <_ ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
86	23 64	resubcld	\|- ( ph -> ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) e. RR )
87	11 20 15	4sqlem7	\|- ( ph -> ( G ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) )
88	12 20 16	4sqlem7	\|- ( ph -> ( H ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) )
89	58 63 24 24 87 88	le2addd	\|- ( ph -> ( ( G ^ 2 ) + ( H ^ 2 ) ) <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) )
90	89 40	breqtrd	\|- ( ph -> ( ( G ^ 2 ) + ( H ^ 2 ) ) <_ ( ( M ^ 2 ) / 2 ) )
91	23 64	subge0d	\|- ( ph -> ( 0 <_ ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) <-> ( ( G ^ 2 ) + ( H ^ 2 ) ) <_ ( ( M ^ 2 ) / 2 ) ) )
92	90 91	mpbird	\|- ( ph -> 0 <_ ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) )
93		add20	\|- ( ( ( ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) e. RR /\ 0 <_ ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) ) /\ ( ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) e. RR /\ 0 <_ ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) ) -> ( ( ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) + ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) = 0 <-> ( ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) = 0 /\ ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) = 0 ) ) )
94	79 85 86 92 93	syl22anc	\|- ( ph -> ( ( ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) + ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) = 0 <-> ( ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) = 0 /\ ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) = 0 ) ) )
95	94	biimpa	\|- ( ( ph /\ ( ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) + ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) = 0 ) -> ( ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) = 0 /\ ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) = 0 ) )
96	78 95	syldan	\|- ( ( ph /\ R = M ) -> ( ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) = 0 /\ ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) = 0 ) )
97	96	simpld	\|- ( ( ph /\ R = M ) -> ( ( ( M ^ 2 ) / 2 ) - ( ( E ^ 2 ) + ( F ^ 2 ) ) ) = 0 )
98	43 97	eqtrd	\|- ( ( ph /\ R = M ) -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) + ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) ) = 0 )
99	24 30	resubcld	\|- ( ph -> ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) e. RR )
100	24 30	subge0d	\|- ( ph -> ( 0 <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) <-> ( E ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) ) )
101	80 100	mpbird	\|- ( ph -> 0 <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) )
102	24 36	resubcld	\|- ( ph -> ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) e. RR )
103	24 36	subge0d	\|- ( ph -> ( 0 <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) <-> ( F ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) ) )
104	81 103	mpbird	\|- ( ph -> 0 <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) )
105		add20	\|- ( ( ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) e. RR /\ 0 <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) ) /\ ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) e. RR /\ 0 <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) ) ) -> ( ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) + ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) ) = 0 <-> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) = 0 ) ) )
106	99 101 102 104 105	syl22anc	\|- ( ph -> ( ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) + ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) ) = 0 <-> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) = 0 ) ) )
107	106	biimpa	\|- ( ( ph /\ ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) + ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) ) = 0 ) -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) = 0 ) )
108	98 107	syldan	\|- ( ( ph /\ R = M ) -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) = 0 ) )
109	58	recnd	\|- ( ph -> ( G ^ 2 ) e. CC )
110	63	recnd	\|- ( ph -> ( H ^ 2 ) e. CC )
111	25 25 109 110	addsub4d	\|- ( ph -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) = ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) + ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) ) )
112	40	oveq1d	\|- ( ph -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) = ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) )
113	111 112	eqtr3d	\|- ( ph -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) + ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) ) = ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) )
114	113	adantr	\|- ( ( ph /\ R = M ) -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) + ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) ) = ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) )
115	96	simprd	\|- ( ( ph /\ R = M ) -> ( ( ( M ^ 2 ) / 2 ) - ( ( G ^ 2 ) + ( H ^ 2 ) ) ) = 0 )
116	114 115	eqtrd	\|- ( ( ph /\ R = M ) -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) + ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) ) = 0 )
117	24 58	resubcld	\|- ( ph -> ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) e. RR )
118	24 58	subge0d	\|- ( ph -> ( 0 <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) <-> ( G ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) ) )
119	87 118	mpbird	\|- ( ph -> 0 <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) )
120	24 63	resubcld	\|- ( ph -> ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) e. RR )
121	24 63	subge0d	\|- ( ph -> ( 0 <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) <-> ( H ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) ) )
122	88 121	mpbird	\|- ( ph -> 0 <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) )
123		add20	\|- ( ( ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) e. RR /\ 0 <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) ) /\ ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) e. RR /\ 0 <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) ) ) -> ( ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) + ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) ) = 0 <-> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) = 0 ) ) )
124	117 119 120 122 123	syl22anc	\|- ( ph -> ( ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) + ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) ) = 0 <-> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) = 0 ) ) )
125	124	biimpa	\|- ( ( ph /\ ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) + ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) ) = 0 ) -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) = 0 ) )
126	116 125	syldan	\|- ( ( ph /\ R = M ) -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) = 0 ) )
127	108 126	jca	\|- ( ( ph /\ R = M ) -> ( ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) = 0 ) /\ ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) = 0 ) ) )

Metamath Proof Explorer

Theorem 4sqlem15

Proof