Metamath Proof Explorer

Theorem 2sqlem8

Description: Lemma for 2sq . (Contributed by Mario Carneiro, 20-Jun-2015)

Ref Expression
Hypotheses 2sq.1 
|- S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2sqlem7.2 
|- Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }
2sqlem9.5 
|- ( ph -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )
2sqlem9.7 
|- ( ph -> M || N )
2sqlem8.n 
|- ( ph -> N e. NN )
2sqlem8.m 
|- ( ph -> M e. ( ZZ>= ` 2 ) )
2sqlem8.1 
|- ( ph -> A e. ZZ )
2sqlem8.2 
|- ( ph -> B e. ZZ )
2sqlem8.3 
|- ( ph -> ( A gcd B ) = 1 )
2sqlem8.4 
|- ( ph -> N = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
2sqlem8.c 
|- C = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )
2sqlem8.d 
|- D = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )
2sqlem8.e 
|- E = ( C / ( C gcd D ) )
2sqlem8.f 
|- F = ( D / ( C gcd D ) )
Assertion 2sqlem8 
|- ( ph -> M e. S )

Proof

Step Hyp Ref Expression
1 2sq.1 
 |-  S = ran ( w e. Z[i] |-> ( ( abs ` w ) ^ 2 ) )
2 2sqlem7.2 
 |-  Y = { z | E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) }
3 2sqlem9.5 
 |-  ( ph -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )
4 2sqlem9.7 
 |-  ( ph -> M || N )
5 2sqlem8.n 
 |-  ( ph -> N e. NN )
6 2sqlem8.m 
 |-  ( ph -> M e. ( ZZ>= ` 2 ) )
7 2sqlem8.1 
 |-  ( ph -> A e. ZZ )
8 2sqlem8.2 
 |-  ( ph -> B e. ZZ )
9 2sqlem8.3 
 |-  ( ph -> ( A gcd B ) = 1 )
10 2sqlem8.4 
 |-  ( ph -> N = ( ( A ^ 2 ) + ( B ^ 2 ) ) )
11 2sqlem8.c 
 |-  C = ( ( ( A + ( M / 2 ) ) mod M ) - ( M / 2 ) )
12 2sqlem8.d 
 |-  D = ( ( ( B + ( M / 2 ) ) mod M ) - ( M / 2 ) )
13 2sqlem8.e 
 |-  E = ( C / ( C gcd D ) )
14 2sqlem8.f 
 |-  F = ( D / ( C gcd D ) )
15 eluz2b3 
 |-  ( M e. ( ZZ>= ` 2 ) <-> ( M e. NN /\ M =/= 1 ) )
16 6 15 sylib 
 |-  ( ph -> ( M e. NN /\ M =/= 1 ) )
17 16 simpld 
 |-  ( ph -> M e. NN )
18 eluzelz 
 |-  ( M e. ( ZZ>= ` 2 ) -> M e. ZZ )
19 6 18 syl 
 |-  ( ph -> M e. ZZ )
20 5 nnzd 
 |-  ( ph -> N e. ZZ )
21 7 17 11 4sqlem5 
 |-  ( ph -> ( C e. ZZ /\ ( ( A - C ) / M ) e. ZZ ) )
22 21 simpld 
 |-  ( ph -> C e. ZZ )
23 zsqcl 
 |-  ( C e. ZZ -> ( C ^ 2 ) e. ZZ )
24 22 23 syl 
 |-  ( ph -> ( C ^ 2 ) e. ZZ )
25 8 17 12 4sqlem5 
 |-  ( ph -> ( D e. ZZ /\ ( ( B - D ) / M ) e. ZZ ) )
26 25 simpld 
 |-  ( ph -> D e. ZZ )
27 zsqcl 
 |-  ( D e. ZZ -> ( D ^ 2 ) e. ZZ )
28 26 27 syl 
 |-  ( ph -> ( D ^ 2 ) e. ZZ )
29 24 28 zaddcld 
 |-  ( ph -> ( ( C ^ 2 ) + ( D ^ 2 ) ) e. ZZ )
30 zsqcl 
 |-  ( A e. ZZ -> ( A ^ 2 ) e. ZZ )
31 7 30 syl 
 |-  ( ph -> ( A ^ 2 ) e. ZZ )
32 31 24 zsubcld 
 |-  ( ph -> ( ( A ^ 2 ) - ( C ^ 2 ) ) e. ZZ )
33 zsqcl 
 |-  ( B e. ZZ -> ( B ^ 2 ) e. ZZ )
34 8 33 syl 
 |-  ( ph -> ( B ^ 2 ) e. ZZ )
35 34 28 zsubcld 
 |-  ( ph -> ( ( B ^ 2 ) - ( D ^ 2 ) ) e. ZZ )
36 7 17 11 4sqlem8 
 |-  ( ph -> M || ( ( A ^ 2 ) - ( C ^ 2 ) ) )
37 8 17 12 4sqlem8 
 |-  ( ph -> M || ( ( B ^ 2 ) - ( D ^ 2 ) ) )
38 19 32 35 36 37 dvds2addd 
 |-  ( ph -> M || ( ( ( A ^ 2 ) - ( C ^ 2 ) ) + ( ( B ^ 2 ) - ( D ^ 2 ) ) ) )
39 10 oveq1d 
 |-  ( ph -> ( N - ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
40 31 zcnd 
 |-  ( ph -> ( A ^ 2 ) e. CC )
41 34 zcnd 
 |-  ( ph -> ( B ^ 2 ) e. CC )
42 24 zcnd 
 |-  ( ph -> ( C ^ 2 ) e. CC )
43 28 zcnd 
 |-  ( ph -> ( D ^ 2 ) e. CC )
44 40 41 42 43 addsub4d 
 |-  ( ph -> ( ( ( A ^ 2 ) + ( B ^ 2 ) ) - ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) - ( C ^ 2 ) ) + ( ( B ^ 2 ) - ( D ^ 2 ) ) ) )
45 39 44 eqtrd 
 |-  ( ph -> ( N - ( ( C ^ 2 ) + ( D ^ 2 ) ) ) = ( ( ( A ^ 2 ) - ( C ^ 2 ) ) + ( ( B ^ 2 ) - ( D ^ 2 ) ) ) )
46 38 45 breqtrrd 
 |-  ( ph -> M || ( N - ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
47 dvdssub2 
 |-  ( ( ( M e. ZZ /\ N e. ZZ /\ ( ( C ^ 2 ) + ( D ^ 2 ) ) e. ZZ ) /\ M || ( N - ( ( C ^ 2 ) + ( D ^ 2 ) ) ) ) -> ( M || N <-> M || ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
48 19 20 29 46 47 syl31anc 
 |-  ( ph -> ( M || N <-> M || ( ( C ^ 2 ) + ( D ^ 2 ) ) ) )
49 4 48 mpbid 
 |-  ( ph -> M || ( ( C ^ 2 ) + ( D ^ 2 ) ) )
50 1 2 3 4 5 6 7 8 9 10 11 12 2sqlem8a 
 |-  ( ph -> ( C gcd D ) e. NN )
51 50 nnzd 
 |-  ( ph -> ( C gcd D ) e. ZZ )
52 zsqcl2 
 |-  ( ( C gcd D ) e. ZZ -> ( ( C gcd D ) ^ 2 ) e. NN0 )
53 51 52 syl 
 |-  ( ph -> ( ( C gcd D ) ^ 2 ) e. NN0 )
54 53 nn0cnd 
 |-  ( ph -> ( ( C gcd D ) ^ 2 ) e. CC )
55 gcddvds 
 |-  ( ( C e. ZZ /\ D e. ZZ ) -> ( ( C gcd D ) || C /\ ( C gcd D ) || D ) )
56 22 26 55 syl2anc 
 |-  ( ph -> ( ( C gcd D ) || C /\ ( C gcd D ) || D ) )
57 56 simpld 
 |-  ( ph -> ( C gcd D ) || C )
58 50 nnne0d 
 |-  ( ph -> ( C gcd D ) =/= 0 )
59 dvdsval2 
 |-  ( ( ( C gcd D ) e. ZZ /\ ( C gcd D ) =/= 0 /\ C e. ZZ ) -> ( ( C gcd D ) || C <-> ( C / ( C gcd D ) ) e. ZZ ) )
60 51 58 22 59 syl3anc 
 |-  ( ph -> ( ( C gcd D ) || C <-> ( C / ( C gcd D ) ) e. ZZ ) )
61 57 60 mpbid 
 |-  ( ph -> ( C / ( C gcd D ) ) e. ZZ )
62 13 61 eqeltrid 
 |-  ( ph -> E e. ZZ )
63 zsqcl2 
 |-  ( E e. ZZ -> ( E ^ 2 ) e. NN0 )
64 62 63 syl 
 |-  ( ph -> ( E ^ 2 ) e. NN0 )
65 64 nn0cnd 
 |-  ( ph -> ( E ^ 2 ) e. CC )
66 56 simprd 
 |-  ( ph -> ( C gcd D ) || D )
67 dvdsval2 
 |-  ( ( ( C gcd D ) e. ZZ /\ ( C gcd D ) =/= 0 /\ D e. ZZ ) -> ( ( C gcd D ) || D <-> ( D / ( C gcd D ) ) e. ZZ ) )
68 51 58 26 67 syl3anc 
 |-  ( ph -> ( ( C gcd D ) || D <-> ( D / ( C gcd D ) ) e. ZZ ) )
69 66 68 mpbid 
 |-  ( ph -> ( D / ( C gcd D ) ) e. ZZ )
70 14 69 eqeltrid 
 |-  ( ph -> F e. ZZ )
71 zsqcl2 
 |-  ( F e. ZZ -> ( F ^ 2 ) e. NN0 )
72 70 71 syl 
 |-  ( ph -> ( F ^ 2 ) e. NN0 )
73 72 nn0cnd 
 |-  ( ph -> ( F ^ 2 ) e. CC )
74 54 65 73 adddid 
 |-  ( ph -> ( ( ( C gcd D ) ^ 2 ) x. ( ( E ^ 2 ) + ( F ^ 2 ) ) ) = ( ( ( ( C gcd D ) ^ 2 ) x. ( E ^ 2 ) ) + ( ( ( C gcd D ) ^ 2 ) x. ( F ^ 2 ) ) ) )
75 51 zcnd 
 |-  ( ph -> ( C gcd D ) e. CC )
76 62 zcnd 
 |-  ( ph -> E e. CC )
77 75 76 sqmuld 
 |-  ( ph -> ( ( ( C gcd D ) x. E ) ^ 2 ) = ( ( ( C gcd D ) ^ 2 ) x. ( E ^ 2 ) ) )
78 13 oveq2i 
 |-  ( ( C gcd D ) x. E ) = ( ( C gcd D ) x. ( C / ( C gcd D ) ) )
79 22 zcnd 
 |-  ( ph -> C e. CC )
80 79 75 58 divcan2d 
 |-  ( ph -> ( ( C gcd D ) x. ( C / ( C gcd D ) ) ) = C )
81 78 80 eqtrid 
 |-  ( ph -> ( ( C gcd D ) x. E ) = C )
82 81 oveq1d 
 |-  ( ph -> ( ( ( C gcd D ) x. E ) ^ 2 ) = ( C ^ 2 ) )
83 77 82 eqtr3d 
 |-  ( ph -> ( ( ( C gcd D ) ^ 2 ) x. ( E ^ 2 ) ) = ( C ^ 2 ) )
84 70 zcnd 
 |-  ( ph -> F e. CC )
85 75 84 sqmuld 
 |-  ( ph -> ( ( ( C gcd D ) x. F ) ^ 2 ) = ( ( ( C gcd D ) ^ 2 ) x. ( F ^ 2 ) ) )
86 14 oveq2i 
 |-  ( ( C gcd D ) x. F ) = ( ( C gcd D ) x. ( D / ( C gcd D ) ) )
87 26 zcnd 
 |-  ( ph -> D e. CC )
88 87 75 58 divcan2d 
 |-  ( ph -> ( ( C gcd D ) x. ( D / ( C gcd D ) ) ) = D )
89 86 88 eqtrid 
 |-  ( ph -> ( ( C gcd D ) x. F ) = D )
90 89 oveq1d 
 |-  ( ph -> ( ( ( C gcd D ) x. F ) ^ 2 ) = ( D ^ 2 ) )
91 85 90 eqtr3d 
 |-  ( ph -> ( ( ( C gcd D ) ^ 2 ) x. ( F ^ 2 ) ) = ( D ^ 2 ) )
92 83 91 oveq12d 
 |-  ( ph -> ( ( ( ( C gcd D ) ^ 2 ) x. ( E ^ 2 ) ) + ( ( ( C gcd D ) ^ 2 ) x. ( F ^ 2 ) ) ) = ( ( C ^ 2 ) + ( D ^ 2 ) ) )
93 74 92 eqtrd 
 |-  ( ph -> ( ( ( C gcd D ) ^ 2 ) x. ( ( E ^ 2 ) + ( F ^ 2 ) ) ) = ( ( C ^ 2 ) + ( D ^ 2 ) ) )
94 49 93 breqtrrd 
 |-  ( ph -> M || ( ( ( C gcd D ) ^ 2 ) x. ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
95 zsqcl 
 |-  ( ( C gcd D ) e. ZZ -> ( ( C gcd D ) ^ 2 ) e. ZZ )
96 51 95 syl 
 |-  ( ph -> ( ( C gcd D ) ^ 2 ) e. ZZ )
97 19 96 gcdcomd 
 |-  ( ph -> ( M gcd ( ( C gcd D ) ^ 2 ) ) = ( ( ( C gcd D ) ^ 2 ) gcd M ) )
98 51 19 gcdcld 
 |-  ( ph -> ( ( C gcd D ) gcd M ) e. NN0 )
99 98 nn0zd 
 |-  ( ph -> ( ( C gcd D ) gcd M ) e. ZZ )
100 gcddvds 
 |-  ( ( ( C gcd D ) e. ZZ /\ M e. ZZ ) -> ( ( ( C gcd D ) gcd M ) || ( C gcd D ) /\ ( ( C gcd D ) gcd M ) || M ) )
101 51 19 100 syl2anc 
 |-  ( ph -> ( ( ( C gcd D ) gcd M ) || ( C gcd D ) /\ ( ( C gcd D ) gcd M ) || M ) )
102 101 simpld 
 |-  ( ph -> ( ( C gcd D ) gcd M ) || ( C gcd D ) )
103 99 51 22 102 57 dvdstrd 
 |-  ( ph -> ( ( C gcd D ) gcd M ) || C )
104 7 22 zsubcld 
 |-  ( ph -> ( A - C ) e. ZZ )
105 101 simprd 
 |-  ( ph -> ( ( C gcd D ) gcd M ) || M )
106 21 simprd 
 |-  ( ph -> ( ( A - C ) / M ) e. ZZ )
107 17 nnne0d 
 |-  ( ph -> M =/= 0 )
108 dvdsval2 
 |-  ( ( M e. ZZ /\ M =/= 0 /\ ( A - C ) e. ZZ ) -> ( M || ( A - C ) <-> ( ( A - C ) / M ) e. ZZ ) )
109 19 107 104 108 syl3anc 
 |-  ( ph -> ( M || ( A - C ) <-> ( ( A - C ) / M ) e. ZZ ) )
110 106 109 mpbird 
 |-  ( ph -> M || ( A - C ) )
111 99 19 104 105 110 dvdstrd 
 |-  ( ph -> ( ( C gcd D ) gcd M ) || ( A - C ) )
112 dvdssub2 
 |-  ( ( ( ( ( C gcd D ) gcd M ) e. ZZ /\ A e. ZZ /\ C e. ZZ ) /\ ( ( C gcd D ) gcd M ) || ( A - C ) ) -> ( ( ( C gcd D ) gcd M ) || A <-> ( ( C gcd D ) gcd M ) || C ) )
113 99 7 22 111 112 syl31anc 
 |-  ( ph -> ( ( ( C gcd D ) gcd M ) || A <-> ( ( C gcd D ) gcd M ) || C ) )
114 103 113 mpbird 
 |-  ( ph -> ( ( C gcd D ) gcd M ) || A )
115 99 51 26 102 66 dvdstrd 
 |-  ( ph -> ( ( C gcd D ) gcd M ) || D )
116 8 26 zsubcld 
 |-  ( ph -> ( B - D ) e. ZZ )
117 25 simprd 
 |-  ( ph -> ( ( B - D ) / M ) e. ZZ )
118 dvdsval2 
 |-  ( ( M e. ZZ /\ M =/= 0 /\ ( B - D ) e. ZZ ) -> ( M || ( B - D ) <-> ( ( B - D ) / M ) e. ZZ ) )
119 19 107 116 118 syl3anc 
 |-  ( ph -> ( M || ( B - D ) <-> ( ( B - D ) / M ) e. ZZ ) )
120 117 119 mpbird 
 |-  ( ph -> M || ( B - D ) )
121 99 19 116 105 120 dvdstrd 
 |-  ( ph -> ( ( C gcd D ) gcd M ) || ( B - D ) )
122 dvdssub2 
 |-  ( ( ( ( ( C gcd D ) gcd M ) e. ZZ /\ B e. ZZ /\ D e. ZZ ) /\ ( ( C gcd D ) gcd M ) || ( B - D ) ) -> ( ( ( C gcd D ) gcd M ) || B <-> ( ( C gcd D ) gcd M ) || D ) )
123 99 8 26 121 122 syl31anc 
 |-  ( ph -> ( ( ( C gcd D ) gcd M ) || B <-> ( ( C gcd D ) gcd M ) || D ) )
124 115 123 mpbird 
 |-  ( ph -> ( ( C gcd D ) gcd M ) || B )
125 ax-1ne0 
 |-  1 =/= 0
126 125 a1i 
 |-  ( ph -> 1 =/= 0 )
127 9 126 eqnetrd 
 |-  ( ph -> ( A gcd B ) =/= 0 )
128 127 neneqd 
 |-  ( ph -> -. ( A gcd B ) = 0 )
129 gcdeq0 
 |-  ( ( A e. ZZ /\ B e. ZZ ) -> ( ( A gcd B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
130 7 8 129 syl2anc 
 |-  ( ph -> ( ( A gcd B ) = 0 <-> ( A = 0 /\ B = 0 ) ) )
131 128 130 mtbid 
 |-  ( ph -> -. ( A = 0 /\ B = 0 ) )
132 dvdslegcd 
 |-  ( ( ( ( ( C gcd D ) gcd M ) e. ZZ /\ A e. ZZ /\ B e. ZZ ) /\ -. ( A = 0 /\ B = 0 ) ) -> ( ( ( ( C gcd D ) gcd M ) || A /\ ( ( C gcd D ) gcd M ) || B ) -> ( ( C gcd D ) gcd M ) <_ ( A gcd B ) ) )
133 99 7 8 131 132 syl31anc 
 |-  ( ph -> ( ( ( ( C gcd D ) gcd M ) || A /\ ( ( C gcd D ) gcd M ) || B ) -> ( ( C gcd D ) gcd M ) <_ ( A gcd B ) ) )
134 114 124 133 mp2and 
 |-  ( ph -> ( ( C gcd D ) gcd M ) <_ ( A gcd B ) )
135 134 9 breqtrd 
 |-  ( ph -> ( ( C gcd D ) gcd M ) <_ 1 )
136 simpr 
 |-  ( ( ( C gcd D ) = 0 /\ M = 0 ) -> M = 0 )
137 136 necon3ai 
 |-  ( M =/= 0 -> -. ( ( C gcd D ) = 0 /\ M = 0 ) )
138 107 137 syl 
 |-  ( ph -> -. ( ( C gcd D ) = 0 /\ M = 0 ) )
139 gcdn0cl 
 |-  ( ( ( ( C gcd D ) e. ZZ /\ M e. ZZ ) /\ -. ( ( C gcd D ) = 0 /\ M = 0 ) ) -> ( ( C gcd D ) gcd M ) e. NN )
140 51 19 138 139 syl21anc 
 |-  ( ph -> ( ( C gcd D ) gcd M ) e. NN )
141 nnle1eq1 
 |-  ( ( ( C gcd D ) gcd M ) e. NN -> ( ( ( C gcd D ) gcd M ) <_ 1 <-> ( ( C gcd D ) gcd M ) = 1 ) )
142 140 141 syl 
 |-  ( ph -> ( ( ( C gcd D ) gcd M ) <_ 1 <-> ( ( C gcd D ) gcd M ) = 1 ) )
143 135 142 mpbid 
 |-  ( ph -> ( ( C gcd D ) gcd M ) = 1 )
144 2nn 
 |-  2 e. NN
145 144 a1i 
 |-  ( ph -> 2 e. NN )
146 rplpwr 
 |-  ( ( ( C gcd D ) e. NN /\ M e. NN /\ 2 e. NN ) -> ( ( ( C gcd D ) gcd M ) = 1 -> ( ( ( C gcd D ) ^ 2 ) gcd M ) = 1 ) )
147 50 17 145 146 syl3anc 
 |-  ( ph -> ( ( ( C gcd D ) gcd M ) = 1 -> ( ( ( C gcd D ) ^ 2 ) gcd M ) = 1 ) )
148 143 147 mpd 
 |-  ( ph -> ( ( ( C gcd D ) ^ 2 ) gcd M ) = 1 )
149 97 148 eqtrd 
 |-  ( ph -> ( M gcd ( ( C gcd D ) ^ 2 ) ) = 1 )
150 64 72 nn0addcld 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. NN0 )
151 150 nn0zd 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. ZZ )
152 coprmdvds 
 |-  ( ( M e. ZZ /\ ( ( C gcd D ) ^ 2 ) e. ZZ /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) e. ZZ ) -> ( ( M || ( ( ( C gcd D ) ^ 2 ) x. ( ( E ^ 2 ) + ( F ^ 2 ) ) ) /\ ( M gcd ( ( C gcd D ) ^ 2 ) ) = 1 ) -> M || ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
153 19 96 151 152 syl3anc 
 |-  ( ph -> ( ( M || ( ( ( C gcd D ) ^ 2 ) x. ( ( E ^ 2 ) + ( F ^ 2 ) ) ) /\ ( M gcd ( ( C gcd D ) ^ 2 ) ) = 1 ) -> M || ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
154 94 149 153 mp2and 
 |-  ( ph -> M || ( ( E ^ 2 ) + ( F ^ 2 ) ) )
155 dvdsval2 
 |-  ( ( M e. ZZ /\ M =/= 0 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) e. ZZ ) -> ( M || ( ( E ^ 2 ) + ( F ^ 2 ) ) <-> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. ZZ ) )
156 19 107 151 155 syl3anc 
 |-  ( ph -> ( M || ( ( E ^ 2 ) + ( F ^ 2 ) ) <-> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. ZZ ) )
157 154 156 mpbid 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. ZZ )
158 64 nn0red 
 |-  ( ph -> ( E ^ 2 ) e. RR )
159 72 nn0red 
 |-  ( ph -> ( F ^ 2 ) e. RR )
160 158 159 readdcld 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. RR )
161 17 nnred 
 |-  ( ph -> M e. RR )
162 1 2 2sqlem7 
 |-  Y C_ ( S i^i NN )
163 inss2 
 |-  ( S i^i NN ) C_ NN
164 162 163 sstri 
 |-  Y C_ NN
165 62 70 gcdcld 
 |-  ( ph -> ( E gcd F ) e. NN0 )
166 165 nn0cnd 
 |-  ( ph -> ( E gcd F ) e. CC )
167 1cnd 
 |-  ( ph -> 1 e. CC )
168 75 mulridd 
 |-  ( ph -> ( ( C gcd D ) x. 1 ) = ( C gcd D ) )
169 81 89 oveq12d 
 |-  ( ph -> ( ( ( C gcd D ) x. E ) gcd ( ( C gcd D ) x. F ) ) = ( C gcd D ) )
170 22 26 gcdcld 
 |-  ( ph -> ( C gcd D ) e. NN0 )
171 mulgcd 
 |-  ( ( ( C gcd D ) e. NN0 /\ E e. ZZ /\ F e. ZZ ) -> ( ( ( C gcd D ) x. E ) gcd ( ( C gcd D ) x. F ) ) = ( ( C gcd D ) x. ( E gcd F ) ) )
172 170 62 70 171 syl3anc 
 |-  ( ph -> ( ( ( C gcd D ) x. E ) gcd ( ( C gcd D ) x. F ) ) = ( ( C gcd D ) x. ( E gcd F ) ) )
173 168 169 172 3eqtr2rd 
 |-  ( ph -> ( ( C gcd D ) x. ( E gcd F ) ) = ( ( C gcd D ) x. 1 ) )
174 166 167 75 58 173 mulcanad 
 |-  ( ph -> ( E gcd F ) = 1 )
175 eqidd 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( E ^ 2 ) + ( F ^ 2 ) ) )
176 oveq1 
 |-  ( x = E -> ( x gcd y ) = ( E gcd y ) )
177 176 eqeq1d 
 |-  ( x = E -> ( ( x gcd y ) = 1 <-> ( E gcd y ) = 1 ) )
178 oveq1 
 |-  ( x = E -> ( x ^ 2 ) = ( E ^ 2 ) )
179 178 oveq1d 
 |-  ( x = E -> ( ( x ^ 2 ) + ( y ^ 2 ) ) = ( ( E ^ 2 ) + ( y ^ 2 ) ) )
180 179 eqeq2d 
 |-  ( x = E -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( E ^ 2 ) + ( y ^ 2 ) ) ) )
181 177 180 anbi12d 
 |-  ( x = E -> ( ( ( x gcd y ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> ( ( E gcd y ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( E ^ 2 ) + ( y ^ 2 ) ) ) ) )
182 oveq2 
 |-  ( y = F -> ( E gcd y ) = ( E gcd F ) )
183 182 eqeq1d 
 |-  ( y = F -> ( ( E gcd y ) = 1 <-> ( E gcd F ) = 1 ) )
184 oveq1 
 |-  ( y = F -> ( y ^ 2 ) = ( F ^ 2 ) )
185 184 oveq2d 
 |-  ( y = F -> ( ( E ^ 2 ) + ( y ^ 2 ) ) = ( ( E ^ 2 ) + ( F ^ 2 ) ) )
186 185 eqeq2d 
 |-  ( y = F -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( E ^ 2 ) + ( y ^ 2 ) ) <-> ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
187 183 186 anbi12d 
 |-  ( y = F -> ( ( ( E gcd y ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( E ^ 2 ) + ( y ^ 2 ) ) ) <-> ( ( E gcd F ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( E ^ 2 ) + ( F ^ 2 ) ) ) ) )
188 181 187 rspc2ev 
 |-  ( ( E e. ZZ /\ F e. ZZ /\ ( ( E gcd F ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( E ^ 2 ) + ( F ^ 2 ) ) ) ) -> E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
189 62 70 174 175 188 syl112anc 
 |-  ( ph -> E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
190 ovex 
 |-  ( ( E ^ 2 ) + ( F ^ 2 ) ) e. _V
191 eqeq1 
 |-  ( z = ( ( E ^ 2 ) + ( F ^ 2 ) ) -> ( z = ( ( x ^ 2 ) + ( y ^ 2 ) ) <-> ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
192 191 anbi2d 
 |-  ( z = ( ( E ^ 2 ) + ( F ^ 2 ) ) -> ( ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> ( ( x gcd y ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
193 192 2rexbidv 
 |-  ( z = ( ( E ^ 2 ) + ( F ^ 2 ) ) -> ( E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ z = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) <-> E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) ) )
194 190 193 2 elab2 
 |-  ( ( ( E ^ 2 ) + ( F ^ 2 ) ) e. Y <-> E. x e. ZZ E. y e. ZZ ( ( x gcd y ) = 1 /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) = ( ( x ^ 2 ) + ( y ^ 2 ) ) ) )
195 189 194 sylibr 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. Y )
196 164 195 sselid 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. NN )
197 196 nngt0d 
 |-  ( ph -> 0 < ( ( E ^ 2 ) + ( F ^ 2 ) ) )
198 17 nngt0d 
 |-  ( ph -> 0 < M )
199 160 161 197 198 divgt0d 
 |-  ( ph -> 0 < ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) )
200 elnnz 
 |-  ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. NN <-> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. ZZ /\ 0 < ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) )
201 157 199 200 sylanbrc 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. NN )
202 prmnn 
 |-  ( p e. Prime -> p e. NN )
203 202 ad2antrl 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p e. NN )
204 203 nnred 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p e. RR )
205 157 adantr 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. ZZ )
206 205 zred 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. RR )
207 peano2zm 
 |-  ( M e. ZZ -> ( M - 1 ) e. ZZ )
208 19 207 syl 
 |-  ( ph -> ( M - 1 ) e. ZZ )
209 208 zred 
 |-  ( ph -> ( M - 1 ) e. RR )
210 209 adantr 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( M - 1 ) e. RR )
211 simprr 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) )
212 prmz 
 |-  ( p e. Prime -> p e. ZZ )
213 212 ad2antrl 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p e. ZZ )
214 201 adantr 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. NN )
215 dvdsle 
 |-  ( ( p e. ZZ /\ ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. NN ) -> ( p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) -> p <_ ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) )
216 213 214 215 syl2anc 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) -> p <_ ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) )
217 211 216 mpd 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p <_ ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) )
218 zsqcl 
 |-  ( M e. ZZ -> ( M ^ 2 ) e. ZZ )
219 19 218 syl 
 |-  ( ph -> ( M ^ 2 ) e. ZZ )
220 219 zred 
 |-  ( ph -> ( M ^ 2 ) e. RR )
221 220 rehalfcld 
 |-  ( ph -> ( ( M ^ 2 ) / 2 ) e. RR )
222 24 zred 
 |-  ( ph -> ( C ^ 2 ) e. RR )
223 28 zred 
 |-  ( ph -> ( D ^ 2 ) e. RR )
224 222 223 readdcld 
 |-  ( ph -> ( ( C ^ 2 ) + ( D ^ 2 ) ) e. RR )
225 1red 
 |-  ( ph -> 1 e. RR )
226 50 nnsqcld 
 |-  ( ph -> ( ( C gcd D ) ^ 2 ) e. NN )
227 226 nnred 
 |-  ( ph -> ( ( C gcd D ) ^ 2 ) e. RR )
228 150 nn0ge0d 
 |-  ( ph -> 0 <_ ( ( E ^ 2 ) + ( F ^ 2 ) ) )
229 226 nnge1d 
 |-  ( ph -> 1 <_ ( ( C gcd D ) ^ 2 ) )
230 225 227 160 228 229 lemul1ad 
 |-  ( ph -> ( 1 x. ( ( E ^ 2 ) + ( F ^ 2 ) ) ) <_ ( ( ( C gcd D ) ^ 2 ) x. ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
231 150 nn0cnd 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. CC )
232 231 mullidd 
 |-  ( ph -> ( 1 x. ( ( E ^ 2 ) + ( F ^ 2 ) ) ) = ( ( E ^ 2 ) + ( F ^ 2 ) ) )
233 230 232 93 3brtr3d 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) <_ ( ( C ^ 2 ) + ( D ^ 2 ) ) )
234 221 rehalfcld 
 |-  ( ph -> ( ( ( M ^ 2 ) / 2 ) / 2 ) e. RR )
235 7 17 11 4sqlem7 
 |-  ( ph -> ( C ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) )
236 8 17 12 4sqlem7 
 |-  ( ph -> ( D ^ 2 ) <_ ( ( ( M ^ 2 ) / 2 ) / 2 ) )
237 222 223 234 234 235 236 le2addd 
 |-  ( ph -> ( ( C ^ 2 ) + ( D ^ 2 ) ) <_ ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) )
238 221 recnd 
 |-  ( ph -> ( ( M ^ 2 ) / 2 ) e. CC )
239 238 2halvesd 
 |-  ( ph -> ( ( ( ( M ^ 2 ) / 2 ) / 2 ) + ( ( ( M ^ 2 ) / 2 ) / 2 ) ) = ( ( M ^ 2 ) / 2 ) )
240 237 239 breqtrd 
 |-  ( ph -> ( ( C ^ 2 ) + ( D ^ 2 ) ) <_ ( ( M ^ 2 ) / 2 ) )
241 160 224 221 233 240 letrd 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) <_ ( ( M ^ 2 ) / 2 ) )
242 17 nnsqcld 
 |-  ( ph -> ( M ^ 2 ) e. NN )
243 242 nnrpd 
 |-  ( ph -> ( M ^ 2 ) e. RR+ )
244 rphalflt 
 |-  ( ( M ^ 2 ) e. RR+ -> ( ( M ^ 2 ) / 2 ) < ( M ^ 2 ) )
245 243 244 syl 
 |-  ( ph -> ( ( M ^ 2 ) / 2 ) < ( M ^ 2 ) )
246 160 221 220 241 245 lelttrd 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) < ( M ^ 2 ) )
247 19 zcnd 
 |-  ( ph -> M e. CC )
248 247 sqvald 
 |-  ( ph -> ( M ^ 2 ) = ( M x. M ) )
249 246 248 breqtrd 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) < ( M x. M ) )
250 ltdivmul 
 |-  ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) e. RR /\ M e. RR /\ ( M e. RR /\ 0 < M ) ) -> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) < M <-> ( ( E ^ 2 ) + ( F ^ 2 ) ) < ( M x. M ) ) )
251 160 161 161 198 250 syl112anc 
 |-  ( ph -> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) < M <-> ( ( E ^ 2 ) + ( F ^ 2 ) ) < ( M x. M ) ) )
252 249 251 mpbird 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) < M )
253 zltlem1 
 |-  ( ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. ZZ /\ M e. ZZ ) -> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) < M <-> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) <_ ( M - 1 ) ) )
254 157 19 253 syl2anc 
 |-  ( ph -> ( ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) < M <-> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) <_ ( M - 1 ) ) )
255 252 254 mpbid 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) <_ ( M - 1 ) )
256 255 adantr 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) <_ ( M - 1 ) )
257 204 206 210 217 256 letrd 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p <_ ( M - 1 ) )
258 208 adantr 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( M - 1 ) e. ZZ )
259 fznn 
 |-  ( ( M - 1 ) e. ZZ -> ( p e. ( 1 ... ( M - 1 ) ) <-> ( p e. NN /\ p <_ ( M - 1 ) ) ) )
260 258 259 syl 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( p e. ( 1 ... ( M - 1 ) ) <-> ( p e. NN /\ p <_ ( M - 1 ) ) ) )
261 203 257 260 mpbir2and 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p e. ( 1 ... ( M - 1 ) ) )
262 195 adantr 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. Y )
263 261 262 jca 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( p e. ( 1 ... ( M - 1 ) ) /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) e. Y ) )
264 3 adantr 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) )
265 151 adantr 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. ZZ )
266 dvdsmul2 
 |-  ( ( M e. ZZ /\ ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) e. ZZ ) -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) || ( M x. ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) )
267 19 157 266 syl2anc 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) || ( M x. ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) )
268 231 247 107 divcan2d 
 |-  ( ph -> ( M x. ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) = ( ( E ^ 2 ) + ( F ^ 2 ) ) )
269 267 268 breqtrd 
 |-  ( ph -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) || ( ( E ^ 2 ) + ( F ^ 2 ) ) )
270 269 adantr 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) || ( ( E ^ 2 ) + ( F ^ 2 ) ) )
271 213 205 265 211 270 dvdstrd 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p || ( ( E ^ 2 ) + ( F ^ 2 ) ) )
272 breq1 
 |-  ( b = p -> ( b || a <-> p || a ) )
273 eleq1w 
 |-  ( b = p -> ( b e. S <-> p e. S ) )
274 272 273 imbi12d 
 |-  ( b = p -> ( ( b || a -> b e. S ) <-> ( p || a -> p e. S ) ) )
275 breq2 
 |-  ( a = ( ( E ^ 2 ) + ( F ^ 2 ) ) -> ( p || a <-> p || ( ( E ^ 2 ) + ( F ^ 2 ) ) ) )
276 275 imbi1d 
 |-  ( a = ( ( E ^ 2 ) + ( F ^ 2 ) ) -> ( ( p || a -> p e. S ) <-> ( p || ( ( E ^ 2 ) + ( F ^ 2 ) ) -> p e. S ) ) )
277 274 276 rspc2v 
 |-  ( ( p e. ( 1 ... ( M - 1 ) ) /\ ( ( E ^ 2 ) + ( F ^ 2 ) ) e. Y ) -> ( A. b e. ( 1 ... ( M - 1 ) ) A. a e. Y ( b || a -> b e. S ) -> ( p || ( ( E ^ 2 ) + ( F ^ 2 ) ) -> p e. S ) ) )
278 263 264 271 277 syl3c 
 |-  ( ( ph /\ ( p e. Prime /\ p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) ) -> p e. S )
279 278 expr 
 |-  ( ( ph /\ p e. Prime ) -> ( p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) -> p e. S ) )
280 279 ralrimiva 
 |-  ( ph -> A. p e. Prime ( p || ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) -> p e. S ) )
281 inss1 
 |-  ( S i^i NN ) C_ S
282 162 281 sstri 
 |-  Y C_ S
283 282 195 sselid 
 |-  ( ph -> ( ( E ^ 2 ) + ( F ^ 2 ) ) e. S )
284 268 283 eqeltrd 
 |-  ( ph -> ( M x. ( ( ( E ^ 2 ) + ( F ^ 2 ) ) / M ) ) e. S )
285 1 17 201 280 284 2sqlem6 
 |-  ( ph -> M e. S )