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