MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  4sqlem11 Unicode version

Theorem 4sqlem11 14473
Description: Lemma for 4sq 14482. Use the pigeonhole principle to show that the sets { 2| e.(0 N)} and {-u1 2| e.(0 N)} have a common element, P. (Contributed by Mario Carneiro, 15-Jul-2014.)
Hypotheses
Ref Expression
4sq.1
4sq.2
4sq.3
4sq.4
4sqlem11.5
4sqlem11.6
Assertion
Ref Expression
4sqlem11
Distinct variable groups:   , , , ,   , ,   ,   , , , ,N   P, , , ,   , , , ,   S, , , ,

Proof of Theorem 4sqlem11
Dummy variable is distinct from all other variables.
StepHypRef Expression
1 fzfid 12083 . . . . . 6
2 4sqlem11.5 . . . . . . . 8
3 elfzelz 11717 . . . . . . . . . . . . 13
4 zsqcl 12238 . . . . . . . . . . . . 13
53, 4syl 16 . . . . . . . . . . . 12
6 4sq.4 . . . . . . . . . . . . 13
7 prmnn 14220 . . . . . . . . . . . . 13
86, 7syl 16 . . . . . . . . . . . 12
9 zmodfz 12017 . . . . . . . . . . . 12
105, 8, 9syl2anr 478 . . . . . . . . . . 11
11 eleq1a 2540 . . . . . . . . . . 11
1210, 11syl 16 . . . . . . . . . 10
1312rexlimdva 2949 . . . . . . . . 9
1413abssdv 3573 . . . . . . . 8
152, 14syl5eqss 3547 . . . . . . 7
16 prmz 14221 . . . . . . . . . . . . . . . 16
176, 16syl 16 . . . . . . . . . . . . . . 15
18 peano2zm 10932 . . . . . . . . . . . . . . 15
1917, 18syl 16 . . . . . . . . . . . . . 14
2019zcnd 10995 . . . . . . . . . . . . 13
2120addid2d 9802 . . . . . . . . . . . 12
2221oveq1d 6311 . . . . . . . . . . 11
2322adantr 465 . . . . . . . . . 10
2415sselda 3503 . . . . . . . . . . 11
25 fzrev3i 11775 . . . . . . . . . . 11
2624, 25syl 16 . . . . . . . . . 10
2723, 26eqeltrrd 2546 . . . . . . . . 9
28 4sqlem11.6 . . . . . . . . 9
2927, 28fmptd 6055 . . . . . . . 8
30 frn 5742 . . . . . . . 8
3129, 30syl 16 . . . . . . 7
3215, 31unssd 3679 . . . . . 6
33 ssdomg 7581 . . . . . 6
341, 32, 33sylc 60 . . . . 5
35 ssfi 7760 . . . . . . 7
361, 32, 35syl2anc 661 . . . . . 6
37 hashdom 12447 . . . . . 6
3836, 1, 37syl2anc 661 . . . . 5
3934, 38mpbird 232 . . . 4
40 fz01en 11742 . . . . . . 7
4117, 40syl 16 . . . . . 6
42 fzfid 12083 . . . . . . 7
43 hashen 12420 . . . . . . 7
441, 42, 43syl2anc 661 . . . . . 6
4541, 44mpbird 232 . . . . 5
468nnnn0d 10877 . . . . . 6
47 hashfz1 12419 . . . . . 6
4846, 47syl 16 . . . . 5
4945, 48eqtrd 2498 . . . 4
5039, 49breqtrd 4476 . . 3
51 hashcl 12428 . . . . . 6
5236, 51syl 16 . . . . 5
5352nn0red 10878 . . . 4
5417zred 10994 . . . 4
5553, 54lenltd 9752 . . 3
5650, 55mpbid 210 . 2
5754adantr 465 . . . . . 6
5857ltp1d 10501 . . . . 5
59 4sq.2 . . . . . . . . . 10
6059nncnd 10577 . . . . . . . . 9
61 1cnd 9633 . . . . . . . . 9
6260, 60, 61, 61add4d 9826 . . . . . . . 8
63 4sq.3 . . . . . . . . . 10
6463oveq1d 6311 . . . . . . . . 9
65 2cn 10631 . . . . . . . . . . 11
66 mulcl 9597 . . . . . . . . . . 11
6765, 60, 66sylancr 663 . . . . . . . . . 10
6867, 61, 61addassd 9639 . . . . . . . . 9
69602timesd 10806 . . . . . . . . . 10
7069oveq1d 6311 . . . . . . . . 9
7164, 68, 703eqtrd 2502 . . . . . . . 8
7210ex 434 . . . . . . . . . . . . . . . . 17
738adantr 465 . . . . . . . . . . . . . . . . . . . . . 22
743ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . 23
7574, 4syl 16 . . . . . . . . . . . . . . . . . . . . . 22
76 elfzelz 11717 . . . . . . . . . . . . . . . . . . . . . . . 24
7776ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . 23
78 zsqcl 12238 . . . . . . . . . . . . . . . . . . . . . . 23
7977, 78syl 16 . . . . . . . . . . . . . . . . . . . . . 22
80 moddvds 13993 . . . . . . . . . . . . . . . . . . . . . 22
8173, 75, 79, 80syl3anc 1228 . . . . . . . . . . . . . . . . . . . . 21
8274zcnd 10995 . . . . . . . . . . . . . . . . . . . . . . 23
8377zcnd 10995 . . . . . . . . . . . . . . . . . . . . . . 23
84 subsq 12275 . . . . . . . . . . . . . . . . . . . . . . 23
8582, 83, 84syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22
8685breq2d 4464 . . . . . . . . . . . . . . . . . . . . 21
876adantr 465 . . . . . . . . . . . . . . . . . . . . . 22
8874, 77zaddcld 10998 . . . . . . . . . . . . . . . . . . . . . 22
8974, 77zsubcld 10999 . . . . . . . . . . . . . . . . . . . . . 22
90 euclemma 14249 . . . . . . . . . . . . . . . . . . . . . 22
9187, 88, 89, 90syl3anc 1228 . . . . . . . . . . . . . . . . . . . . 21
9281, 86, 913bitrd 279 . . . . . . . . . . . . . . . . . . . 20
9388zred 10994 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
94 2re 10630 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9559nnred 10576 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
96 remulcl 9598 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
9794, 95, 96sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
9897adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
9987, 16syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
10099zred 10994 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
10174zred 10994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
10277zred 10994 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
10395adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
104 elfzle2 11719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
105104ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
106 elfzle2 11719 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
107106ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
108101, 102, 103, 103, 105, 107le2addd 10195 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
10960adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
1101092timesd 10806 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
111108, 110breqtrrd 4478 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
11297ltp1d 10501 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
113112, 63breqtrrd 4478 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
114113adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
11593, 98, 100, 111, 114lelttrd 9761 . . . . . . . . . . . . . . . . . . . . . . . . . 26
11693, 100ltnled 9753 . . . . . . . . . . . . . . . . . . . . . . . . . 26
117115, 116mpbid 210 . . . . . . . . . . . . . . . . . . . . . . . . 25
118117adantr 465 . . . . . . . . . . . . . . . . . . . . . . . 24
11917ad2antrr 725 . . . . . . . . . . . . . . . . . . . . . . . . 25
12088adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
121 1red 9632 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
122 nn0abscl 13145 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
12389, 122syl 16 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
124123nn0red 10878 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
125124adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
126120zred 10994 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
127123adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
128127nn0zd 10992 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
12989zcnd 10995 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
130129adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
13182, 83subeq0ad 9964 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
132131necon3bid 2715 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
133132biimpar 485 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
134130, 133absrpcld 13279 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
135134rpgt0d 11288 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
136 elnnz 10899 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
137128, 135, 136sylanbrc 664 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
138137nnge1d 10603 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
139 0cnd 9610 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
14082, 83, 139abs3difd 13291 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
14182subid1d 9943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
142141fveq2d 5875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
143 elfzle1 11718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
144143ad2antrl 727 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
145101, 144absidd 13254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
146142, 145eqtrd 2498 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
147 0cn 9609 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
148 abssub 13159 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
149147, 83, 148sylancr 663 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
15083subid1d 9943 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
151150fveq2d 5875 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
152 elfzle1 11718 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33
153152ad2antll 728 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
154102, 153absidd 13254 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
155149, 151, 1543eqtrd 2502 . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
156146, 155oveq12d 6314 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
157140, 156breqtrd 4476 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
158157adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
159121, 125, 126, 138, 158letrd 9760 . . . . . . . . . . . . . . . . . . . . . . . . . 26
160 elnnz1 10915 . . . . . . . . . . . . . . . . . . . . . . . . . 26
161120, 159, 160sylanbrc 664 . . . . . . . . . . . . . . . . . . . . . . . . 25
162 dvdsle 14031 . . . . . . . . . . . . . . . . . . . . . . . . 25
163119, 161, 162syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . 24
164118, 163mtod 177 . . . . . . . . . . . . . . . . . . . . . . 23
165164ex 434 . . . . . . . . . . . . . . . . . . . . . 22
166165necon4ad 2677 . . . . . . . . . . . . . . . . . . . . 21
167 dvdsabsb 14003 . . . . . . . . . . . . . . . . . . . . . . 23
16899, 89, 167syl2anc 661 . . . . . . . . . . . . . . . . . . . . . 22
169 letr 9699 . . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
170100, 124, 93, 169syl3anc 1228 . . . . . . . . . . . . . . . . . . . . . . . . . . . 28
171157, 170mpan2d 674 . . . . . . . . . . . . . . . . . . . . . . . . . . 27
172117, 171mtod 177 . . . . . . . . . . . . . . . . . . . . . . . . . 26
173172adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . 25
17499adantr 465 . . . . . . . . . . . . . . . . . . . . . . . . . 26
175 dvdsle 14031 . . . . . . . . . . . . . . . . . . . . . . . . . 26
176174, 137, 175syl2anc 661 . . . . . . . . . . . . . . . . . . . . . . . . 25
177173, 176mtod 177 . . . . . . . . . . . . . . . . . . . . . . . 24
178177ex 434 . . . . . . . . . . . . . . . . . . . . . . 23
179178necon4ad 2677 . . . . . . . . . . . . . . . . . . . . . 22
180168, 179sylbid 215 . . . . . . . . . . . . . . . . . . . . 21
181166, 180jaod 380 . . . . . . . . . . . . . . . . . . . 20
18292, 181sylbid 215 . . . . . . . . . . . . . . . . . . 19
183 oveq1 6303 . . . . . . . . . . . . . . . . . . . 20
184183oveq1d 6311 . . . . . . . . . . . . . . . . . . 19
185182, 184impbid1 203 . . . . . . . . . . . . . . . . . 18
186185ex 434 . . . . . . . . . . . . . . . . 17
18772, 186dom2lem 7575 . . . . . . . . . . . . . . . 16
188 f1f1orn 5832 . . . . . . . . . . . . . . . 16
189187, 188syl 16 . . . . . . . . . . . . . . 15
190 eqid 2457 . . . . . . . . . . . . . . . . . 18
191190rnmpt 5253 . . . . . . . . . . . . . . . . 17
1922, 191eqtr4i 2489 . . . . . . . . . . . . . . . 16
193 f1oeq3 5814 . . . . . . . . . . . . . . . 16
194192, 193ax-mp 5 . . . . . . . . . . . . . . 15
195189, 194sylibr 212 . . . . . . . . . . . . . 14
196 ovex 6324 . . . . . . . . . . . . . . 15
197196f1oen 7556 . . . . . . . . . . . . . 14
198195, 197syl 16 . . . . . . . . . . . . 13
199198ensymd 7586 . . . . . . . . . . . 12
200 ax-1cn 9571 . . . . . . . . . . . . . . 15
201 pncan 9849 . . . . . . . . . . . . . . 15
20260, 200, 201sylancl 662 . . . . . . . . . . . . . 14
203202oveq2d 6312 . . . . . . . . . . . . 13
20459nnnn0d 10877 . . . . . . . . . . . . . . . 16
205 peano2nn0 10861 . . . . . . . . . . . . . . . 16
206204, 205syl 16 . . . . . . . . . . . . . . 15
207206nn0zd 10992 . . . . . . . . . . . . . 14
208 fz01en 11742 . . . . . . . . . . . . . 14
209207, 208syl 16 . . . . . . . . . . . . 13
210203, 209eqbrtrrd 4474 . . . . . . . . . . . 12
211 entr 7587 . . . . . . . . . . . 12
212199, 210, 211syl2anc 661 . . . . . . . . . . 11
213 ssfi 7760 . . . . . . . . . . . . 13
2141, 15, 213syl2anc 661 . . . . . . . . . . . 12
215 fzfid 12083 . . . . . . . . . . . 12
216 hashen 12420 . . . . . . . . . . . 12
217214, 215, 216syl2anc 661 . . . . . . . . . . 11
218212, 217mpbird 232 . . . . . . . . . 10
219 hashfz1 12419 . . . . . . . . . . 11
220206, 219syl 16 . . . . . . . . . 10
221218, 220eqtrd 2498 . . . . . . . . 9
22227ex 434 . . . . . . . . . . . . . . 15
22320adantr 465 . . . . . . . . . . . . . . . . 17
224 fzssuz 11753 . . . . . . . . . . . . . . . . . . . . 21
225 uzssz 11129 . . . . . . . . . . . . . . . . . . . . . 22
226 zsscn 10897 . . . . . . . . . . . . . . . . . . . . . 22
227225, 226sstri 3512 . . . . . . . . . . . . . . . . . . . . 21
228224, 227sstri 3512 . . . . . . . . . . . . . . . . . . . 20
22915, 228syl6ss 3515 . . . . . . . . . . . . . . . . . . 19
230229sselda 3503 . . . . . . . . . . . . . . . . . 18
231230adantrr 716 . . . . . . . . . . . . . . . . 17
232229sselda 3503 . . . . . . . . . . . . . . . . . 18
233232adantrl 715 . . . . . . . . . . . . . . . . 17
234223, 231, 233subcanad 9997 . . . . . . . . . . . . . . . 16
235234ex 434 . . . . . . . . . . . . . . 15
236222, 235dom2lem 7575 . . . . . . . . . . . . . 14
237 f1eq1 5781 . . . . . . . . . . . . . . 15
23828, 237ax-mp 5 . . . . . . . . . . . . . 14
239236, 238sylibr 212 . . . . . . . . . . . . 13
240 f1f1orn 5832 . . . . . . . . . . . . 13
241239, 240syl 16 . . . . . . . . . . . 12
242 f1oeng 7554 . . . . . . . . . . . 12
243214, 241, 242syl2anc 661 . . . . . . . . . . 11
244 ssfi 7760 . . . . . . . . . . . . 13
2451, 31, 244syl2anc 661 . . . . . . . . . . . 12
246 hashen 12420 . . . . . . . . . . . 12
247214, 245, 246syl2anc 661 . . . . . . . . . . 11
248243, 247mpbird 232 . . . . . . . . . 10
249248, 221eqtr3d 2500 . . . . . . . . 9
250221, 249oveq12d 6314 . . . . . . . 8