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

Theorem dchrmusumlem 21169
 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
dchrmusumlem
Distinct variable groups:   ,,,   ,,,   ,,,   ,,   ,,,   ,,   ,,,   ,,,   ,,,   ,,,,   ,,,,
Allowed substitution hints:   (,)   ()   ()   ()   ()   ()   (,,,)   ()   ()

Proof of Theorem dchrmusumlem
StepHypRef Expression
1 fzfid 11267 . . . . . . 7
2 dchrmusum.g . . . . . . . . 9 DChr
3 rpvmasum.z . . . . . . . . 9 ℤ/n
4 dchrmusum.d . . . . . . . . 9
5 rpvmasum.l . . . . . . . . 9 RHom
6 dchrmusum.b . . . . . . . . . 10
76ad2antrr 707 . . . . . . . . 9
8 elfzelz 11015 . . . . . . . . . 10
98adantl 453 . . . . . . . . 9
102, 3, 4, 5, 7, 9dchrzrhcl 20982 . . . . . . . 8
11 elfznn 11036 . . . . . . . . . . . . 13
1211adantl 453 . . . . . . . . . . . 12
13 mucl 20877 . . . . . . . . . . . 12
1412, 13syl 16 . . . . . . . . . . 11
1514zred 10331 . . . . . . . . . 10
1615, 12nndivred 10004 . . . . . . . . 9
1716recnd 9070 . . . . . . . 8
1810, 17mulcld 9064 . . . . . . 7
191, 18fsumcl 12482 . . . . . 6
20 dchrmusum.t . . . . . . . 8
21 climcl 12248 . . . . . . . 8
2220, 21syl 16 . . . . . . 7
2322adantr 452 . . . . . 6
2419, 23mulcld 9064 . . . . 5
25 rpvmasum.a . . . . . . 7
26 dchrmusum.1 . . . . . . 7
27 dchrmusum.n1 . . . . . . 7
28 dchrmusum.f . . . . . . 7
29 dchrmusum.c . . . . . . 7
30 dchrmusum.2 . . . . . . 7
313, 5, 25, 2, 4, 26, 6, 27, 28, 29, 20, 30dchrisumn0 21168 . . . . . 6
3231adantr 452 . . . . 5
3324, 23, 32divrecd 9749 . . . 4
3419, 23, 32divcan4d 9752 . . . 4
3533, 34eqtr3d 2438 . . 3
3635mpteq2dva 4255 . 2
3722, 31reccld 9739 . . . 4