This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem 4sqlem16

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 4sqlem16 
|- ( ph -> ( R <_ M /\ ( ( R = 0 \/ R = M ) -> ( M ^ 2 ) || ( M x. P ) ) ) )

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 9 20 13 4sqlem5 
 |-  ( ph -> ( E e. ZZ /\ ( ( A - E ) / M ) e. ZZ ) )
22 21 simpld 
 |-  ( ph -> E e. ZZ )
23 zsqcl 
 |-  ( E e. ZZ -> ( E ^ 2 ) e. ZZ )
24 22 23 syl 
 |-  ( ph -> ( E ^ 2 ) e. ZZ )
25 24 zred 
 |-  ( ph -> ( E ^ 2 ) e. RR )
26 10 20 14 4sqlem5 
 |-  ( ph -> ( F e. ZZ /\ ( ( B - F ) / M ) e. ZZ ) )
27 26 simpld 
 |-  ( ph -> F e. ZZ )
28 zsqcl 
 |-  ( F e. ZZ -> ( F ^ 2 ) e. ZZ )
29 27 28 syl 
 |-  ( ph -> ( F ^ 2 ) e. ZZ )
30 29 zred 
 |-  ( ph -> ( F ^ 2 ) e. RR )
31 25 30 readdcld 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. RR )
32 11 20 15 4sqlem5 
 |-  ( ph -> ( G e. ZZ /\ ( ( C - G ) / M ) e. ZZ ) )
33 32 simpld 
 |-  ( ph -> G e. ZZ )
34 zsqcl 
 |-  ( G e. ZZ -> ( G ^ 2 ) e. ZZ )
35 33 34 syl 
 |-  ( ph -> ( G ^ 2 ) e. ZZ )
36 35 zred 
 |-  ( ph -> ( G ^ 2 ) e. RR )
37 12 20 16 4sqlem5 
 |-  ( ph -> ( H e. ZZ /\ ( ( D - H ) / M ) e. ZZ ) )
38 37 simpld 
 |-  ( ph -> H e. ZZ )
39 zsqcl 
 |-  ( H e. ZZ -> ( H ^ 2 ) e. ZZ )
40 38 39 syl 
 |-  ( ph -> ( H ^ 2 ) e. ZZ )
41 40 zred 
 |-  ( ph -> ( H ^ 2 ) e. RR )
42 36 41 readdcld 
 |-  ( ph -> ( ( G ^ 2 ) + ( H ^ 2 ) ) e. RR )
43 20 nnred 
 |-  ( ph -> M e. RR )
44 43 resqcld 
 |-  ( ph -> ( M ^ 2 ) e. RR )
45 44 rehalfcld 
 |-  ( ph -> ( ( M ^ 2 ) / 2 ) e. RR )
46 45 rehalfcld 
 |-  ( ph -> ( ( ( M ^ 2 ) / 2 ) / 2 ) e. RR )
47 9 20 13 4sqlem7 
 |-  ( ph -> ( E ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) )
48 10 20 14 4sqlem7 
 |-  ( ph -> ( F ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) )
49 25 30 46 46 47 48 le2addd 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) )
50 45 recnd 
 |-  ( ph -> ( ( M ^ 2 ) / 2 ) e. CC )
51 50 2halvesd 
 |-  ( ph -> ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) = ( ( M ^ 2 ) / 2 ) )
52 49 51 breqtrd 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) <_ ( ( M ^ 2 ) / 2 ) )
53 11 20 15 4sqlem7 
 |-  ( ph -> ( G ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) )
54 12 20 16 4sqlem7 
 |-  ( ph -> ( H ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) )
55 36 41 46 46 53 54 le2addd 
 |-  ( ph -> ( ( G ^ 2 ) + ( H ^ 2 ) ) <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) )
56 55 51 breqtrd 
 |-  ( ph -> ( ( G ^ 2 ) + ( H ^ 2 ) ) <_ ( ( M ^ 2 ) / 2 ) )
57 31 42 45 45 52 56 le2addd 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) <_ ( ( ( M ^ 2 ) / 2 ) + ( ( M ^ 2 ) / 2 ) ) )
58 44 recnd 
 |-  ( ph -> ( M ^ 2 ) e. CC )
59 58 2halvesd 
 |-  ( ph -> ( ( ( M ^ 2 ) / 2 ) + ( ( M ^ 2 ) / 2 ) ) = ( M ^ 2 ) )
60 57 59 breqtrd 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) <_ ( M ^ 2 ) )
61 43 recnd 
 |-  ( ph -> M e. CC )
62 61 sqvald 
 |-  ( ph -> ( M ^ 2 ) = ( M x. M ) )
63 60 62 breqtrd 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) <_ ( M x. M ) )
64 31 42 readdcld 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) e. RR )
65 20 nngt0d 
 |-  ( ph -> 0 < M )
66 ledivmul 
 |-  ( ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) e. RR /\ M e. RR /\ ( M e. RR /\ 0 < M ) ) -> ( ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) <_ M <-> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) <_ ( M x. M ) ) )
67 64 43 43 65 66 syl112anc 
 |-  ( ph -> ( ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) <_ M <-> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) <_ ( M x. M ) ) )
68 63 67 mpbird 
 |-  ( ph -> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) <_ M )
69 17 68 eqbrtrid 
 |-  ( ph -> R <_ M )
70 simpr 
 |-  ( ( ph /\ R = 0 ) -> R = 0 )
71 17 70 eqtr3id 
 |-  ( ( ph /\ R = 0 ) -> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) = 0 )
72 64 recnd 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) e. CC )
73 20 nnne0d 
 |-  ( ph -> M =/= 0 )
74 72 61 73 diveq0ad 
 |-  ( ph -> ( ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) = 0 <-> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) = 0 ) )
75 zsqcl2 
 |-  ( E e. ZZ -> ( E ^ 2 ) e. NN0 )
76 22 75 syl 
 |-  ( ph -> ( E ^ 2 ) e. NN0 )
77 zsqcl2 
 |-  ( F e. ZZ -> ( F ^ 2 ) e. NN0 )
78 27 77 syl 
 |-  ( ph -> ( F ^ 2 ) e. NN0 )
79 76 78 nn0addcld 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. NN0 )
80 79 nn0ge0d 
 |-  ( ph -> 0 <_ ( ( E ^ 2 ) + ( F ^ 2 ) ) )
81 zsqcl2 
 |-  ( G e. ZZ -> ( G ^ 2 ) e. NN0 )
82 33 81 syl 
 |-  ( ph -> ( G ^ 2 ) e. NN0 )
83 zsqcl2 
 |-  ( H e. ZZ -> ( H ^ 2 ) e. NN0 )
84 38 83 syl 
 |-  ( ph -> ( H ^ 2 ) e. NN0 )
85 82 84 nn0addcld 
 |-  ( ph -> ( ( G ^ 2 ) + ( H ^ 2 ) ) e. NN0 )
86 85 nn0ge0d 
 |-  ( ph -> 0 <_ ( ( G ^ 2 ) + ( H ^ 2 ) ) )
87 add20 
 |-  ( ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) e. RR /\ 0 <_ ( ( E ^ 2 ) + ( F ^ 2 ) ) ) /\ ( ( ( G ^ 2 ) + ( H ^ 2 ) ) e. RR /\ 0 <_ ( ( G ^ 2 ) + ( H ^ 2 ) ) ) ) -> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) = 0 <-> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) = 0 /\ ( ( G ^ 2 ) + ( H ^ 2 ) ) = 0 ) ) )
88 31 80 42 86 87 syl22anc 
 |-  ( ph -> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) = 0 <-> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) = 0 /\ ( ( G ^ 2 ) + ( H ^ 2 ) ) = 0 ) ) )
89 74 88 bitrd 
 |-  ( ph -> ( ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) = 0 <-> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) = 0 /\ ( ( G ^ 2 ) + ( H ^ 2 ) ) = 0 ) ) )
90 89 biimpa 
 |-  ( ( ph /\ ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) + ( ( G ^ 2 ) + ( H ^ 2 ) ) ) / M ) = 0 ) -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) = 0 /\ ( ( G ^ 2 ) + ( H ^ 2 ) ) = 0 ) )
91 71 90 syldan 
 |-  ( ( ph /\ R = 0 ) -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) = 0 /\ ( ( G ^ 2 ) + ( H ^ 2 ) ) = 0 ) )
92 91 simpld 
 |-  ( ( ph /\ R = 0 ) -> ( ( E ^ 2 ) + ( F ^ 2 ) ) = 0 )
93 76 nn0ge0d 
 |-  ( ph -> 0 <_ ( E ^ 2 ) )
94 78 nn0ge0d 
 |-  ( ph -> 0 <_ ( F ^ 2 ) )
95 add20 
 |-  ( ( ( ( E ^ 2 ) e. RR /\ 0 <_ ( E ^ 2 ) ) /\ ( ( F ^ 2 ) e. RR /\ 0 <_ ( F ^ 2 ) ) ) -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) = 0 <-> ( ( E ^ 2 ) = 0 /\ ( F ^ 2 ) = 0 ) ) )
96 25 93 30 94 95 syl22anc 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) = 0 <-> ( ( E ^ 2 ) = 0 /\ ( F ^ 2 ) = 0 ) ) )
97 96 biimpa 
 |-  ( ( ph /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = 0 ) -> ( ( E ^ 2 ) = 0 /\ ( F ^ 2 ) = 0 ) )
98 92 97 syldan 
 |-  ( ( ph /\ R = 0 ) -> ( ( E ^ 2 ) = 0 /\ ( F ^ 2 ) = 0 ) )
99 98 simpld 
 |-  ( ( ph /\ R = 0 ) -> ( E ^ 2 ) = 0 )
100 9 20 13 99 4sqlem9 
 |-  ( ( ph /\ R = 0 ) -> ( M ^ 2 ) || ( A ^ 2 ) )
101 98 simprd 
 |-  ( ( ph /\ R = 0 ) -> ( F ^ 2 ) = 0 )
102 10 20 14 101 4sqlem9 
 |-  ( ( ph /\ R = 0 ) -> ( M ^ 2 ) || ( B ^ 2 ) )
103 20 nnsqcld 
 |-  ( ph -> ( M ^ 2 ) e. NN )
104 103 nnzd 
 |-  ( ph -> ( M ^ 2 ) e. ZZ )
105 zsqcl 
 |-  ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
106 9 105 syl 
 |-  ( ph -> ( A ^ 2 ) e. ZZ )
107 zsqcl 
 |-  ( B e. ZZ -> ( B ^ 2 ) e. ZZ )
108 10 107 syl 
 |-  ( ph -> ( B ^ 2 ) e. ZZ )
109 dvds2add 
 |-  ( ( ( M ^ 2 ) e. ZZ /\ ( A ^ 2 ) e. ZZ /\ ( B ^ 2 ) e. ZZ ) -> ( ( ( M ^ 2 ) || ( A ^ 2 ) /\ ( M ^ 2 ) || ( B ^ 2 ) ) -> ( M ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
110 104 106 108 109 syl3anc 
 |-  ( ph -> ( ( ( M ^ 2 ) || ( A ^ 2 ) /\ ( M ^ 2 ) || ( B ^ 2 ) ) -> ( M ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
111 110 adantr 
 |-  ( ( ph /\ R = 0 ) -> ( ( ( M ^ 2 ) || ( A ^ 2 ) /\ ( M ^ 2 ) || ( B ^ 2 ) ) -> ( M ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) ) )
112 100 102 111 mp2and 
 |-  ( ( ph /\ R = 0 ) -> ( M ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) )
113 91 simprd 
 |-  ( ( ph /\ R = 0 ) -> ( ( G ^ 2 ) + ( H ^ 2 ) ) = 0 )
114 82 nn0ge0d 
 |-  ( ph -> 0 <_ ( G ^ 2 ) )
115 84 nn0ge0d 
 |-  ( ph -> 0 <_ ( H ^ 2 ) )
116 add20 
 |-  ( ( ( ( G ^ 2 ) e. RR /\ 0 <_ ( G ^ 2 ) ) /\ ( ( H ^ 2 ) e. RR /\ 0 <_ ( H ^ 2 ) ) ) -> ( ( ( G ^ 2 ) + ( H ^ 2 ) ) = 0 <-> ( ( G ^ 2 ) = 0 /\ ( H ^ 2 ) = 0 ) ) )
117 36 114 41 115 116 syl22anc 
 |-  ( ph -> ( ( ( G ^ 2 ) + ( H ^ 2 ) ) = 0 <-> ( ( G ^ 2 ) = 0 /\ ( H ^ 2 ) = 0 ) ) )
118 117 biimpa 
 |-  ( ( ph /\ ( ( G ^ 2 ) + ( H ^ 2 ) ) = 0 ) -> ( ( G ^ 2 ) = 0 /\ ( H ^ 2 ) = 0 ) )
119 113 118 syldan 
 |-  ( ( ph /\ R = 0 ) -> ( ( G ^ 2 ) = 0 /\ ( H ^ 2 ) = 0 ) )
120 119 simpld 
 |-  ( ( ph /\ R = 0 ) -> ( G ^ 2 ) = 0 )
121 11 20 15 120 4sqlem9 
 |-  ( ( ph /\ R = 0 ) -> ( M ^ 2 ) || ( C ^ 2 ) )
122 119 simprd 
 |-  ( ( ph /\ R = 0 ) -> ( H ^ 2 ) = 0 )
123 12 20 16 122 4sqlem9 
 |-  ( ( ph /\ R = 0 ) -> ( M ^ 2 ) || ( D ^ 2 ) )
124 zsqcl 
 |-  ( C e. ZZ -> ( C ^ 2 ) e. ZZ )
125 11 124 syl 
 |-  ( ph -> ( C ^ 2 ) e. ZZ )
126 zsqcl 
 |-  ( D e. ZZ -> ( D ^ 2 ) e. ZZ )
127 12 126 syl 
 |-  ( ph -> ( D ^ 2 ) e. ZZ )
128 dvds2add 
 |-  ( ( ( M ^ 2 ) e. ZZ /\ ( C ^ 2 ) e. ZZ /\ ( D ^ 2 ) e. ZZ ) -> ( ( ( M ^ 2 ) || ( C ^ 2 ) /\ ( M ^ 2 ) || ( D ^ 2 ) ) -> ( M ^ 2 ) || ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
129 104 125 127 128 syl3anc 
 |-  ( ph -> ( ( ( M ^ 2 ) || ( C ^ 2 ) /\ ( M ^ 2 ) || ( D ^ 2 ) ) -> ( M ^ 2 ) || ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
130 129 adantr 
 |-  ( ( ph /\ R = 0 ) -> ( ( ( M ^ 2 ) || ( C ^ 2 ) /\ ( M ^ 2 ) || ( D ^ 2 ) ) -> ( M ^ 2 ) || ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
131 121 123 130 mp2and 
 |-  ( ( ph /\ R = 0 ) -> ( M ^ 2 ) || ( ( C ^ 2 ) + ( D ^ 2 ) ) )
132 106 108 zaddcld 
 |-  ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) e. ZZ )
133 125 127 zaddcld 
 |-  ( ph -> ( ( C ^ 2 ) + ( D ^ 2 ) ) e. ZZ )
134 dvds2add 
 |-  ( ( ( M ^ 2 ) e. ZZ /\ ( ( A ^ 2 ) + ( B ^ 2 ) ) e. ZZ /\ ( ( C ^ 2 ) + ( D ^ 2 ) ) e. ZZ ) -> ( ( ( M ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) /\ ( M ^ 2 ) || ( ( C ^ 2 ) + ( D ^ 2 ) ) ) -> ( M ^ 2 ) || ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) ) )
135 104 132 133 134 syl3anc 
 |-  ( ph -> ( ( ( M ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) /\ ( M ^ 2 ) || ( ( C ^ 2 ) + ( D ^ 2 ) ) ) -> ( M ^ 2 ) || ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) ) )
136 135 adantr 
 |-  ( ( ph /\ R = 0 ) -> ( ( ( M ^ 2 ) || ( ( A ^ 2 ) + ( B ^ 2 ) ) /\ ( M ^ 2 ) || ( ( C ^ 2 ) + ( D ^ 2 ) ) ) -> ( M ^ 2 ) || ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) ) )
137 112 131 136 mp2and 
 |-  ( ( ph /\ R = 0 ) -> ( M ^ 2 ) || ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
138 104 adantr 
 |-  ( ( ph /\ R = M ) -> ( M ^ 2 ) e. ZZ )
139 132 adantr 
 |-  ( ( ph /\ R = M ) -> ( ( A ^ 2 ) + ( B ^ 2 ) ) e. ZZ )
140 51 adantr 
 |-  ( ( ph /\ R = M ) -> ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) = ( ( M ^ 2 ) / 2 ) )
141 1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 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 ) ) )
142 141 simpld 
 |-  ( ( ph /\ R = M ) -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) = 0 ) )
143 142 simpld 
 |-  ( ( ph /\ R = M ) -> ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) = 0 )
144 46 recnd 
 |-  ( ph -> ( ( ( M ^ 2 ) / 2 ) / 2 ) e. CC )
145 24 zcnd 
 |-  ( ph -> ( E ^ 2 ) e. CC )
146 144 145 subeq0ad 
 |-  ( ph -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) = 0 <-> ( ( ( M ^ 2 ) / 2 ) / 2 ) = ( E ^ 2 ) ) )
147 146 adantr 
 |-  ( ( ph /\ R = M ) -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( E ^ 2 ) ) = 0 <-> ( ( ( M ^ 2 ) / 2 ) / 2 ) = ( E ^ 2 ) ) )
148 143 147 mpbid 
 |-  ( ( ph /\ R = M ) -> ( ( ( M ^ 2 ) / 2 ) / 2 ) = ( E ^ 2 ) )
149 24 adantr 
 |-  ( ( ph /\ R = M ) -> ( E ^ 2 ) e. ZZ )
150 148 149 eqeltrd 
 |-  ( ( ph /\ R = M ) -> ( ( ( M ^ 2 ) / 2 ) / 2 ) e. ZZ )
151 150 150 zaddcld 
 |-  ( ( ph /\ R = M ) -> ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) e. ZZ )
152 140 151 eqeltrrd 
 |-  ( ( ph /\ R = M ) -> ( ( M ^ 2 ) / 2 ) e. ZZ )
153 139 152 zsubcld 
 |-  ( ( ph /\ R = M ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) e. ZZ )
154 133 adantr 
 |-  ( ( ph /\ R = M ) -> ( ( C ^ 2 ) + ( D ^ 2 ) ) e. ZZ )
155 154 152 zsubcld 
 |-  ( ( ph /\ R = M ) -> ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) e. ZZ )
156 106 adantr 
 |-  ( ( ph /\ R = M ) -> ( A ^ 2 ) e. ZZ )
157 156 150 zsubcld 
 |-  ( ( ph /\ R = M ) -> ( ( A ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) e. ZZ )
158 108 adantr 
 |-  ( ( ph /\ R = M ) -> ( B ^ 2 ) e. ZZ )
159 158 150 zsubcld 
 |-  ( ( ph /\ R = M ) -> ( ( B ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) e. ZZ )
160 9 20 13 143 4sqlem10 
 |-  ( ( ph /\ R = M ) -> ( M ^ 2 ) || ( ( A ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) )
161 142 simprd 
 |-  ( ( ph /\ R = M ) -> ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( F ^ 2 ) ) = 0 )
162 10 20 14 161 4sqlem10 
 |-  ( ( ph /\ R = M ) -> ( M ^ 2 ) || ( ( B ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) )
163 138 157 159 160 162 dvds2addd 
 |-  ( ( ph /\ R = M ) -> ( M ^ 2 ) || ( ( ( A ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) + ( ( B ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) ) )
164 106 zcnd 
 |-  ( ph -> ( A ^ 2 ) e. CC )
165 108 zcnd 
 |-  ( ph -> ( B ^ 2 ) e. CC )
166 164 165 144 144 addsub4d 
 |-  ( ph -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) ) = ( ( ( A ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) + ( ( B ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) ) )
167 51 oveq2d 
 |-  ( ph -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) )
168 166 167 eqtr3d 
 |-  ( ph -> ( ( ( A ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) + ( ( B ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) )
169 168 adantr 
 |-  ( ( ph /\ R = M ) -> ( ( ( A ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) + ( ( B ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) )
170 163 169 breqtrd 
 |-  ( ( ph /\ R = M ) -> ( M ^ 2 ) || ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) )
171 125 adantr 
 |-  ( ( ph /\ R = M ) -> ( C ^ 2 ) e. ZZ )
172 171 150 zsubcld 
 |-  ( ( ph /\ R = M ) -> ( ( C ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) e. ZZ )
173 127 adantr 
 |-  ( ( ph /\ R = M ) -> ( D ^ 2 ) e. ZZ )
174 173 150 zsubcld 
 |-  ( ( ph /\ R = M ) -> ( ( D ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) e. ZZ )
175 141 simprd 
 |-  ( ( ph /\ R = M ) -> ( ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) = 0 /\ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) = 0 ) )
176 175 simpld 
 |-  ( ( ph /\ R = M ) -> ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( G ^ 2 ) ) = 0 )
177 11 20 15 176 4sqlem10 
 |-  ( ( ph /\ R = M ) -> ( M ^ 2 ) || ( ( C ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) )
178 175 simprd 
 |-  ( ( ph /\ R = M ) -> ( ( ( ( M ^ 2 ) / 2 ) / 2 ) - ( H ^ 2 ) ) = 0 )
179 12 20 16 178 4sqlem10 
 |-  ( ( ph /\ R = M ) -> ( M ^ 2 ) || ( ( D ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) )
180 138 172 174 177 179 dvds2addd 
 |-  ( ( ph /\ R = M ) -> ( M ^ 2 ) || ( ( ( C ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) + ( ( D ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) ) )
181 125 zcnd 
 |-  ( ph -> ( C ^ 2 ) e. CC )
182 127 zcnd 
 |-  ( ph -> ( D ^ 2 ) e. CC )
183 181 182 144 144 addsub4d 
 |-  ( ph -> ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) ) = ( ( ( C ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) + ( ( D ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) ) )
184 51 oveq2d 
 |-  ( ph -> ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) ) = ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) )
185 183 184 eqtr3d 
 |-  ( ph -> ( ( ( C ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) + ( ( D ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) ) = ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) )
186 185 adantr 
 |-  ( ( ph /\ R = M ) -> ( ( ( C ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) + ( ( D ^ 2 ) - ( ( ( M ^ 2 ) / 2 ) / 2 ) ) ) = ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) )
187 180 186 breqtrd 
 |-  ( ( ph /\ R = M ) -> ( M ^ 2 ) || ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) )
188 138 153 155 170 187 dvds2addd 
 |-  ( ( ph /\ R = M ) -> ( M ^ 2 ) || ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) + ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) ) )
189 132 zcnd 
 |-  ( ph -> ( ( A ^ 2 ) + ( B ^ 2 ) ) e. CC )
190 133 zcnd 
 |-  ( ph -> ( ( C ^ 2 ) + ( D ^ 2 ) ) e. CC )
191 189 190 50 50 addsub4d 
 |-  ( ph -> ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) - ( ( ( M ^ 2 ) / 2 ) + ( ( M ^ 2 ) / 2 ) ) ) = ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) + ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) ) )
192 59 oveq2d 
 |-  ( ph -> ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) - ( ( ( M ^ 2 ) / 2 ) + ( ( M ^ 2 ) / 2 ) ) ) = ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) - ( M ^ 2 ) ) )
193 191 192 eqtr3d 
 |-  ( ph -> ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) + ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) ) = ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) - ( M ^ 2 ) ) )
194 193 adantr 
 |-  ( ( ph /\ R = M ) -> ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) + ( ( ( C ^ 2 ) + ( D ^ 2 ) ) - ( ( M ^ 2 ) / 2 ) ) ) = ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) - ( M ^ 2 ) ) )
195 188 194 breqtrd 
 |-  ( ( ph /\ R = M ) -> ( M ^ 2 ) || ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) - ( M ^ 2 ) ) )
196 132 133 zaddcld 
 |-  ( ph -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) e. ZZ )
197 196 adantr 
 |-  ( ( ph /\ R = M ) -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) e. ZZ )
198 dvdssubr 
 |-  ( ( ( M ^ 2 ) e. ZZ /\ ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) e. ZZ ) -> ( ( M ^ 2 ) || ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) <-> ( M ^ 2 ) || ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) - ( M ^ 2 ) ) ) )
199 138 197 198 syl2anc 
 |-  ( ( ph /\ R = M ) -> ( ( M ^ 2 ) || ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) <-> ( M ^ 2 ) || ( ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) - ( M ^ 2 ) ) ) )
200 195 199 mpbird 
 |-  ( ( ph /\ R = M ) -> ( M ^ 2 ) || ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
201 137 200 jaodan 
 |-  ( ( ph /\ ( R = 0 \/ R = M ) ) -> ( M ^ 2 ) || ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
202 18 adantr 
 |-  ( ( ph /\ ( R = 0 \/ R = M ) ) -> ( M x. P ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) + ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
203 201 202 breqtrrd 
 |-  ( ( ph /\ ( R = 0 \/ R = M ) ) -> ( M ^ 2 ) || ( M x. P ) )
204 203 ex 
 |-  ( ph -> ( ( R = 0 \/ R = M ) -> ( M ^ 2 ) || ( M x. P ) ) )
205 69 204 jca 
 |-  ( ph -> ( R <_ M /\ ( ( R = 0 \/ R = M ) -> ( M ^ 2 ) || ( M x. P ) ) ) )