Metamath Proof Explorer

Theorem selberg4

Description: The Selberg symmetry formula for products of three primes, instead of two. The sum here can also be written in the symmetric form sum_ i j k <_ x , Lam ( i ) Lam ( j ) Lam ( k ) ; we eliminate one of the nested sums by using the definition of psi ( x ) = sum_ k <_ x , Lam ( k ) . This statement can thus equivalently be written psi ( x ) log ^ 2 ( x ) = 2 sum_ i j k <_ x , Lam ( i ) Lam ( j ) Lam ( k ) + O ( x log x ) . Equation 10.4.23 of Shapiro, p. 422. (Contributed by Mario Carneiro, 30-May-2016)

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

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 1 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℝ )
3 elioore ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ )
4 3 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ )
5 eliooord ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
6 5 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
7 6 simpld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 𝑥 )
8 4 7 rplogcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
9 2 8 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 / ( log ‘ 𝑥 ) ) ∈ ℝ )
10 fzfid ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
11 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑚 ∈ ℕ )
12 11 adantl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℕ )
13 vmacl ⊢ ( 𝑚 ∈ ℕ → ( Λ ‘ 𝑚 ) ∈ ℝ )
14 12 13 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ )
15 4 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ )
16 15 12 nndivred ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑚 ) ∈ ℝ )
17 chpcl ⊢ ( ( 𝑥 / 𝑚 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑚 ) ) ∈ ℝ )
18 16 17 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑚 ) ) ∈ ℝ )
19 14 18 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ∈ ℝ )
20 12 nnrpd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℝ+ )
21 20 relogcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ )
22 19 21 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ∈ ℝ )
23 10 22 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ∈ ℝ )
24 9 23 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) ∈ ℝ )
25 10 19 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ∈ ℝ )
26 24 25 resubcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) ∈ ℝ )
27 1rp ⊢ 1 ∈ ℝ+
28 27 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ+ )
29 1red ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ )
30 29 4 7 ltled ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ≤ 𝑥 )
31 4 28 30 rpgecld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ+ )
32 26 31 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ∈ ℝ )
33 32 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ∈ ℂ )
34 chpcl ⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) ∈ ℝ )
35 4 34 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ψ ‘ 𝑥 ) ∈ ℝ )
36 31 relogcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
37 35 36 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ )
38 37 25 readdcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) ∈ ℝ )
39 38 31 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ∈ ℝ )
40 39 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ∈ ℂ )
41 2 36 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℝ )
42 41 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℂ )
43 33 40 42 addsubassd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) + ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) + ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) )
44 26 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) ∈ ℂ )
45 38 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) ∈ ℂ )
46 4 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℂ )
47 31 rpne0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ≠ 0 )
48 44 45 46 47 divdird ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) + ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) / 𝑥 ) = ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) + ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ) )
49 24 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) ∈ ℂ )
50 25 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ∈ ℂ )
51 37 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
52 49 50 51 nppcan3d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) + ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
53 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) → 𝑛 ∈ ℕ )
54 53 ad2antll ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → 𝑛 ∈ ℕ )
55 vmacl ⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
56 54 55 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
57 14 adantrr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ )
58 20 adantrr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → 𝑚 ∈ ℝ+ )
59 58 relogcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ )
60 57 59 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ )
61 56 60 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ∈ ℝ )
62 61 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ∈ ℂ )
63 4 62 fsumfldivdiag ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
64 14 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℂ )
65 18 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑚 ) ) ∈ ℂ )
66 21 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑚 ) ∈ ℂ )
67 64 65 66 mul32d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) = ( ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) )
68 64 66 mulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ )
69 68 65 mulcomd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) = ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
70 chpval ⊢ ( ( 𝑥 / 𝑚 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑚 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( Λ ‘ 𝑛 ) )
71 16 70 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑚 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( Λ ‘ 𝑛 ) )
72 71 oveq1d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
73 fzfid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ∈ Fin )
74 56 anassrs ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
75 74 recnd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
76 73 68 75 fsummulc1 ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
77 72 76 eqtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
78 67 69 77 3eqtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
79 78 sumeq2dv ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
80 fzfid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ Fin )
81 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
82 81 adantl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
83 82 55 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
84 83 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
85 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) → 𝑚 ∈ ℕ )
86 85 adantl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℕ )
87 86 13 syl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ )
88 86 nnrpd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℝ+ )
89 88 relogcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ )
90 87 89 remulcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ )
91 90 recnd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ )
92 80 84 91 fsummulc2 ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
93 92 sumeq2dv ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
94 63 79 93 3eqtr4d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
95 94 oveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) )
96 95 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
97 52 96 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) + ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
98 97 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) + ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) / 𝑥 ) = ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) )
99 48 98 eqtr3d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) + ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ) = ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) )
100 99 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) + ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
101 43 100 eqtr3d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) + ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) = ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
102 101 mpteq2dva ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) + ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) )
103 39 41 resubcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
104 selberg3lem2 ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1)
105 104 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) )
106 31 ex ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ+ ) )
107 106 ssrdv ⊢ ( ⊤ → ( 1 (,) +∞ ) ⊆ ℝ+ )
108 selberg2 ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)
109 108 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
110 107 109 o1res2 ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
111 32 103 105 110 o1add2 ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) + ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ) ∈ 𝑂(1) )
112 102 111 eqeltrrd ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
113 80 90 fsumrecl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ )
114 83 113 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ∈ ℝ )
115 10 114 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ∈ ℝ )
116 9 115 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) ∈ ℝ )
117 116 37 readdcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
118 117 31 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) ∈ ℝ )
119 118 41 resubcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
120 119 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
121 4 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ )
122 121 82 nndivred ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
123 122 adantr ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
124 123 86 nndivred ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( 𝑥 / 𝑛 ) / 𝑚 ) ∈ ℝ )
125 chpcl ⊢ ( ( ( 𝑥 / 𝑛 ) / 𝑚 ) ∈ ℝ → ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ∈ ℝ )
126 124 125 syl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ∈ ℝ )
127 87 126 remulcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ∈ ℝ )
128 80 127 fsumrecl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ∈ ℝ )
129 83 128 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ∈ ℝ )
130 10 129 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ∈ ℝ )
131 9 130 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ∈ ℝ )
132 37 131 resubcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ∈ ℝ )
133 132 31 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ∈ ℝ )
134 133 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ∈ ℂ )
135 116 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) ∈ ℂ )
136 131 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ∈ ℂ )
137 51 135 136 pnncand ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) ) − ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) )
138 135 51 addcomd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) = ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) ) )
139 138 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ) = ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) ) − ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ) )
140 87 recnd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℂ )
141 89 recnd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( log ‘ 𝑚 ) ∈ ℂ )
142 126 recnd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ∈ ℂ )
143 140 141 142 adddid ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) = ( ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) )
144 143 sumeq2dv ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) )
145 127 recnd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ∈ ℂ )
146 80 91 145 fsumadd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) )
147 144 146 eqtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) )
148 147 oveq2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) = ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) )
149 113 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ )
150 128 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ∈ ℂ )
151 84 149 150 adddid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) )
152 148 151 eqtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) )
153 152 sumeq2dv ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) )
154 114 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ∈ ℂ )
155 129 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ∈ ℂ )
156 10 154 155 fsumadd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) )
157 153 156 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) )
158 157 oveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) )
159 9 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 / ( log ‘ 𝑥 ) ) ∈ ℂ )
160 115 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ∈ ℂ )
161 130 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ∈ ℂ )
162 159 160 161 adddid ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) )
163 158 162 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) )
164 137 139 163 3eqtr4d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) )
165 164 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ) / 𝑥 ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) )
166 117 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
167 51 136 subcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ∈ ℂ )
168 166 167 46 47 divsubdird ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ) / 𝑥 ) = ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) )
169 2cnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℂ )
170 89 126 readdcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ∈ ℝ )
171 87 170 remulcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ∈ ℝ )
172 80 171 fsumrecl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ∈ ℝ )
173 83 172 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ∈ ℝ )
174 10 173 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ∈ ℝ )
175 174 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ∈ ℂ )
176 169 175 mulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ∈ ℂ )
177 36 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
178 8 rpne0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ≠ 0 )
179 176 177 46 178 47 divdiv1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) / 𝑥 ) = ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( ( log ‘ 𝑥 ) · 𝑥 ) ) )
180 177 46 mulcomd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) · 𝑥 ) = ( 𝑥 · ( log ‘ 𝑥 ) ) )
181 180 oveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( ( log ‘ 𝑥 ) · 𝑥 ) ) = ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
182 179 181 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) / 𝑥 ) = ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
183 169 175 177 178 div23d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) )
184 183 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) / 𝑥 ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) )
185 31 8 rpmulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℝ+ )
186 185 rpcnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℂ )
187 185 rpne0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ≠ 0 )
188 169 175 186 187 divassd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
189 182 184 188 3eqtr3d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) = ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
190 165 168 189 3eqtr3d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) = ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
191 190 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
192 118 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) ∈ ℂ )
193 192 42 134 sub32d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) − ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) = ( ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
194 174 185 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
195 194 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
196 169 195 177 subdid ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) = ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
197 191 193 196 3eqtr4d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) − ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) = ( 2 · ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) )
198 197 mpteq2dva ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) − ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 2 · ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) ) )
199 194 36 resubcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ∈ ℝ )
200 ioossre ⊢ ( 1 (,) +∞ ) ⊆ ℝ
201 2cnd ⊢ ( ⊤ → 2 ∈ ℂ )
202 o1const ⊢ ( ( ( 1 (,) +∞ ) ⊆ ℝ ∧ 2 ∈ ℂ ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 2 ) ∈ 𝑂(1) )
203 200 201 202 sylancr ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 2 ) ∈ 𝑂(1) )
204 selbergb ⊢ ∃ 𝑐 ∈ ℝ+ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐
205 simpl ⊢ ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐 ) → 𝑐 ∈ ℝ+ )
206 simpr ⊢ ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐 ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐 )
207 205 206 selberg4lem1 ⊢ ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐 ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
208 207 rexlimiva ⊢ ( ∃ 𝑐 ∈ ℝ+ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
209 204 208 mp1i ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
210 2 199 203 209 o1mul2 ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 2 · ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
211 198 210 eqeltrd ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) − ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) ) ∈ 𝑂(1) )
212 120 134 211 o1dif ⊢ ( ⊤ → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) ) )
213 112 212 mpbid ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) )
214 213 mptru ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1)