Metamath Proof Explorer

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 ∈ 1 +∞ ⟼ ∑ n = 1 x Λ ⁡ n n ⁢ ∑ m = 1 x n Λ ⁡ m m log ⁡ x − log ⁡ x 2 ∈ 𝑂⁡1

Proof

Step Hyp Ref Expression
1 vmadivsumb ⊢ ∃ c ∈ ℝ + ∀ y ∈ 1 +∞ ∑ i = 1 y Λ ⁡ i i − log ⁡ y ≤ c
2 simpl ⊢ c ∈ ℝ + ∧ ∀ y ∈ 1 +∞ ∑ i = 1 y Λ ⁡ i i − log ⁡ y ≤ c → c ∈ ℝ +
3 simpr ⊢ c ∈ ℝ + ∧ ∀ y ∈ 1 +∞ ∑ i = 1 y Λ ⁡ i i − log ⁡ y ≤ c → ∀ y ∈ 1 +∞ ∑ i = 1 y Λ ⁡ i i − log ⁡ y ≤ c
4 2 3 2vmadivsumlem ⊢ c ∈ ℝ + ∧ ∀ y ∈ 1 +∞ ∑ i = 1 y Λ ⁡ i i − log ⁡ y ≤ c → x ∈ 1 +∞ ⟼ ∑ n = 1 x Λ ⁡ n n ⁢ ∑ m = 1 x n Λ ⁡ m m log ⁡ x − log ⁡ x 2 ∈ 𝑂⁡1
5 4 rexlimiva ⊢ ∃ c ∈ ℝ + ∀ y ∈ 1 +∞ ∑ i = 1 y Λ ⁡ i i − log ⁡ y ≤ c → x ∈ 1 +∞ ⟼ ∑ n = 1 x Λ ⁡ n n ⁢ ∑ m = 1 x n Λ ⁡ m m log ⁡ x − log ⁡ x 2 ∈ 𝑂⁡1
6 1 5 ax-mp ⊢ x ∈ 1 +∞ ⟼ ∑ n = 1 x Λ ⁡ n n ⁢ ∑ m = 1 x n Λ ⁡ m m log ⁡ x − log ⁡ x 2 ∈ 𝑂⁡1