Metamath Proof Explorer

Theorem selbergs

Description: Selberg's symmetry formula, using the definition of the Selberg function. (Contributed by Mario Carneiro, 31-May-2016)

Ref Expression
Hypothesis pntsval.1 
|- S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) )
Assertion selbergs 
|- ( x e. RR+ |-> ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 pntsval.1 
 |-  S = ( a e. RR |-> sum_ i e. ( 1 ... ( |_ ` a ) ) ( ( Lam ` i ) x. ( ( log ` i ) + ( psi ` ( a / i ) ) ) ) )
2 rpre 
 |-  ( x e. RR+ -> x e. RR )
3 1 pntsval 
 |-  ( x e. RR -> ( S ` x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) )
4 2 3 syl 
 |-  ( x e. RR+ -> ( S ` x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) )
5 4 oveq1d 
 |-  ( x e. RR+ -> ( ( S ` x ) / x ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) )
6 5 oveq1d 
 |-  ( x e. RR+ -> ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) = ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) )
7 6 mpteq2ia 
 |-  ( x e. RR+ |-> ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) ) = ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) )
8 selberg 
 |-  ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
9 7 8 eqeltri 
 |-  ( x e. RR+ |-> ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)