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	⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) / 𝑚 ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1)

Proof

Step	Hyp	Ref	Expression
1		vmadivsumb	⊢ ∃ 𝑐 ∈ ℝ+ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) / 𝑖 ) − ( log ‘ 𝑦 ) ) ) ≤ 𝑐
2		simpl	⊢ ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) / 𝑖 ) − ( log ‘ 𝑦 ) ) ) ≤ 𝑐 ) → 𝑐 ∈ ℝ+ )
3		simpr	⊢ ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) / 𝑖 ) − ( log ‘ 𝑦 ) ) ) ≤ 𝑐 ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) / 𝑖 ) − ( log ‘ 𝑦 ) ) ) ≤ 𝑐 )
4	2 3	2vmadivsumlem	⊢ ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) / 𝑖 ) − ( log ‘ 𝑦 ) ) ) ≤ 𝑐 ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) / 𝑚 ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1) )
5	4	rexlimiva	⊢ ( ∃ 𝑐 ∈ ℝ+ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) / 𝑖 ) − ( log ‘ 𝑦 ) ) ) ≤ 𝑐 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) / 𝑚 ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1) )
6	1 5	ax-mp	⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) / 𝑚 ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1)