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	syl5eq	⊢ ( 𝑎 = 𝐴 → Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝐴 / 𝑛 ) ) ) ) )
17		sumex	⊢ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝐴 / 𝑛 ) ) ) ) ∈ V
18	16 1 17	fvmpt	⊢ ( 𝐴 ∈ ℝ → ( 𝑆 ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝐴 / 𝑛 ) ) ) ) )