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