Metamath Proof Explorer


Theorem selberg3

Description: Introduce a log weighting on the summands of sum_ m x. n <_ x , Lam ( m ) Lam ( n ) , the core of selberg2 (written here as sum_ n <_ x , Lam ( n ) psi ( x / n ) ). Equation 10.6.7 of Shapiro, p. 422. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Assertion selberg3 ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)

Proof

Step Hyp Ref Expression
1 elioore ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ )
2 1 adantl ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ )
3 chpcl ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) ∈ ℝ )
4 2 3 syl ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ψ ‘ 𝑥 ) ∈ ℝ )
5 1rp 1 ∈ ℝ+
6 5 a1i ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ+ )
7 1red ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ )
8 eliooord ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥𝑥 < +∞ ) )
9 8 adantl ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 < 𝑥𝑥 < +∞ ) )
10 9 simpld ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 𝑥 )
11 7 2 10 ltled ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ≤ 𝑥 )
12 2 6 11 rpgecld ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ+ )
13 12 relogcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
14 4 13 remulcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ )
15 14 recnd ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
16 fzfid ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
17 elfznn ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
18 17 adantl ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
19 vmacl ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
20 18 19 syl ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
21 2 adantr ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ )
22 21 18 nndivred ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
23 chpcl ( ( 𝑥 / 𝑛 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
24 22 23 syl ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
25 20 24 remulcld ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
26 16 25 fsumrecl ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
27 26 recnd ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
28 2re 2 ∈ ℝ
29 28 a1i ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℝ )
30 2 10 rplogcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
31 29 30 rerpdivcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 / ( log ‘ 𝑥 ) ) ∈ ℝ )
32 18 nnrpd ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
33 32 relogcld ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
34 25 33 remulcld ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
35 16 34 fsumrecl ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
36 31 35 remulcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℝ )
37 36 26 resubcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
38 37 recnd ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
39 15 27 38 addassd ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) + ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) + ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) )
40 2cnd ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℂ )
41 13 recnd ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
42 30 rpne0d ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ≠ 0 )
43 40 41 42 divcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 / ( log ‘ 𝑥 ) ) ∈ ℂ )
44 35 recnd ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
45 43 44 mulcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℂ )
46 27 45 pncan3d ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) + ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) )
47 46 oveq2d ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) + ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) = ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
48 39 47 eqtr2d ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) = ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) + ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ) )
49 48 oveq1d ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) + ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / 𝑥 ) )
50 14 26 readdcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
51 50 recnd ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
52 2 recnd ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℂ )
53 12 rpne0d ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ≠ 0 )
54 51 38 52 53 divdird ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) + ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / 𝑥 ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) + ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) )
55 49 54 eqtrd ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) = ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) + ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) )
56 55 oveq1d ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) + ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
57 50 12 rerpdivcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ∈ ℝ )
58 57 recnd ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ∈ ℂ )
59 37 12 rerpdivcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ∈ ℝ )
60 59 recnd ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ∈ ℂ )
61 29 13 remulcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℝ )
62 61 recnd ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℂ )
63 58 60 62 addsubd ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) + ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) + ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) )
64 56 63 eqtrd ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) + ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) )
65 64 mpteq2dva ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) + ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ) )
66 57 61 resubcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
67 12 ex ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ+ ) )
68 67 ssrdv ( ⊤ → ( 1 (,) +∞ ) ⊆ ℝ+ )
69 selberg2 ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)
70 69 a1i ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
71 68 70 o1res2 ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
72 selberg3lem2 ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1)
73 72 a1i ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) )
74 66 59 71 73 o1add2 ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) + ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ) ∈ 𝑂(1) )
75 65 74 eqeltrd ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
76 75 mptru ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)