Metamath Proof Explorer

Theorem selbergsb

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 selbergsb 
|- E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ c

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 selbergb 
 |-  E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ c
3 1re 
 |-  1 e. RR
4 elicopnf 
 |-  ( 1 e. RR -> ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) ) )
5 3 4 ax-mp 
 |-  ( x e. ( 1 [,) +oo ) <-> ( x e. RR /\ 1 <_ x ) )
6 5 simplbi 
 |-  ( x e. ( 1 [,) +oo ) -> x e. RR )
7 1 pntsval 
 |-  ( x e. RR -> ( S ` x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) )
8 6 7 syl 
 |-  ( x e. ( 1 [,) +oo ) -> ( S ` x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) )
9 8 oveq1d 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( S ` x ) / x ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) )
10 9 fvoveq1d 
 |-  ( x e. ( 1 [,) +oo ) -> ( abs ` ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) ) = ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) )
11 10 breq1d 
 |-  ( x e. ( 1 [,) +oo ) -> ( ( abs ` ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ c <-> ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ c ) )
12 11 ralbiia 
 |-  ( A. x e. ( 1 [,) +oo ) ( abs ` ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ c <-> A. x e. ( 1 [,) +oo ) ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ c )
13 12 rexbii 
 |-  ( E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ c <-> E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( Lam ` n ) x. ( ( log ` n ) + ( psi ` ( x / n ) ) ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ c )
14 2 13 mpbir 
 |-  E. c e. RR+ A. x e. ( 1 [,) +oo ) ( abs ` ( ( ( S ` x ) / x ) - ( 2 x. ( log ` x ) ) ) ) <_ c