Metamath Proof Explorer


Theorem pntsval

Description: Define the "Selberg function", whose asymptotic behavior is the content of selberg . (Contributed by Mario Carneiro, 31-May-2016)

Ref Expression
Hypothesis pntsval.1 โŠข ๐‘† = ( ๐‘Ž โˆˆ โ„ โ†ฆ ฮฃ ๐‘– โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐‘Ž ) ) ( ( ฮ› โ€˜ ๐‘– ) ยท ( ( log โ€˜ ๐‘– ) + ( ฯˆ โ€˜ ( ๐‘Ž / ๐‘– ) ) ) ) )
Assertion pntsval ( ๐ด โˆˆ โ„ โ†’ ( ๐‘† โ€˜ ๐ด ) = ฮฃ ๐‘› โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐ด ) ) ( ( ฮ› โ€˜ ๐‘› ) ยท ( ( log โ€˜ ๐‘› ) + ( ฯˆ โ€˜ ( ๐ด / ๐‘› ) ) ) ) )

Proof

Step Hyp Ref Expression
1 pntsval.1 โŠข ๐‘† = ( ๐‘Ž โˆˆ โ„ โ†ฆ ฮฃ ๐‘– โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐‘Ž ) ) ( ( ฮ› โ€˜ ๐‘– ) ยท ( ( log โ€˜ ๐‘– ) + ( ฯˆ โ€˜ ( ๐‘Ž / ๐‘– ) ) ) ) )
2 fveq2 โŠข ( ๐‘– = ๐‘› โ†’ ( ฮ› โ€˜ ๐‘– ) = ( ฮ› โ€˜ ๐‘› ) )
3 fveq2 โŠข ( ๐‘– = ๐‘› โ†’ ( log โ€˜ ๐‘– ) = ( log โ€˜ ๐‘› ) )
4 oveq2 โŠข ( ๐‘– = ๐‘› โ†’ ( ๐‘Ž / ๐‘– ) = ( ๐‘Ž / ๐‘› ) )
5 4 fveq2d โŠข ( ๐‘– = ๐‘› โ†’ ( ฯˆ โ€˜ ( ๐‘Ž / ๐‘– ) ) = ( ฯˆ โ€˜ ( ๐‘Ž / ๐‘› ) ) )
6 3 5 oveq12d โŠข ( ๐‘– = ๐‘› โ†’ ( ( log โ€˜ ๐‘– ) + ( ฯˆ โ€˜ ( ๐‘Ž / ๐‘– ) ) ) = ( ( log โ€˜ ๐‘› ) + ( ฯˆ โ€˜ ( ๐‘Ž / ๐‘› ) ) ) )
7 2 6 oveq12d โŠข ( ๐‘– = ๐‘› โ†’ ( ( ฮ› โ€˜ ๐‘– ) ยท ( ( log โ€˜ ๐‘– ) + ( ฯˆ โ€˜ ( ๐‘Ž / ๐‘– ) ) ) ) = ( ( ฮ› โ€˜ ๐‘› ) ยท ( ( log โ€˜ ๐‘› ) + ( ฯˆ โ€˜ ( ๐‘Ž / ๐‘› ) ) ) ) )
8 7 cbvsumv โŠข ฮฃ ๐‘– โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐‘Ž ) ) ( ( ฮ› โ€˜ ๐‘– ) ยท ( ( log โ€˜ ๐‘– ) + ( ฯˆ โ€˜ ( ๐‘Ž / ๐‘– ) ) ) ) = ฮฃ ๐‘› โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐‘Ž ) ) ( ( ฮ› โ€˜ ๐‘› ) ยท ( ( log โ€˜ ๐‘› ) + ( ฯˆ โ€˜ ( ๐‘Ž / ๐‘› ) ) ) )
9 fveq2 โŠข ( ๐‘Ž = ๐ด โ†’ ( โŒŠ โ€˜ ๐‘Ž ) = ( โŒŠ โ€˜ ๐ด ) )
10 9 oveq2d โŠข ( ๐‘Ž = ๐ด โ†’ ( 1 ... ( โŒŠ โ€˜ ๐‘Ž ) ) = ( 1 ... ( โŒŠ โ€˜ ๐ด ) ) )
11 fvoveq1 โŠข ( ๐‘Ž = ๐ด โ†’ ( ฯˆ โ€˜ ( ๐‘Ž / ๐‘› ) ) = ( ฯˆ โ€˜ ( ๐ด / ๐‘› ) ) )
12 11 oveq2d โŠข ( ๐‘Ž = ๐ด โ†’ ( ( log โ€˜ ๐‘› ) + ( ฯˆ โ€˜ ( ๐‘Ž / ๐‘› ) ) ) = ( ( log โ€˜ ๐‘› ) + ( ฯˆ โ€˜ ( ๐ด / ๐‘› ) ) ) )
13 12 oveq2d โŠข ( ๐‘Ž = ๐ด โ†’ ( ( ฮ› โ€˜ ๐‘› ) ยท ( ( log โ€˜ ๐‘› ) + ( ฯˆ โ€˜ ( ๐‘Ž / ๐‘› ) ) ) ) = ( ( ฮ› โ€˜ ๐‘› ) ยท ( ( log โ€˜ ๐‘› ) + ( ฯˆ โ€˜ ( ๐ด / ๐‘› ) ) ) ) )
14 13 adantr โŠข ( ( ๐‘Ž = ๐ด โˆง ๐‘› โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐‘Ž ) ) ) โ†’ ( ( ฮ› โ€˜ ๐‘› ) ยท ( ( log โ€˜ ๐‘› ) + ( ฯˆ โ€˜ ( ๐‘Ž / ๐‘› ) ) ) ) = ( ( ฮ› โ€˜ ๐‘› ) ยท ( ( log โ€˜ ๐‘› ) + ( ฯˆ โ€˜ ( ๐ด / ๐‘› ) ) ) ) )
15 10 14 sumeq12dv โŠข ( ๐‘Ž = ๐ด โ†’ ฮฃ ๐‘› โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐‘Ž ) ) ( ( ฮ› โ€˜ ๐‘› ) ยท ( ( log โ€˜ ๐‘› ) + ( ฯˆ โ€˜ ( ๐‘Ž / ๐‘› ) ) ) ) = ฮฃ ๐‘› โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐ด ) ) ( ( ฮ› โ€˜ ๐‘› ) ยท ( ( log โ€˜ ๐‘› ) + ( ฯˆ โ€˜ ( ๐ด / ๐‘› ) ) ) ) )
16 8 15 eqtrid โŠข ( ๐‘Ž = ๐ด โ†’ ฮฃ ๐‘– โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐‘Ž ) ) ( ( ฮ› โ€˜ ๐‘– ) ยท ( ( log โ€˜ ๐‘– ) + ( ฯˆ โ€˜ ( ๐‘Ž / ๐‘– ) ) ) ) = ฮฃ ๐‘› โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐ด ) ) ( ( ฮ› โ€˜ ๐‘› ) ยท ( ( log โ€˜ ๐‘› ) + ( ฯˆ โ€˜ ( ๐ด / ๐‘› ) ) ) ) )
17 sumex โŠข ฮฃ ๐‘› โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐ด ) ) ( ( ฮ› โ€˜ ๐‘› ) ยท ( ( log โ€˜ ๐‘› ) + ( ฯˆ โ€˜ ( ๐ด / ๐‘› ) ) ) ) โˆˆ V
18 16 1 17 fvmpt โŠข ( ๐ด โˆˆ โ„ โ†’ ( ๐‘† โ€˜ ๐ด ) = ฮฃ ๐‘› โˆˆ ( 1 ... ( โŒŠ โ€˜ ๐ด ) ) ( ( ฮ› โ€˜ ๐‘› ) ยท ( ( log โ€˜ ๐‘› ) + ( ฯˆ โ€˜ ( ๐ด / ๐‘› ) ) ) ) )