Metamath Proof Explorer


Theorem 4sqlem11

Description: Lemma for 4sq . Use the pigeonhole principle to show that the sets { m ^ 2 | m e. ( 0 ... N ) } and { -u 1 - n ^ 2 | n e. ( 0 ... N ) } have a common element, mod P . (Contributed by Mario Carneiro, 15-Jul-2014)

Ref Expression
Hypotheses 4sq.1 S = n | x y z w n = x 2 + y 2 + z 2 + w 2
4sq.2 φ N
4sq.3 φ P = 2 N + 1
4sq.4 φ P
4sqlem11.5 A = u | m 0 N u = m 2 mod P
4sqlem11.6 F = v A P - 1 - v
Assertion 4sqlem11 φ A ran F

Proof

Step Hyp Ref Expression
1 4sq.1 S = n | x y z w n = x 2 + y 2 + z 2 + w 2
2 4sq.2 φ N
3 4sq.3 φ P = 2 N + 1
4 4sq.4 φ P
5 4sqlem11.5 A = u | m 0 N u = m 2 mod P
6 4sqlem11.6 F = v A P - 1 - v
7 fzfid φ 0 P 1 Fin
8 elfzelz m 0 N m
9 zsqcl m m 2
10 8 9 syl m 0 N m 2
11 prmnn P P
12 4 11 syl φ P
13 zmodfz m 2 P m 2 mod P 0 P 1
14 10 12 13 syl2anr φ m 0 N m 2 mod P 0 P 1
15 eleq1a m 2 mod P 0 P 1 u = m 2 mod P u 0 P 1
16 14 15 syl φ m 0 N u = m 2 mod P u 0 P 1
17 16 rexlimdva φ m 0 N u = m 2 mod P u 0 P 1
18 17 abssdv φ u | m 0 N u = m 2 mod P 0 P 1
19 5 18 eqsstrid φ A 0 P 1
20 prmz P P
21 4 20 syl φ P
22 peano2zm P P 1
23 21 22 syl φ P 1
24 23 zcnd φ P 1
25 24 addid2d φ 0 + P - 1 = P 1
26 25 oveq1d φ 0 + P 1 - v = P - 1 - v
27 26 adantr φ v A 0 + P 1 - v = P - 1 - v
28 19 sselda φ v A v 0 P 1
29 fzrev3i v 0 P 1 0 + P 1 - v 0 P 1
30 28 29 syl φ v A 0 + P 1 - v 0 P 1
31 27 30 eqeltrrd φ v A P - 1 - v 0 P 1
32 31 6 fmptd φ F : A 0 P 1
33 32 frnd φ ran F 0 P 1
34 19 33 unssd φ A ran F 0 P 1
35 7 34 ssfid φ A ran F Fin
36 hashcl A ran F Fin A ran F 0
37 35 36 syl φ A ran F 0
38 37 nn0red φ A ran F
39 21 zred φ P
40 ssdomg 0 P 1 Fin A ran F 0 P 1 A ran F 0 P 1
41 7 34 40 sylc φ A ran F 0 P 1
42 hashdom A ran F Fin 0 P 1 Fin A ran F 0 P 1 A ran F 0 P 1
43 35 7 42 syl2anc φ A ran F 0 P 1 A ran F 0 P 1
44 41 43 mpbird φ A ran F 0 P 1
45 fz01en P 0 P 1 1 P
46 21 45 syl φ 0 P 1 1 P
47 fzfid φ 1 P Fin
48 hashen 0 P 1 Fin 1 P Fin 0 P 1 = 1 P 0 P 1 1 P
49 7 47 48 syl2anc φ 0 P 1 = 1 P 0 P 1 1 P
50 46 49 mpbird φ 0 P 1 = 1 P
51 12 nnnn0d φ P 0
52 hashfz1 P 0 1 P = P
53 51 52 syl φ 1 P = P
54 50 53 eqtrd φ 0 P 1 = P
55 44 54 breqtrd φ A ran F P
56 38 39 55 lensymd φ ¬ P < A ran F
57 39 adantr φ A ran F = P
58 57 ltp1d φ A ran F = P < P + 1
59 2 nncnd φ N
60 1cnd φ 1
61 59 59 60 60 add4d φ N + N + 1 + 1 = N + 1 + N + 1
62 3 oveq1d φ P + 1 = 2 N + 1 + 1
63 2cn 2
64 mulcl 2 N 2 N
65 63 59 64 sylancr φ 2 N
66 65 60 60 addassd φ 2 N + 1 + 1 = 2 N + 1 + 1
67 59 2timesd φ 2 N = N + N
68 67 oveq1d φ 2 N + 1 + 1 = N + N + 1 + 1
69 62 66 68 3eqtrd φ P + 1 = N + N + 1 + 1
70 14 ex φ m 0 N m 2 mod P 0 P 1
71 12 adantr φ m 0 N u 0 N P
72 8 ad2antrl φ m 0 N u 0 N m
73 72 9 syl φ m 0 N u 0 N m 2
74 elfzelz u 0 N u
75 74 ad2antll φ m 0 N u 0 N u
76 zsqcl u u 2
77 75 76 syl φ m 0 N u 0 N u 2
78 moddvds P m 2 u 2 m 2 mod P = u 2 mod P P m 2 u 2
79 71 73 77 78 syl3anc φ m 0 N u 0 N m 2 mod P = u 2 mod P P m 2 u 2
80 72 zcnd φ m 0 N u 0 N m
81 75 zcnd φ m 0 N u 0 N u
82 subsq m u m 2 u 2 = m + u m u
83 80 81 82 syl2anc φ m 0 N u 0 N m 2 u 2 = m + u m u
84 83 breq2d φ m 0 N u 0 N P m 2 u 2 P m + u m u
85 4 adantr φ m 0 N u 0 N P
86 72 75 zaddcld φ m 0 N u 0 N m + u
87 72 75 zsubcld φ m 0 N u 0 N m u
88 euclemma P m + u m u P m + u m u P m + u P m u
89 85 86 87 88 syl3anc φ m 0 N u 0 N P m + u m u P m + u P m u
90 79 84 89 3bitrd φ m 0 N u 0 N m 2 mod P = u 2 mod P P m + u P m u
91 86 zred φ m 0 N u 0 N m + u
92 2re 2
93 2 nnred φ N
94 remulcl 2 N 2 N
95 92 93 94 sylancr φ 2 N
96 95 adantr φ m 0 N u 0 N 2 N
97 85 20 syl φ m 0 N u 0 N P
98 97 zred φ m 0 N u 0 N P
99 72 zred φ m 0 N u 0 N m
100 75 zred φ m 0 N u 0 N u
101 93 adantr φ m 0 N u 0 N N
102 elfzle2 m 0 N m N
103 102 ad2antrl φ m 0 N u 0 N m N
104 elfzle2 u 0 N u N
105 104 ad2antll φ m 0 N u 0 N u N
106 99 100 101 101 103 105 le2addd φ m 0 N u 0 N m + u N + N
107 59 adantr φ m 0 N u 0 N N
108 107 2timesd φ m 0 N u 0 N 2 N = N + N
109 106 108 breqtrrd φ m 0 N u 0 N m + u 2 N
110 95 ltp1d φ 2 N < 2 N + 1
111 110 3 breqtrrd φ 2 N < P
112 111 adantr φ m 0 N u 0 N 2 N < P
113 91 96 98 109 112 lelttrd φ m 0 N u 0 N m + u < P
114 91 98 ltnled φ m 0 N u 0 N m + u < P ¬ P m + u
115 113 114 mpbid φ m 0 N u 0 N ¬ P m + u
116 115 adantr φ m 0 N u 0 N m u ¬ P m + u
117 21 ad2antrr φ m 0 N u 0 N m u P
118 86 adantr φ m 0 N u 0 N m u m + u
119 1red φ m 0 N u 0 N m u 1
120 nn0abscl m u m u 0
121 87 120 syl φ m 0 N u 0 N m u 0
122 121 nn0red φ m 0 N u 0 N m u
123 122 adantr φ m 0 N u 0 N m u m u
124 118 zred φ m 0 N u 0 N m u m + u
125 121 adantr φ m 0 N u 0 N m u m u 0
126 125 nn0zd φ m 0 N u 0 N m u m u
127 87 zcnd φ m 0 N u 0 N m u
128 127 adantr φ m 0 N u 0 N m u m u
129 80 81 subeq0ad φ m 0 N u 0 N m u = 0 m = u
130 129 necon3bid φ m 0 N u 0 N m u 0 m u
131 130 biimpar φ m 0 N u 0 N m u m u 0
132 128 131 absrpcld φ m 0 N u 0 N m u m u +
133 132 rpgt0d φ m 0 N u 0 N m u 0 < m u
134 elnnz m u m u 0 < m u
135 126 133 134 sylanbrc φ m 0 N u 0 N m u m u
136 135 nnge1d φ m 0 N u 0 N m u 1 m u
137 0cnd φ m 0 N u 0 N 0
138 80 81 137 abs3difd φ m 0 N u 0 N m u m 0 + 0 u
139 80 subid1d φ m 0 N u 0 N m 0 = m
140 139 fveq2d φ m 0 N u 0 N m 0 = m
141 elfzle1 m 0 N 0 m
142 141 ad2antrl φ m 0 N u 0 N 0 m
143 99 142 absidd φ m 0 N u 0 N m = m
144 140 143 eqtrd φ m 0 N u 0 N m 0 = m
145 0cn 0
146 abssub 0 u 0 u = u 0
147 145 81 146 sylancr φ m 0 N u 0 N 0 u = u 0
148 81 subid1d φ m 0 N u 0 N u 0 = u
149 148 fveq2d φ m 0 N u 0 N u 0 = u
150 elfzle1 u 0 N 0 u
151 150 ad2antll φ m 0 N u 0 N 0 u
152 100 151 absidd φ m 0 N u 0 N u = u
153 147 149 152 3eqtrd φ m 0 N u 0 N 0 u = u
154 144 153 oveq12d φ m 0 N u 0 N m 0 + 0 u = m + u
155 138 154 breqtrd φ m 0 N u 0 N m u m + u
156 155 adantr φ m 0 N u 0 N m u m u m + u
157 119 123 124 136 156 letrd φ m 0 N u 0 N m u 1 m + u
158 elnnz1 m + u m + u 1 m + u
159 118 157 158 sylanbrc φ m 0 N u 0 N m u m + u
160 dvdsle P m + u P m + u P m + u
161 117 159 160 syl2anc φ m 0 N u 0 N m u P m + u P m + u
162 116 161 mtod φ m 0 N u 0 N m u ¬ P m + u
163 162 ex φ m 0 N u 0 N m u ¬ P m + u
164 163 necon4ad φ m 0 N u 0 N P m + u m = u
165 dvdsabsb P m u P m u P m u
166 97 87 165 syl2anc φ m 0 N u 0 N P m u P m u
167 letr P m u m + u P m u m u m + u P m + u
168 98 122 91 167 syl3anc φ m 0 N u 0 N P m u m u m + u P m + u
169 155 168 mpan2d φ m 0 N u 0 N P m u P m + u
170 115 169 mtod φ m 0 N u 0 N ¬ P m u
171 170 adantr φ m 0 N u 0 N m u ¬ P m u
172 97 adantr φ m 0 N u 0 N m u P
173 dvdsle P m u P m u P m u
174 172 135 173 syl2anc φ m 0 N u 0 N m u P m u P m u
175 171 174 mtod φ m 0 N u 0 N m u ¬ P m u
176 175 ex φ m 0 N u 0 N m u ¬ P m u
177 176 necon4ad φ m 0 N u 0 N P m u m = u
178 166 177 sylbid φ m 0 N u 0 N P m u m = u
179 164 178 jaod φ m 0 N u 0 N P m + u P m u m = u
180 90 179 sylbid φ m 0 N u 0 N m 2 mod P = u 2 mod P m = u
181 oveq1 m = u m 2 = u 2
182 181 oveq1d m = u m 2 mod P = u 2 mod P
183 180 182 impbid1 φ m 0 N u 0 N m 2 mod P = u 2 mod P m = u
184 183 ex φ m 0 N u 0 N m 2 mod P = u 2 mod P m = u
185 70 184 dom2lem φ m 0 N m 2 mod P : 0 N 1-1 0 P 1
186 f1f1orn m 0 N m 2 mod P : 0 N 1-1 0 P 1 m 0 N m 2 mod P : 0 N 1-1 onto ran m 0 N m 2 mod P
187 185 186 syl φ m 0 N m 2 mod P : 0 N 1-1 onto ran m 0 N m 2 mod P
188 eqid m 0 N m 2 mod P = m 0 N m 2 mod P
189 188 rnmpt ran m 0 N m 2 mod P = u | m 0 N u = m 2 mod P
190 5 189 eqtr4i A = ran m 0 N m 2 mod P
191 f1oeq3 A = ran m 0 N m 2 mod P m 0 N m 2 mod P : 0 N 1-1 onto A m 0 N m 2 mod P : 0 N 1-1 onto ran m 0 N m 2 mod P
192 190 191 ax-mp m 0 N m 2 mod P : 0 N 1-1 onto A m 0 N m 2 mod P : 0 N 1-1 onto ran m 0 N m 2 mod P
193 187 192 sylibr φ m 0 N m 2 mod P : 0 N 1-1 onto A
194 ovex 0 N V
195 194 f1oen m 0 N m 2 mod P : 0 N 1-1 onto A 0 N A
196 193 195 syl φ 0 N A
197 196 ensymd φ A 0 N
198 ax-1cn 1
199 pncan N 1 N + 1 - 1 = N
200 59 198 199 sylancl φ N + 1 - 1 = N
201 200 oveq2d φ 0 N + 1 - 1 = 0 N
202 2 nnnn0d φ N 0
203 peano2nn0 N 0 N + 1 0
204 202 203 syl φ N + 1 0
205 204 nn0zd φ N + 1
206 fz01en N + 1 0 N + 1 - 1 1 N + 1
207 205 206 syl φ 0 N + 1 - 1 1 N + 1
208 201 207 eqbrtrrd φ 0 N 1 N + 1
209 entr A 0 N 0 N 1 N + 1 A 1 N + 1
210 197 208 209 syl2anc φ A 1 N + 1
211 7 19 ssfid φ A Fin
212 fzfid φ 1 N + 1 Fin
213 hashen A Fin 1 N + 1 Fin A = 1 N + 1 A 1 N + 1
214 211 212 213 syl2anc φ A = 1 N + 1 A 1 N + 1
215 210 214 mpbird φ A = 1 N + 1
216 hashfz1 N + 1 0 1 N + 1 = N + 1
217 204 216 syl φ 1 N + 1 = N + 1
218 215 217 eqtrd φ A = N + 1
219 31 ex φ v A P - 1 - v 0 P 1
220 24 adantr φ v A k A P 1
221 fzssuz 0 P 1 0
222 uzssz 0
223 zsscn
224 222 223 sstri 0
225 221 224 sstri 0 P 1
226 19 225 sstrdi φ A
227 226 sselda φ v A v
228 227 adantrr φ v A k A v
229 226 sselda φ k A k
230 229 adantrl φ v A k A k
231 220 228 230 subcanad φ v A k A P - 1 - v = P - 1 - k v = k
232 231 ex φ v A k A P - 1 - v = P - 1 - k v = k
233 219 232 dom2lem φ v A P - 1 - v : A 1-1 0 P 1
234 f1eq1 F = v A P - 1 - v F : A 1-1 0 P 1 v A P - 1 - v : A 1-1 0 P 1
235 6 234 ax-mp F : A 1-1 0 P 1 v A P - 1 - v : A 1-1 0 P 1
236 233 235 sylibr φ F : A 1-1 0 P 1
237 f1f1orn F : A 1-1 0 P 1 F : A 1-1 onto ran F
238 236 237 syl φ F : A 1-1 onto ran F
239 211 238 hasheqf1od φ A = ran F
240 239 218 eqtr3d φ ran F = N + 1
241 218 240 oveq12d φ A + ran F = N + 1 + N + 1
242 61 69 241 3eqtr4d φ P + 1 = A + ran F
243 242 adantr φ A ran F = P + 1 = A + ran F
244 211 adantr φ A ran F = A Fin
245 7 33 ssfid φ ran F Fin
246 245 adantr φ A ran F = ran F Fin
247 simpr φ A ran F = A ran F =
248 hashun A Fin ran F Fin A ran F = A ran F = A + ran F
249 244 246 247 248 syl3anc φ A ran F = A ran F = A + ran F
250 243 249 eqtr4d φ A ran F = P + 1 = A ran F
251 58 250 breqtrd φ A ran F = P < A ran F
252 251 ex φ A ran F = P < A ran F
253 252 necon3bd φ ¬ P < A ran F A ran F
254 56 253 mpd φ A ran F