Metamath Proof Explorer

Theorem 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 ) ) )