Metamath Proof Explorer


Theorem dchrvmasum

Description: The sum of the von Mangoldt function multiplied by a non-principal Dirichlet character, divided by n , is bounded. Equation 9.4.8 of Shapiro, p. 376. (Contributed by Mario Carneiro, 12-May-2016)

Ref Expression
Hypotheses rpvmasum.z โŠข ๐‘ = ( โ„ค/nโ„ค โ€˜ ๐‘ )
rpvmasum.l โŠข ๐ฟ = ( โ„คRHom โ€˜ ๐‘ )
rpvmasum.a โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„• )
dchrmusum.g โŠข ๐บ = ( DChr โ€˜ ๐‘ )
dchrmusum.d โŠข ๐ท = ( Base โ€˜ ๐บ )
dchrmusum.1 โŠข 1 = ( 0g โ€˜ ๐บ )
dchrmusum.b โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ท )
dchrmusum.n1 โŠข ( ๐œ‘ โ†’ ๐‘‹ โ‰  1 )
Assertion dchrvmasum ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ โ„+ โ†ฆ ฮฃ ๐‘› โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐‘ฅ ) ) ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘› ) ) ยท ( ( ฮ› โ€˜ ๐‘› ) / ๐‘› ) ) ) โˆˆ ๐‘‚(1) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z โŠข ๐‘ = ( โ„ค/nโ„ค โ€˜ ๐‘ )
2 rpvmasum.l โŠข ๐ฟ = ( โ„คRHom โ€˜ ๐‘ )
3 rpvmasum.a โŠข ( ๐œ‘ โ†’ ๐‘ โˆˆ โ„• )
4 dchrmusum.g โŠข ๐บ = ( DChr โ€˜ ๐‘ )
5 dchrmusum.d โŠข ๐ท = ( Base โ€˜ ๐บ )
6 dchrmusum.1 โŠข 1 = ( 0g โ€˜ ๐บ )
7 dchrmusum.b โŠข ( ๐œ‘ โ†’ ๐‘‹ โˆˆ ๐ท )
8 dchrmusum.n1 โŠข ( ๐œ‘ โ†’ ๐‘‹ โ‰  1 )
9 eqid โŠข ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) = ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) )
10 1 2 3 4 5 6 7 8 9 dchrmusumlema โŠข ( ๐œ‘ โ†’ โˆƒ ๐‘ก โˆƒ ๐‘ โˆˆ ( 0 [,) +โˆž ) ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ‡ ๐‘ก โˆง โˆ€ ๐‘ฆ โˆˆ ( 1 [,) +โˆž ) ( abs โ€˜ ( ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ€˜ ( โŒŠ โ€˜ ๐‘ฆ ) ) โˆ’ ๐‘ก ) ) โ‰ค ( ๐‘ / ๐‘ฆ ) ) )
11 3 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ( 0 [,) +โˆž ) โˆง ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ‡ ๐‘ก โˆง โˆ€ ๐‘ฆ โˆˆ ( 1 [,) +โˆž ) ( abs โ€˜ ( ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ€˜ ( โŒŠ โ€˜ ๐‘ฆ ) ) โˆ’ ๐‘ก ) ) โ‰ค ( ๐‘ / ๐‘ฆ ) ) ) ) โ†’ ๐‘ โˆˆ โ„• )
12 7 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ( 0 [,) +โˆž ) โˆง ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ‡ ๐‘ก โˆง โˆ€ ๐‘ฆ โˆˆ ( 1 [,) +โˆž ) ( abs โ€˜ ( ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ€˜ ( โŒŠ โ€˜ ๐‘ฆ ) ) โˆ’ ๐‘ก ) ) โ‰ค ( ๐‘ / ๐‘ฆ ) ) ) ) โ†’ ๐‘‹ โˆˆ ๐ท )
13 8 adantr โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ( 0 [,) +โˆž ) โˆง ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ‡ ๐‘ก โˆง โˆ€ ๐‘ฆ โˆˆ ( 1 [,) +โˆž ) ( abs โ€˜ ( ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ€˜ ( โŒŠ โ€˜ ๐‘ฆ ) ) โˆ’ ๐‘ก ) ) โ‰ค ( ๐‘ / ๐‘ฆ ) ) ) ) โ†’ ๐‘‹ โ‰  1 )
14 simprl โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ( 0 [,) +โˆž ) โˆง ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ‡ ๐‘ก โˆง โˆ€ ๐‘ฆ โˆˆ ( 1 [,) +โˆž ) ( abs โ€˜ ( ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ€˜ ( โŒŠ โ€˜ ๐‘ฆ ) ) โˆ’ ๐‘ก ) ) โ‰ค ( ๐‘ / ๐‘ฆ ) ) ) ) โ†’ ๐‘ โˆˆ ( 0 [,) +โˆž ) )
15 simprrl โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ( 0 [,) +โˆž ) โˆง ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ‡ ๐‘ก โˆง โˆ€ ๐‘ฆ โˆˆ ( 1 [,) +โˆž ) ( abs โ€˜ ( ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ€˜ ( โŒŠ โ€˜ ๐‘ฆ ) ) โˆ’ ๐‘ก ) ) โ‰ค ( ๐‘ / ๐‘ฆ ) ) ) ) โ†’ seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ‡ ๐‘ก )
16 simprrr โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ( 0 [,) +โˆž ) โˆง ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ‡ ๐‘ก โˆง โˆ€ ๐‘ฆ โˆˆ ( 1 [,) +โˆž ) ( abs โ€˜ ( ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ€˜ ( โŒŠ โ€˜ ๐‘ฆ ) ) โˆ’ ๐‘ก ) ) โ‰ค ( ๐‘ / ๐‘ฆ ) ) ) ) โ†’ โˆ€ ๐‘ฆ โˆˆ ( 1 [,) +โˆž ) ( abs โ€˜ ( ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ€˜ ( โŒŠ โ€˜ ๐‘ฆ ) ) โˆ’ ๐‘ก ) ) โ‰ค ( ๐‘ / ๐‘ฆ ) )
17 1 2 11 4 5 6 12 13 9 14 15 16 dchrvmasumlem โŠข ( ( ๐œ‘ โˆง ( ๐‘ โˆˆ ( 0 [,) +โˆž ) โˆง ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ‡ ๐‘ก โˆง โˆ€ ๐‘ฆ โˆˆ ( 1 [,) +โˆž ) ( abs โ€˜ ( ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ€˜ ( โŒŠ โ€˜ ๐‘ฆ ) ) โˆ’ ๐‘ก ) ) โ‰ค ( ๐‘ / ๐‘ฆ ) ) ) ) โ†’ ( ๐‘ฅ โˆˆ โ„+ โ†ฆ ฮฃ ๐‘› โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐‘ฅ ) ) ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘› ) ) ยท ( ( ฮ› โ€˜ ๐‘› ) / ๐‘› ) ) ) โˆˆ ๐‘‚(1) )
18 17 rexlimdvaa โŠข ( ๐œ‘ โ†’ ( โˆƒ ๐‘ โˆˆ ( 0 [,) +โˆž ) ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ‡ ๐‘ก โˆง โˆ€ ๐‘ฆ โˆˆ ( 1 [,) +โˆž ) ( abs โ€˜ ( ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ€˜ ( โŒŠ โ€˜ ๐‘ฆ ) ) โˆ’ ๐‘ก ) ) โ‰ค ( ๐‘ / ๐‘ฆ ) ) โ†’ ( ๐‘ฅ โˆˆ โ„+ โ†ฆ ฮฃ ๐‘› โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐‘ฅ ) ) ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘› ) ) ยท ( ( ฮ› โ€˜ ๐‘› ) / ๐‘› ) ) ) โˆˆ ๐‘‚(1) ) )
19 18 exlimdv โŠข ( ๐œ‘ โ†’ ( โˆƒ ๐‘ก โˆƒ ๐‘ โˆˆ ( 0 [,) +โˆž ) ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ‡ ๐‘ก โˆง โˆ€ ๐‘ฆ โˆˆ ( 1 [,) +โˆž ) ( abs โ€˜ ( ( seq 1 ( + , ( ๐‘Ž โˆˆ โ„• โ†ฆ ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘Ž ) ) / ๐‘Ž ) ) ) โ€˜ ( โŒŠ โ€˜ ๐‘ฆ ) ) โˆ’ ๐‘ก ) ) โ‰ค ( ๐‘ / ๐‘ฆ ) ) โ†’ ( ๐‘ฅ โˆˆ โ„+ โ†ฆ ฮฃ ๐‘› โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐‘ฅ ) ) ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘› ) ) ยท ( ( ฮ› โ€˜ ๐‘› ) / ๐‘› ) ) ) โˆˆ ๐‘‚(1) ) )
20 10 19 mpd โŠข ( ๐œ‘ โ†’ ( ๐‘ฅ โˆˆ โ„+ โ†ฆ ฮฃ ๐‘› โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐‘ฅ ) ) ( ( ๐‘‹ โ€˜ ( ๐ฟ โ€˜ ๐‘› ) ) ยท ( ( ฮ› โ€˜ ๐‘› ) / ๐‘› ) ) ) โˆˆ ๐‘‚(1) )