Metamath Proof Explorer

Theorem selberglem3

Description: Lemma for selberg . Estimation of the left-hand side of logsqvma2 . (Contributed by Mario Carneiro, 23-May-2016)

Ref Expression
Assertion selberglem3 
|- ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)

Proof

Step Hyp Ref Expression
1 fvoveq1 
 |-  ( n = ( d x. m ) -> ( log ` ( n / d ) ) = ( log ` ( ( d x. m ) / d ) ) )
2 1 oveq1d 
 |-  ( n = ( d x. m ) -> ( ( log ` ( n / d ) ) ^ 2 ) = ( ( log ` ( ( d x. m ) / d ) ) ^ 2 ) )
3 2 oveq2d 
 |-  ( n = ( d x. m ) -> ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) = ( ( mmu ` d ) x. ( ( log ` ( ( d x. m ) / d ) ) ^ 2 ) ) )
4 rpre 
 |-  ( x e. RR+ -> x e. RR )
5 ssrab2 
 |-  { y e. NN | y || n } C_ NN
6 simprr 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> d e. { y e. NN | y || n } )
7 5 6 sselid 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> d e. NN )
8 mucl 
 |-  ( d e. NN -> ( mmu ` d ) e. ZZ )
9 7 8 syl 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( mmu ` d ) e. ZZ )
10 9 zcnd 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( mmu ` d ) e. CC )
11 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
12 11 nnrpd 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. RR+ )
13 12 ad2antrl 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> n e. RR+ )
14 7 nnrpd 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> d e. RR+ )
15 13 14 rpdivcld 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( n / d ) e. RR+ )
16 relogcl 
 |-  ( ( n / d ) e. RR+ -> ( log ` ( n / d ) ) e. RR )
17 16 recnd 
 |-  ( ( n / d ) e. RR+ -> ( log ` ( n / d ) ) e. CC )
18 15 17 syl 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( log ` ( n / d ) ) e. CC )
19 18 sqcld 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( ( log ` ( n / d ) ) ^ 2 ) e. CC )
20 10 19 mulcld 
 |-  ( ( x e. RR+ /\ ( n e. ( 1 ... ( |_ ` x ) ) /\ d e. { y e. NN | y || n } ) ) -> ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) e. CC )
21 3 4 20 dvdsflsumcom 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` ( ( d x. m ) / d ) ) ^ 2 ) ) )
22 elfznn 
 |-  ( m e. ( 1 ... ( |_ ` ( x / d ) ) ) -> m e. NN )
23 22 3ad2ant3 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> m e. NN )
24 23 nncnd 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> m e. CC )
25 elfznn 
 |-  ( d e. ( 1 ... ( |_ ` x ) ) -> d e. NN )
26 25 3ad2ant2 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> d e. NN )
27 26 nncnd 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> d e. CC )
28 26 nnne0d 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> d =/= 0 )
29 24 27 28 divcan3d 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( d x. m ) / d ) = m )
30 29 fveq2d 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( log ` ( ( d x. m ) / d ) ) = ( log ` m ) )
31 30 oveq1d 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( log ` ( ( d x. m ) / d ) ) ^ 2 ) = ( ( log ` m ) ^ 2 ) )
32 31 oveq2d 
 |-  ( ( x e. RR+ /\ d e. ( 1 ... ( |_ ` x ) ) /\ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ) -> ( ( mmu ` d ) x. ( ( log ` ( ( d x. m ) / d ) ) ^ 2 ) ) = ( ( mmu ` d ) x. ( ( log ` m ) ^ 2 ) ) )
33 32 2sumeq2dv 
 |-  ( x e. RR+ -> sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` ( ( d x. m ) / d ) ) ^ 2 ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` m ) ^ 2 ) ) )
34 21 33 eqtrd 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) = sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` m ) ^ 2 ) ) )
35 34 oveq1d 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) / x ) = ( sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` m ) ^ 2 ) ) / x ) )
36 35 oveq1d 
 |-  ( x e. RR+ -> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) = ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` m ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) )
37 36 mpteq2ia 
 |-  ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) = ( x e. RR+ |-> ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` m ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) )
38 eqid 
 |-  ( ( ( ( log ` ( x / d ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / d ) ) ) ) ) / d ) = ( ( ( ( log ` ( x / d ) ) ^ 2 ) + ( 2 - ( 2 x. ( log ` ( x / d ) ) ) ) ) / d )
39 38 selberglem2 
 |-  ( x e. RR+ |-> ( ( sum_ d e. ( 1 ... ( |_ ` x ) ) sum_ m e. ( 1 ... ( |_ ` ( x / d ) ) ) ( ( mmu ` d ) x. ( ( log ` m ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)
40 37 39 eqeltri 
 |-  ( x e. RR+ |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) sum_ d e. { y e. NN | y || n } ( ( mmu ` d ) x. ( ( log ` ( n / d ) ) ^ 2 ) ) / x ) - ( 2 x. ( log ` x ) ) ) ) e. O(1)