Intuitionistic Logic Explorer < Previous   Next > Nearby theorems Mirrors  >  Home  >  ILE Home  >  Th. List  >  hashdvds Unicode version

Theorem hashdvds 11931
 Description: The number of numbers in a given residue class in a finite set of integers. (Contributed by Mario Carneiro, 12-Mar-2014.) (Proof shortened by Mario Carneiro, 7-Jun-2016.)
Hypotheses
Ref Expression
hashdvds.1
hashdvds.2
hashdvds.3
hashdvds.4
Assertion
Ref Expression
hashdvds
Distinct variable groups:   ,   ,   ,   ,
Allowed substitution hint:   ()

Proof of Theorem hashdvds
Dummy variables are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 1zzd 9104 . . . . . 6
2 hashdvds.3 . . . . . . . . . . 11
3 eluzelz 9358 . . . . . . . . . . 11
42, 3syl 14 . . . . . . . . . 10
5 hashdvds.4 . . . . . . . . . 10
64, 5zsubcld 9201 . . . . . . . . 9
7 hashdvds.1 . . . . . . . . 9
8 znq 9442 . . . . . . . . 9
96, 7, 8syl2anc 409 . . . . . . . 8
109flqcld 10080 . . . . . . 7
11 hashdvds.2 . . . . . . . . . . 11
12 peano2zm 9115 . . . . . . . . . . 11
1311, 12syl 14 . . . . . . . . . 10
1413, 5zsubcld 9201 . . . . . . . . 9
15 znq 9442 . . . . . . . . 9
1614, 7, 15syl2anc 409 . . . . . . . 8
1716flqcld 10080 . . . . . . 7
1810, 17zsubcld 9201 . . . . . 6
19 fzen 9853 . . . . . 6
201, 18, 17, 19syl3anc 1217 . . . . 5
21 ax-1cn 7736 . . . . . . 7
2217zcnd 9197 . . . . . . 7
23 addcom 7922 . . . . . . 7
2421, 22, 23sylancr 411 . . . . . 6
2510zcnd 9197 . . . . . . 7
2625, 22npcand 8100 . . . . . 6
2724, 26oveq12d 5799 . . . . 5
2820, 27breqtrd 3961 . . . 4
2917peano2zd 9199 . . . . . . 7
3029, 10fzfigd 10234 . . . . . 6
3130elexd 2702 . . . . 5
3211, 4fzfigd 10234 . . . . . . 7
33 elfzelz 9836 . . . . . . . . . . . 12
3433adantl 275 . . . . . . . . . . 11
355adantr 274 . . . . . . . . . . 11
3634, 35zsubcld 9201 . . . . . . . . . 10
37 dvdsdc 11535 . . . . . . . . . 10 DECID
387, 36, 37syl2an2r 585 . . . . . . . . 9 DECID
3938ralrimiva 2508 . . . . . . . 8 DECID
40 oveq1 5788 . . . . . . . . . . 11
4140breq2d 3948 . . . . . . . . . 10
4241dcbid 824 . . . . . . . . 9 DECID DECID
4342cbvralv 2657 . . . . . . . 8 DECID DECID
4439, 43sylibr 133 . . . . . . 7 DECID
4532, 44ssfirab 6829 . . . . . 6
4645elexd 2702 . . . . 5
47 elfzle1 9837 . . . . . . . . . . . . . 14
4847adantl 275 . . . . . . . . . . . . 13
49 elfzelz 9836 . . . . . . . . . . . . . 14
50 zltp1le 9131 . . . . . . . . . . . . . 14
5117, 49, 50syl2an 287 . . . . . . . . . . . . 13
5248, 51mpbird 166 . . . . . . . . . . . 12
53 flqlt 10086 . . . . . . . . . . . . 13
5416, 49, 53syl2an 287 . . . . . . . . . . . 12
5552, 54mpbird 166 . . . . . . . . . . 11
5614zred 9196 . . . . . . . . . . . . 13
5756adantr 274 . . . . . . . . . . . 12
5849adantl 275 . . . . . . . . . . . . 13
5958zred 9196 . . . . . . . . . . . 12
607nnred 8756 . . . . . . . . . . . . . 14
617nngt0d 8787 . . . . . . . . . . . . . 14
6260, 61jca 304 . . . . . . . . . . . . 13
6362adantr 274 . . . . . . . . . . . 12
64 ltdivmul2 8659 . . . . . . . . . . . 12
6557, 59, 63, 64syl3anc 1217 . . . . . . . . . . 11
6655, 65mpbid 146 . . . . . . . . . 10
6713zred 9196 . . . . . . . . . . . 12
6867adantr 274 . . . . . . . . . . 11
695zred 9196 . . . . . . . . . . . 12
7069adantr 274 . . . . . . . . . . 11
717nnzd 9195 . . . . . . . . . . . . . 14
7271adantr 274 . . . . . . . . . . . . 13
7358, 72zmulcld 9202 . . . . . . . . . . . 12
7473zred 9196 . . . . . . . . . . 11
7568, 70, 74ltsubaddd 8326 . . . . . . . . . 10
7666, 75mpbid 146 . . . . . . . . 9
775adantr 274 . . . . . . . . . . 11
7873, 77zaddcld 9200 . . . . . . . . . 10
79 zlem1lt 9133 . . . . . . . . . 10
8011, 78, 79syl2an2r 585 . . . . . . . . 9
8176, 80mpbird 166 . . . . . . . 8
82 elfzle2 9838 . . . . . . . . . . . 12
8382adantl 275 . . . . . . . . . . 11
84 flqge 10085 . . . . . . . . . . . 12
859, 49, 84syl2an 287 . . . . . . . . . . 11
8683, 85mpbird 166 . . . . . . . . . 10
876zred 9196 . . . . . . . . . . . 12
8887adantr 274 . . . . . . . . . . 11
89 lemuldiv 8662 . . . . . . . . . . 11
9059, 88, 63, 89syl3anc 1217 . . . . . . . . . 10
9186, 90mpbird 166 . . . . . . . . 9
924zred 9196 . . . . . . . . . . 11
9392adantr 274 . . . . . . . . . 10
94 leaddsub 8223 . . . . . . . . . 10
9574, 70, 93, 94syl3anc 1217 . . . . . . . . 9
9691, 95mpbird 166 . . . . . . . 8
9711adantr 274 . . . . . . . . 9
984adantr 274 . . . . . . . . 9
99 elfz 9826 . . . . . . . . 9
10078, 97, 98, 99syl3anc 1217 . . . . . . . 8
10181, 96, 100mpbir2and 929 . . . . . . 7
102 dvdsmul2 11550 . . . . . . . . 9
10358, 72, 102syl2anc 409 . . . . . . . 8
10473zcnd 9197 . . . . . . . . 9
1055zcnd 9197 . . . . . . . . . 10
106105adantr 274 . . . . . . . . 9
107104, 106pncand 8097 . . . . . . . 8
108103, 107breqtrrd 3963 . . . . . . 7
109 oveq1 5788 . . . . . . . . 9
110109breq2d 3948 . . . . . . . 8
111110elrab 2843 . . . . . . 7
112101, 108, 111sylanbrc 414 . . . . . 6
113112ex 114 . . . . 5
114 oveq1 5788 . . . . . . . 8
115114breq2d 3948 . . . . . . 7
116115elrab 2843 . . . . . 6
11767adantr 274 . . . . . . . . . . . 12
118 elfzelz 9836 . . . . . . . . . . . . . 14
119118ad2antrl 482 . . . . . . . . . . . . 13
120119zred 9196 . . . . . . . . . . . 12
12169adantr 274 . . . . . . . . . . . 12
122 elfzle1 9837 . . . . . . . . . . . . . 14
123122ad2antrl 482 . . . . . . . . . . . . 13
124 zlem1lt 9133 . . . . . . . . . . . . . 14
12511, 119, 124syl2an2r 585 . . . . . . . . . . . . 13
126123, 125mpbid 146 . . . . . . . . . . . 12
127117, 120, 121, 126ltsub1dd 8342 . . . . . . . . . . 11
12856adantr 274 . . . . . . . . . . . 12
1295adantr 274 . . . . . . . . . . . . . 14
130119, 129zsubcld 9201 . . . . . . . . . . . . 13
131130zred 9196 . . . . . . . . . . . 12
13262adantr 274 . . . . . . . . . . . 12
133 ltdiv1 8649 . . . . . . . . . . . 12
134128, 131, 132, 133syl3anc 1217 . . . . . . . . . . 11
135127, 134mpbid 146 . . . . . . . . . 10
136 simprr 522 . . . . . . . . . . . 12
13771adantr 274 . . . . . . . . . . . . 13
1387nnne0d 8788 . . . . . . . . . . . . . 14
139138adantr 274 . . . . . . . . . . . . 13
140 dvdsval2 11530 . . . . . . . . . . . . 13
141137, 139, 130, 140syl3anc 1217 . . . . . . . . . . . 12
142136, 141mpbid 146 . . . . . . . . . . 11
143 flqlt 10086 . . . . . . . . . . 11
14416, 142, 143syl2an2r 585 . . . . . . . . . 10
145135, 144mpbid 146 . . . . . . . . 9
146 zltp1le 9131 . . . . . . . . . 10
14717, 142, 146syl2an2r 585 . . . . . . . . 9
148145, 147mpbid 146 . . . . . . . 8
14992adantr 274 . . . . . . . . . . 11
150 elfzle2 9838 . . . . . . . . . . . 12
151150ad2antrl 482 . . . . . . . . . . 11
152120, 149, 121, 151lesub1dd 8346 . . . . . . . . . 10
15387adantr 274 . . . . . . . . . . 11
154 lediv1 8650 . . . . . . . . . . 11
155131, 153, 132, 154syl3anc 1217 . . . . . . . . . 10
156152, 155mpbid 146 . . . . . . . . 9
157 flqge 10085 . . . . . . . . . 10
1589, 142, 157syl2an2r 585 . . . . . . . . 9
159156, 158mpbid 146 . . . . . . . 8
16029adantr 274 . . . . . . . . 9
16110adantr 274 . . . . . . . . 9
162 elfz 9826 . . . . . . . . 9
163142, 160, 161, 162syl3anc 1217 . . . . . . . 8
164148, 159, 163mpbir2and 929 . . . . . . 7
165164ex 114 . . . . . 6
166116, 165syl5bi 151 . . . . 5
167116anbi2i 453 . . . . . . 7
168130zcnd 9197 . . . . . . . . . . 11
169168adantrl 470 . . . . . . . . . 10
17058zcnd 9197 . . . . . . . . . . 11
171170adantrr 471 . . . . . . . . . 10
1727nncnd 8757 . . . . . . . . . . 11
173172adantr 274 . . . . . . . . . 10
1747nnap0d 8789 . . . . . . . . . . 11 #
175174adantr 274 . . . . . . . . . 10 #
176169, 171, 173, 175divmulap3d 8608 . . . . . . . . 9
177119zcnd 9197 . . . . . . . . . . 11
178177adantrl 470 . . . . . . . . . 10
179105adantr 274 . . . . . . . . . 10
180104adantrr 471 . . . . . . . . . 10
181178, 179, 180subadd2d 8115 . . . . . . . . 9
182176, 181bitrd 187 . . . . . . . 8
183 eqcom 2142 . . . . . . . 8
184 eqcom 2142 . . . . . . . 8
185182, 183, 1843bitr4g 222 . . . . . . 7
186167, 185sylan2b 285 . . . . . 6
187186ex 114 . . . . 5
18831, 46, 113, 166, 187en3d 6670 . . . 4
189 entr 6685 . . . 4
19028, 188, 189syl2anc 409 . . 3
1911, 18fzfigd 10234 . . . 4
192 hashen 10561 . . . 4
193191, 45, 192syl2anc 409 . . 3
194190, 193mpbird 166 . 2
195 eluzle 9361 . . . . . . 7
1962, 195syl 14 . . . . . 6
197 zre 9081 . . . . . . . 8
198 zre 9081 . . . . . . . 8
199 zre 9081 . . . . . . . 8
200 lesub1 8241 . . . . . . . 8
201197, 198, 199, 200syl3an 1259 . . . . . . 7
20213, 4, 5, 201syl3anc 1217 . . . . . 6
203196, 202mpbid 146 . . . . 5
204 lediv1 8650 . . . . . 6
20556, 87, 62, 204syl3anc 1217 . . . . 5
206203, 205mpbid 146 . . . 4
207 flqword2 10092 . . . 4
20816, 9, 206, 207syl3anc 1217 . . 3
209 uznn0sub 9380 . . 3
210 hashfz1 10560 . . 3
211208, 209, 2103syl 17 . 2
212194, 211eqtr3d 2175 1
 Colors of variables: wff set class Syntax hints:   wi 4   wa 103   wb 104  DECID wdc 820   wceq 1332   wcel 1481   wne 2309  wral 2417  crab 2421   class class class wbr 3936  cfv 5130  (class class class)co 5781   cen 6639  cfn 6641  cc 7641  cr 7642  cc0 7643  c1 7644   caddc 7646   cmul 7648   clt 7823   cle 7824   cmin 7956   # cap 8366   cdiv 8455  cn 8743  cn0 9000  cz 9077  cuz 9349  cq 9437  cfz 9820  cfl 10071  ♯chash 10552   cdvds 11527 This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 604  ax-in2 605  ax-io 699  ax-5 1424  ax-7 1425  ax-gen 1426  ax-ie1 1470  ax-ie2 1471  ax-8 1483  ax-10 1484  ax-11 1485  ax-i12 1486  ax-bndl 1487  ax-4 1488  ax-13 1492  ax-14 1493  ax-17 1507  ax-i9 1511  ax-ial 1515  ax-i5r 1516  ax-ext 2122  ax-coll 4050  ax-sep 4053  ax-nul 4061  ax-pow 4105  ax-pr 4138  ax-un 4362  ax-setind 4459  ax-iinf 4509  ax-cnex 7734  ax-resscn 7735  ax-1cn 7736  ax-1re 7737  ax-icn 7738  ax-addcl 7739  ax-addrcl 7740  ax-mulcl 7741  ax-mulrcl 7742  ax-addcom 7743  ax-mulcom 7744  ax-addass 7745  ax-mulass 7746  ax-distr 7747  ax-i2m1 7748  ax-0lt1 7749  ax-1rid 7750  ax-0id 7751  ax-rnegex 7752  ax-precex 7753  ax-cnre 7754  ax-pre-ltirr 7755  ax-pre-ltwlin 7756  ax-pre-lttrn 7757  ax-pre-apti 7758  ax-pre-ltadd 7759  ax-pre-mulgt0 7760  ax-pre-mulext 7761  ax-arch 7762 This theorem depends on definitions:  df-bi 116  df-dc 821  df-3or 964  df-3an 965  df-tru 1335  df-fal 1338  df-nf 1438  df-sb 1737  df-eu 2003  df-mo 2004  df-clab 2127  df-cleq 2133  df-clel 2136  df-nfc 2271  df-ne 2310  df-nel 2405  df-ral 2422  df-rex 2423  df-reu 2424  df-rmo 2425  df-rab 2426  df-v 2691  df-sbc 2913  df-csb 3007  df-dif 3077  df-un 3079  df-in 3081  df-ss 3088  df-nul 3368  df-if 3479  df-pw 3516  df-sn 3537  df-pr 3538  df-op 3540  df-uni 3744  df-int 3779  df-iun 3822  df-br 3937  df-opab 3997  df-mpt 3998  df-tr 4034  df-id 4222  df-po 4225  df-iso 4226  df-iord 4295  df-on 4297  df-ilim 4298  df-suc 4300  df-iom 4512  df-xp 4552  df-rel 4553  df-cnv 4554  df-co 4555  df-dm 4556  df-rn 4557  df-res 4558  df-ima 4559  df-iota 5095  df-fun 5132  df-fn 5133  df-f 5134  df-f1 5135  df-fo 5136  df-f1o 5137  df-fv 5138  df-riota 5737  df-ov 5784  df-oprab 5785  df-mpo 5786  df-1st 6045  df-2nd 6046  df-recs 6209  df-frec 6295  df-1o 6320  df-er 6436  df-en 6642  df-dom 6643  df-fin 6644  df-pnf 7825  df-mnf 7826  df-xr 7827  df-ltxr 7828  df-le 7829  df-sub 7958  df-neg 7959  df-reap 8360  df-ap 8367  df-div 8456  df-inn 8744  df-n0 9001  df-z 9078  df-uz 9350  df-q 9438  df-rp 9470  df-fz 9821  df-fl 10073  df-mod 10126  df-ihash 10553  df-dvds 11528 This theorem is referenced by:  phiprmpw  11932
 Copyright terms: Public domain W3C validator