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 ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)

Proof

Step Hyp Ref Expression
1 fvoveq1 ⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( log ‘ ( 𝑛 / 𝑑 ) ) = ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) )
2 1 oveq1d ⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) = ( ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ↑ 2 ) )
3 2 oveq2d ⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ) = ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ↑ 2 ) ) )
4 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
5 ssrab2 ⊢ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ⊆ ℕ
6 simprr ⊢ ( ( 𝑥 ∈ ℝ+ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } )
7 5 6 sselid ⊢ ( ( 𝑥 ∈ ℝ+ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → 𝑑 ∈ ℕ )
8 mucl ⊢ ( 𝑑 ∈ ℕ → ( μ ‘ 𝑑 ) ∈ ℤ )
9 7 8 syl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( μ ‘ 𝑑 ) ∈ ℤ )
10 9 zcnd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( μ ‘ 𝑑 ) ∈ ℂ )
11 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
12 11 nnrpd ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℝ+ )
13 12 ad2antrl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → 𝑛 ∈ ℝ+ )
14 7 nnrpd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → 𝑑 ∈ ℝ+ )
15 13 14 rpdivcld ⊢ ( ( 𝑥 ∈ ℝ+ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( 𝑛 / 𝑑 ) ∈ ℝ+ )
16 relogcl ⊢ ( ( 𝑛 / 𝑑 ) ∈ ℝ+ → ( log ‘ ( 𝑛 / 𝑑 ) ) ∈ ℝ )
17 16 recnd ⊢ ( ( 𝑛 / 𝑑 ) ∈ ℝ+ → ( log ‘ ( 𝑛 / 𝑑 ) ) ∈ ℂ )
18 15 17 syl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( log ‘ ( 𝑛 / 𝑑 ) ) ∈ ℂ )
19 18 sqcld ⊢ ( ( 𝑥 ∈ ℝ+ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ∈ ℂ )
20 10 19 mulcld ⊢ ( ( 𝑥 ∈ ℝ+ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ) ) → ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ) ∈ ℂ )
21 3 4 20 dvdsflsumcom ⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ↑ 2 ) ) )
22 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) → 𝑚 ∈ ℕ )
23 22 3ad2ant3 ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑚 ∈ ℕ )
24 23 nncnd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑚 ∈ ℂ )
25 elfznn ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑑 ∈ ℕ )
26 25 3ad2ant2 ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑑 ∈ ℕ )
27 26 nncnd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑑 ∈ ℂ )
28 26 nnne0d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → 𝑑 ≠ 0 )
29 24 27 28 divcan3d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( 𝑑 · 𝑚 ) / 𝑑 ) = 𝑚 )
30 29 fveq2d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) = ( log ‘ 𝑚 ) )
31 30 oveq1d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ↑ 2 ) = ( ( log ‘ 𝑚 ) ↑ 2 ) )
32 31 oveq2d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ) → ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ↑ 2 ) ) = ( ( μ ‘ 𝑑 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) )
33 32 2sumeq2dv ⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ↑ 2 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) )
34 21 33 eqtrd ⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) )
35 34 oveq1d ⊢ ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ) / 𝑥 ) = ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) )
36 35 oveq1d ⊢ ( 𝑥 ∈ ℝ+ → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
37 36 mpteq2ia ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
38 eqid ⊢ ( ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑑 ) ) ) ) ) / 𝑑 ) = ( ( ( ( log ‘ ( 𝑥 / 𝑑 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑑 ) ) ) ) ) / 𝑑 )
39 38 selberglem2 ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)
40 37 39 eqeltri ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑑 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( 𝑛 / 𝑑 ) ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)