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

Theorem dchrvmasumlem 21174
 Description: The sum of the Möbius function multiplied by a non-principal Dirichlet character, divided by , is bounded. Equation 9.4.16 of [Shapiro], p. 379. (Contributed by Mario Carneiro, 12-May-2016.)
Hypotheses
Ref Expression
rpvmasum.z ℤ/n
rpvmasum.l RHom
rpvmasum.a
dchrmusum.g DChr
dchrmusum.d
dchrmusum.1
dchrmusum.b
dchrmusum.n1
dchrmusum.f
dchrmusum.c
dchrmusum.t
dchrmusum.2
Assertion
Ref Expression
dchrvmasumlem Λ
Distinct variable groups:   ,,,   ,,,   ,,,   ,,   ,,,   ,,   ,,,   ,,,   ,,,   ,,,,   ,,,,
Allowed substitution hints:   (,)   ()   ()   ()   ()   ()   (,,,)   ()   ()

Proof of Theorem dchrvmasumlem
StepHypRef Expression
1 rpvmasum.z . . . . . . . 8 ℤ/n
2 rpvmasum.l . . . . . . . 8 RHom
3 rpvmasum.a . . . . . . . 8
4 dchrmusum.g . . . . . . . 8 DChr
5 dchrmusum.d . . . . . . . 8
6 dchrmusum.1 . . . . . . . 8
7 dchrmusum.b . . . . . . . 8
8 dchrmusum.n1 . . . . . . . 8
9 dchrmusum.f . . . . . . . 8
10 dchrmusum.c . . . . . . . 8
11 dchrmusum.t . . . . . . . 8
12 dchrmusum.2 . . . . . . . 8
131, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12dchrisumn0 21172 . . . . . . 7
1413adantr 452 . . . . . 6
15 ifnefalse 3711 . . . . . 6
1614, 15syl 16 . . . . 5
1716oveq2d 6060 . . . 4 Λ Λ
18 fzfid 11271 . . . . . 6
197ad2antrr 707 . . . . . . . 8
20 elfzelz 11019 . . . . . . . . 9
2120adantl 453 . . . . . . . 8
224, 1, 5, 2, 19, 21dchrzrhcl 20986 . . . . . . 7
23 elfznn 11040 . . . . . . . . . 10
2423adantl 453 . . . . . . . . 9
25 vmacl 20858 . . . . . . . . . 10 Λ
26 nndivre 9995 . . . . . . . . . 10 Λ Λ
2725, 26mpancom 651 . . . . . . . . 9 Λ
2824, 27syl 16 . . . . . . . 8 Λ
2928recnd 9074 . . . . . . 7 Λ
3022, 29mulcld 9068 . . . . . 6 Λ
3118, 30fsumcl 12486 . . . . 5 Λ
3231addid1d 9226 . . . 4 Λ Λ
3317, 32eqtrd 2440 . . 3 Λ Λ
3433mpteq2dva 4259 . 2 Λ Λ
351, 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12dchrvmasumif 21154 . 2 Λ
3634, 35eqeltrrd 2483 1 Λ
 Colors of variables: wff set class Syntax hints:   wi 4   wa 359   wceq 1649   wcel 1721   wne 2571  wral 2670  cif 3703   class class class wbr 4176   cmpt 4230  cfv 5417  (class class class)co 6044  cr 8949  cc0 8950  c1 8951   caddc 8953   cmul 8955   cpnf 9077   cle 9081   cmin 9251   cdiv 9637  cn 9960  cz 10242  crp 10572  cico 10878  cfz 11003  cfl 11160   cseq 11282  cabs 11998   cli 12237  co1 12239  csu 12438  cbs 13428  c0g 13682  RHomczrh 16737  ℤ/nℤczn 16740  clog 20409  Λcvma 20831  DChrcdchr 20973 This theorem is referenced by:  dchrvmasum  21176 This theorem was proved from axioms:  ax-1 5  ax-2 6  ax-3 7  ax-mp 8  ax-gen 1552  ax-5 1563  ax-17 1623  ax-9 1662  ax-8 1683  ax-13 1723  ax-14 1725  ax-6 1740  ax-7 1745  ax-11 1757  ax-12 1946  ax-ext 2389  ax-rep 4284  ax-sep 4294  ax-nul 4302  ax-pow 4341  ax-pr 4367  ax-un 4664  ax-inf2 7556  ax-cnex 9006  ax-resscn 9007  ax-1cn 9008  ax-icn 9009  ax-addcl 9010  ax-addrcl 9011  ax-mulcl 9012  ax-mulrcl 9013  ax-mulcom 9014  ax-addass 9015  ax-mulass 9016  ax-distr 9017  ax-i2m1 9018  ax-1ne0 9019  ax-1rid 9020  ax-rnegex 9021  ax-rrecex 9022  ax-cnre 9023  ax-pre-lttri 9024  ax-pre-lttrn 9025  ax-pre-ltadd 9026  ax-pre-mulgt0 9027  ax-pre-sup 9028  ax-addf 9029  ax-mulf 9030 This theorem depends on definitions:  df-bi 178  df-or 360  df-an 361  df-3or 937  df-3an 938  df-tru 1325  df-fal 1326  df-ex 1548  df-nf 1551  df-sb 1656  df-eu 2262  df-mo 2263  df-clab 2395  df-cleq 2401  df-clel 2404  df-nfc 2533  df-ne 2573  df-nel 2574  df-ral 2675  df-rex 2676  df-reu 2677  df-rmo 2678  df-rab 2679  df-v 2922  df-sbc 3126  df-csb 3216  df-dif 3287  df-un 3289  df-in 3291  df-ss 3298  df-pss 3300  df-nul 3593  df-if 3704  df-pw 3765  df-sn 3784  df-pr 3785  df-tp 3786  df-op 3787  df-uni 3980  df-int 4015  df-iun 4059  df-iin 4060  df-disj 4147  df-br 4177  df-opab 4231  df-mpt 4232  df-tr 4267  df-eprel 4458  df-id 4462  df-po 4467  df-so 4468  df-fr 4505  df-se 4506  df-we 4507  df-ord 4548  df-on 4549  df-lim 4550  df-suc 4551  df-om 4809  df-xp 4847  df-rel 4848  df-cnv 4849  df-co 4850  df-dm 4851  df-rn 4852  df-res 4853  df-ima 4854  df-iota 5381  df-fun 5419  df-fn 5420  df-f 5421  df-f1 5422  df-fo 5423  df-f1o 5424  df-fv 5425  df-isom 5426  df-ov 6047  df-oprab 6048  df-mpt2 6049  df-of 6268  df-1st 6312  df-2nd 6313  df-tpos 6442  df-rpss 6485  df-riota 6512  df-recs 6596  df-rdg 6631  df-1o 6687  df-2o 6688  df-oadd 6691  df-omul 6692  df-er 6868  df-ec 6870  df-qs 6874  df-map 6983  df-pm 6984  df-ixp 7027  df-en 7073  df-dom 7074  df-sdom 7075  df-fin 7076  df-fi 7378  df-sup 7408  df-oi 7439  df-card 7786  df-acn 7789  df-cda 8008  df-pnf 9082  df-mnf 9083  df-xr 9084  df-ltxr 9085  df-le 9086  df-sub 9253  df-neg 9254  df-div 9638  df-nn 9961  df-2 10018  df-3 10019  df-4 10020  df-5 10021  df-6 10022  df-7 10023  df-8 10024  df-9 10025  df-10 10026  df-n0 10182  df-z 10243  df-dec 10343  df-uz 10449  df-q 10535  df-rp 10573  df-xneg 10670  df-xadd 10671  df-xmul 10672  df-ioo 10880  df-ioc 10881  df-ico 10882  df-icc 10883  df-fz 11004  df-fzo 11095  df-fl 11161  df-mod 11210  df-seq 11283  df-exp 11342  df-fac 11526  df-bc 11553  df-hash 11578  df-word 11682  df-concat 11683  df-s1 11684  df-shft 11841  df-cj 11863  df-re 11864  df-im 11865  df-sqr 11999  df-abs 12000  df-limsup 12224  df-clim 12241  df-rlim 12242  df-o1 12243  df-lo1 12244  df-sum 12439  df-ef 12629  df-e 12630  df-sin 12631  df-cos 12632  df-pi 12634  df-dvds 12812  df-gcd 12966  df-prm 13039  df-numer 13086  df-denom 13087  df-phi 13114  df-pc 13170  df-struct 13430  df-ndx 13431  df-slot 13432  df-base 13433  df-sets 13434  df-ress 13435  df-plusg 13501  df-mulr 13502  df-starv 13503  df-sca 13504  df-vsca 13505  df-tset 13507  df-ple 13508  df-ds 13510  df-unif 13511  df-hom 13512  df-cco 13513  df-rest 13609  df-topn 13610  df-topgen 13626  df-pt 13627  df-prds 13630  df-xrs 13685  df-0g 13686  df-gsum 13687  df-qtop 13692  df-imas 13693  df-divs 13694  df-xps 13695  df-mre 13770  df-mrc 13771  df-acs 13773  df-mnd 14649  df-mhm 14697  df-submnd 14698  df-grp 14771  df-minusg 14772  df-sbg 14773  df-mulg 14774  df-subg 14900  df-nsg 14901  df-eqg 14902  df-ghm 14963  df-gim 15005  df-ga 15026  df-cntz 15075  df-oppg 15101  df-od 15126  df-gex 15127  df-pgp 15128  df-lsm 15229  df-pj1 15230  df-cmn 15373  df-abl 15374  df-cyg 15447  df-dprd 15515  df-dpj 15516  df-mgp 15608  df-rng 15622  df-cring 15623  df-ur 15624  df-oppr 15687  df-dvdsr 15705  df-unit 15706  df-invr 15736  df-dvr 15747  df-rnghom 15778  df-drng 15796  df-subrg 15825  df-lmod 15911  df-lss 15968  df-lsp 16007  df-sra 16203  df-rgmod 16204  df-lidl 16205  df-rsp 16206  df-2idl 16262  df-psmet 16653  df-xmet 16654  df-met 16655  df-bl 16656  df-mopn 16657  df-fbas 16658  df-fg 16659  df-cnfld 16663  df-zrh 16741  df-zn 16744  df-top 16922  df-bases 16924  df-topon 16925  df-topsp 16926  df-cld 17042  df-ntr 17043  df-cls 17044  df-nei 17121  df-lp 17159  df-perf 17160  df-cn 17249  df-cnp 17250  df-haus 17337  df-cmp 17408  df-tx 17551  df-hmeo 17744  df-fil 17835  df-fm 17927  df-flim 17928  df-flf 17929  df-xms 18307  df-ms 18308  df-tms 18309  df-cncf 18865  df-0p 19519  df-limc 19710  df-dv 19711  df-ply 20064  df-idp 20065  df-coe 20066  df-dgr 20067  df-quot 20165  df-log 20411  df-cxp 20412  df-em 20788  df-cht 20836  df-vma 20837  df-chp 20838  df-ppi 20839  df-mu 20840  df-dchr 20974
 Copyright terms: Public domain W3C validator