Theorem 2vmadivsum

Description: The sum sum_ m n <_ x , Lam ( m ) Lam ( n ) / m n is asymptotic to log ^ 2 ( x ) / 2 + O ( log x ) . (Contributed by Mario Carneiro, 30-May-2016)

	Ref	Expression
Assertion	2vmadivsum	|- ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1)

Proof

Step	Hyp	Ref	Expression
1		vmadivsumb	|- E. c e. RR+ A. y e. ( 1 [,) +oo ) ( abs ` ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) / i ) - ( log ` y ) ) ) <_ c
2		simpl	|- ( ( c e. RR+ /\ A. y e. ( 1 [,) +oo ) ( abs ` ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) / i ) - ( log ` y ) ) ) <_ c ) -> c e. RR+ )
3		simpr	|- ( ( c e. RR+ /\ A. y e. ( 1 [,) +oo ) ( abs ` ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) / i ) - ( log ` y ) ) ) <_ c ) -> A. y e. ( 1 [,) +oo ) ( abs ` ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) / i ) - ( log ` y ) ) ) <_ c )
4	2 3	2vmadivsumlem	|- ( ( c e. RR+ /\ A. y e. ( 1 [,) +oo ) ( abs ` ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) / i ) - ( log ` y ) ) ) <_ c ) -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) )
5	4	rexlimiva	|- ( E. c e. RR+ A. y e. ( 1 [,) +oo ) ( abs ` ( sum_ i e. ( 1 ... ( |_ ` y ) ) ( ( Lam ` i ) / i ) - ( log ` y ) ) ) <_ c -> ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1) )
6	1 5	ax-mp	|- ( x e. ( 1 (,) +oo ) |-> ( ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( ( Lam ` n ) / n ) x. sum_ m e. ( 1 ... ( |_ ` ( x / n ) ) ) ( ( Lam ` m ) / m ) ) / ( log ` x ) ) - ( ( log ` x ) / 2 ) ) ) e. O(1)