Metamath Proof Explorer


Theorem selberg3lem1

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.4.21 of Shapiro, p. 422. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Hypotheses selberg3lem1.1 ( 𝜑𝐴 ∈ ℝ+ )
selberg3lem1.2 ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ≤ 𝐴 )
Assertion selberg3lem1 ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 selberg3lem1.1 ( 𝜑𝐴 ∈ ℝ+ )
2 selberg3lem1.2 ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ≤ 𝐴 )
3 1red ( 𝜑 → 1 ∈ ℝ )
4 ioossre ( 1 (,) +∞ ) ⊆ ℝ
5 1 rpcnd ( 𝜑𝐴 ∈ ℂ )
6 o1const ( ( ( 1 (,) +∞ ) ⊆ ℝ ∧ 𝐴 ∈ ℂ ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 𝐴 ) ∈ 𝑂(1) )
7 4 5 6 sylancr ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 𝐴 ) ∈ 𝑂(1) )
8 fzfid ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
9 elfznn ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
10 9 adantl ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
11 vmacl ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
12 10 11 syl ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
13 12 10 nndivred ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
14 8 13 fsumrecl ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
15 elioore ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ )
16 eliooord ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥𝑥 < +∞ ) )
17 16 simpld ( 𝑥 ∈ ( 1 (,) +∞ ) → 1 < 𝑥 )
18 15 17 rplogcld ( 𝑥 ∈ ( 1 (,) +∞ ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
19 rpdivcl ( ( 𝐴 ∈ ℝ+ ∧ ( log ‘ 𝑥 ) ∈ ℝ+ ) → ( 𝐴 / ( log ‘ 𝑥 ) ) ∈ ℝ+ )
20 1 18 19 syl2an ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 / ( log ‘ 𝑥 ) ) ∈ ℝ+ )
21 20 rpred ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 / ( log ‘ 𝑥 ) ) ∈ ℝ )
22 14 21 remulcld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ∈ ℝ )
23 22 recnd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ∈ ℂ )
24 5 adantr ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐴 ∈ ℂ )
25 14 recnd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
26 18 adantl ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
27 26 rpcnd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
28 20 rpcnd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 / ( log ‘ 𝑥 ) ) ∈ ℂ )
29 25 27 28 subdird ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) − ( ( log ‘ 𝑥 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) )
30 26 rpne0d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ≠ 0 )
31 24 27 30 divcan2d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) = 𝐴 )
32 31 oveq2d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) − ( ( log ‘ 𝑥 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) − 𝐴 ) )
33 29 32 eqtrd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) − 𝐴 ) )
34 33 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) − 𝐴 ) ) )
35 26 rpred ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
36 14 35 resubcld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ∈ ℝ )
37 15 adantl ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ )
38 0red ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ∈ ℝ )
39 1red ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ )
40 0lt1 0 < 1
41 40 a1i ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → 0 < 1 )
42 17 adantl ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 𝑥 )
43 38 39 37 41 42 lttrd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → 0 < 𝑥 )
44 37 43 elrpd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ+ )
45 44 ex ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ+ ) )
46 45 ssrdv ( 𝜑 → ( 1 (,) +∞ ) ⊆ ℝ+ )
47 vmadivsum ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1)
48 47 a1i ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
49 46 48 o1res2 ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
50 4 a1i ( 𝜑 → ( 1 (,) +∞ ) ⊆ ℝ )
51 ere e ∈ ℝ
52 51 a1i ( 𝜑 → e ∈ ℝ )
53 1 rpred ( 𝜑𝐴 ∈ ℝ )
54 20 adantrr ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( 𝐴 / ( log ‘ 𝑥 ) ) ∈ ℝ+ )
55 54 rprege0d ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( ( 𝐴 / ( log ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / ( log ‘ 𝑥 ) ) ) )
56 absid ( ( ( 𝐴 / ( log ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / ( log ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝐴 / ( log ‘ 𝑥 ) ) ) = ( 𝐴 / ( log ‘ 𝑥 ) ) )
57 55 56 syl ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( abs ‘ ( 𝐴 / ( log ‘ 𝑥 ) ) ) = ( 𝐴 / ( log ‘ 𝑥 ) ) )
58 loge ( log ‘ e ) = 1
59 simprr ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → e ≤ 𝑥 )
60 epr e ∈ ℝ+
61 44 adantrr ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → 𝑥 ∈ ℝ+ )
62 logleb ( ( e ∈ ℝ+𝑥 ∈ ℝ+ ) → ( e ≤ 𝑥 ↔ ( log ‘ e ) ≤ ( log ‘ 𝑥 ) ) )
63 60 61 62 sylancr ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( e ≤ 𝑥 ↔ ( log ‘ e ) ≤ ( log ‘ 𝑥 ) ) )
64 59 63 mpbid ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( log ‘ e ) ≤ ( log ‘ 𝑥 ) )
65 58 64 eqbrtrrid ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → 1 ≤ ( log ‘ 𝑥 ) )
66 1rp 1 ∈ ℝ+
67 rpregt0 ( 1 ∈ ℝ+ → ( 1 ∈ ℝ ∧ 0 < 1 ) )
68 66 67 mp1i ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( 1 ∈ ℝ ∧ 0 < 1 ) )
69 26 adantrr ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
70 69 rpregt0d ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) ∈ ℝ ∧ 0 < ( log ‘ 𝑥 ) ) )
71 1 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → 𝐴 ∈ ℝ+ )
72 71 rpregt0d ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) )
73 lediv2 ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( ( log ‘ 𝑥 ) ∈ ℝ ∧ 0 < ( log ‘ 𝑥 ) ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 1 ≤ ( log ‘ 𝑥 ) ↔ ( 𝐴 / ( log ‘ 𝑥 ) ) ≤ ( 𝐴 / 1 ) ) )
74 68 70 72 73 syl3anc ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( 1 ≤ ( log ‘ 𝑥 ) ↔ ( 𝐴 / ( log ‘ 𝑥 ) ) ≤ ( 𝐴 / 1 ) ) )
75 65 74 mpbid ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( 𝐴 / ( log ‘ 𝑥 ) ) ≤ ( 𝐴 / 1 ) )
76 5 adantr ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → 𝐴 ∈ ℂ )
77 76 div1d ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( 𝐴 / 1 ) = 𝐴 )
78 75 77 breqtrd ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( 𝐴 / ( log ‘ 𝑥 ) ) ≤ 𝐴 )
79 57 78 eqbrtrd ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( abs ‘ ( 𝐴 / ( log ‘ 𝑥 ) ) ) ≤ 𝐴 )
80 50 28 52 53 79 elo1d ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 𝐴 / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
81 36 21 49 80 o1mul2 ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
82 34 81 eqeltrrd ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) − 𝐴 ) ) ∈ 𝑂(1) )
83 23 24 82 o1dif ( 𝜑 → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 𝐴 ) ∈ 𝑂(1) ) )
84 7 83 mpbird ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
85 2re 2 ∈ ℝ
86 rerpdivcl ( ( 2 ∈ ℝ ∧ ( log ‘ 𝑥 ) ∈ ℝ+ ) → ( 2 / ( log ‘ 𝑥 ) ) ∈ ℝ )
87 85 26 86 sylancr ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 / ( log ‘ 𝑥 ) ) ∈ ℝ )
88 nndivre ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
89 37 9 88 syl2an ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
90 chpcl ( ( 𝑥 / 𝑛 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
91 89 90 syl ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
92 12 91 remulcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
93 10 nnrpd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
94 93 relogcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
95 92 94 remulcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
96 8 95 fsumrecl ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
97 87 96 remulcld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℝ )
98 8 92 fsumrecl ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
99 97 98 resubcld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
100 99 44 rerpdivcld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ∈ ℝ )
101 100 recnd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ∈ ℂ )
102 101 abscld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ∈ ℝ )
103 23 abscld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) ∈ ℝ )
104 2cnd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℂ )
105 96 recnd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
106 104 105 mulcld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℂ )
107 98 recnd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
108 107 27 mulcld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
109 106 108 subcld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
110 109 abscld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) ∈ ℝ )
111 43 gt0ne0d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ≠ 0 )
112 110 37 111 redivcld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / 𝑥 ) ∈ ℝ )
113 53 adantr ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐴 ∈ ℝ )
114 14 113 remulcld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝐴 ) ∈ ℝ )
115 12 recnd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
116 fzfid ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ Fin )
117 elfznn ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) → 𝑚 ∈ ℕ )
118 117 adantl ( ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℕ )
119 vmacl ( 𝑚 ∈ ℕ → ( Λ ‘ 𝑚 ) ∈ ℝ )
120 118 119 syl ( ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ )
121 118 nnrpd ( ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℝ+ )
122 121 relogcld ( ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ )
123 120 122 remulcld ( ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ )
124 116 123 fsumrecl ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ )
125 9 nnrpd ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℝ+ )
126 rpdivcl ( ( 𝑥 ∈ ℝ+𝑛 ∈ ℝ+ ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
127 44 125 126 syl2an ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
128 127 relogcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
129 91 128 remulcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
130 124 129 resubcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
131 130 recnd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
132 115 131 mulcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ )
133 8 132 fsumcl ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ )
134 133 abscld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ∈ ℝ )
135 132 abscld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ∈ ℝ )
136 8 135 fsumrecl ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ∈ ℝ )
137 113 37 remulcld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 · 𝑥 ) ∈ ℝ )
138 14 137 remulcld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) ∈ ℝ )
139 8 132 fsumabs ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) )
140 53 ad2antrr ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐴 ∈ ℝ )
141 37 adantr ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ )
142 140 141 remulcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐴 · 𝑥 ) ∈ ℝ )
143 13 142 remulcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) ∈ ℝ )
144 131 abscld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℝ )
145 142 10 nndivred ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐴 · 𝑥 ) / 𝑛 ) ∈ ℝ )
146 vmage0 ( 𝑛 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑛 ) )
147 10 146 syl ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) )
148 89 recnd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℂ )
149 127 rpne0d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ≠ 0 )
150 131 148 149 absdivd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( 𝑥 / 𝑛 ) ) ) = ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( abs ‘ ( 𝑥 / 𝑛 ) ) ) )
151 127 rpge0d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( 𝑥 / 𝑛 ) )
152 89 151 absidd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑥 / 𝑛 ) ) = ( 𝑥 / 𝑛 ) )
153 152 oveq2d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( abs ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 / 𝑛 ) ) )
154 150 153 eqtrd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( 𝑥 / 𝑛 ) ) ) = ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 / 𝑛 ) ) )
155 fveq2 ( 𝑘 = 𝑚 → ( Λ ‘ 𝑘 ) = ( Λ ‘ 𝑚 ) )
156 fveq2 ( 𝑘 = 𝑚 → ( log ‘ 𝑘 ) = ( log ‘ 𝑚 ) )
157 155 156 oveq12d ( 𝑘 = 𝑚 → ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) = ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) )
158 157 cbvsumv Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) )
159 fveq2 ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ⌊ ‘ 𝑦 ) = ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) )
160 159 oveq2d ( 𝑦 = ( 𝑥 / 𝑛 ) → ( 1 ... ( ⌊ ‘ 𝑦 ) ) = ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) )
161 160 sumeq1d ( 𝑦 = ( 𝑥 / 𝑛 ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) )
162 158 161 syl5eq ( 𝑦 = ( 𝑥 / 𝑛 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) )
163 fveq2 ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ψ ‘ 𝑦 ) = ( ψ ‘ ( 𝑥 / 𝑛 ) ) )
164 fveq2 ( 𝑦 = ( 𝑥 / 𝑛 ) → ( log ‘ 𝑦 ) = ( log ‘ ( 𝑥 / 𝑛 ) ) )
165 163 164 oveq12d ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) = ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) )
166 162 165 oveq12d ( 𝑦 = ( 𝑥 / 𝑛 ) → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
167 id ( 𝑦 = ( 𝑥 / 𝑛 ) → 𝑦 = ( 𝑥 / 𝑛 ) )
168 166 167 oveq12d ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) = ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( 𝑥 / 𝑛 ) ) )
169 168 fveq2d ( 𝑦 = ( 𝑥 / 𝑛 ) → ( abs ‘ ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) = ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( 𝑥 / 𝑛 ) ) ) )
170 169 breq1d ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ( abs ‘ ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ≤ 𝐴 ↔ ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( 𝑥 / 𝑛 ) ) ) ≤ 𝐴 ) )
171 2 ad2antrr ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ≤ 𝐴 )
172 10 nncnd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ )
173 172 mulid2d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · 𝑛 ) = 𝑛 )
174 fznnfl ( 𝑥 ∈ ℝ → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛𝑥 ) ) )
175 37 174 syl ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛𝑥 ) ) )
176 175 simplbda ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛𝑥 )
177 173 176 eqbrtrd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · 𝑛 ) ≤ 𝑥 )
178 1red ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
179 178 141 93 lemuldivd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 · 𝑛 ) ≤ 𝑥 ↔ 1 ≤ ( 𝑥 / 𝑛 ) ) )
180 177 179 mpbid ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ≤ ( 𝑥 / 𝑛 ) )
181 1re 1 ∈ ℝ
182 elicopnf ( 1 ∈ ℝ → ( ( 𝑥 / 𝑛 ) ∈ ( 1 [,) +∞ ) ↔ ( ( 𝑥 / 𝑛 ) ∈ ℝ ∧ 1 ≤ ( 𝑥 / 𝑛 ) ) ) )
183 181 182 ax-mp ( ( 𝑥 / 𝑛 ) ∈ ( 1 [,) +∞ ) ↔ ( ( 𝑥 / 𝑛 ) ∈ ℝ ∧ 1 ≤ ( 𝑥 / 𝑛 ) ) )
184 89 180 183 sylanbrc ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ( 1 [,) +∞ ) )
185 170 171 184 rspcdva ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( 𝑥 / 𝑛 ) ) ) ≤ 𝐴 )
186 154 185 eqbrtrrd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 / 𝑛 ) ) ≤ 𝐴 )
187 144 140 127 ledivmul2d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 / 𝑛 ) ) ≤ 𝐴 ↔ ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ≤ ( 𝐴 · ( 𝑥 / 𝑛 ) ) ) )
188 186 187 mpbid ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ≤ ( 𝐴 · ( 𝑥 / 𝑛 ) ) )
189 24 adantr ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐴 ∈ ℂ )
190 141 recnd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℂ )
191 10 nnne0d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≠ 0 )
192 189 190 172 191 divassd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐴 · 𝑥 ) / 𝑛 ) = ( 𝐴 · ( 𝑥 / 𝑛 ) ) )
193 188 192 breqtrrd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ≤ ( ( 𝐴 · 𝑥 ) / 𝑛 ) )
194 144 145 12 147 193 lemul2ad ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ≤ ( ( Λ ‘ 𝑛 ) · ( ( 𝐴 · 𝑥 ) / 𝑛 ) ) )
195 115 131 absmuld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) = ( ( abs ‘ ( Λ ‘ 𝑛 ) ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) )
196 12 147 absidd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Λ ‘ 𝑛 ) ) = ( Λ ‘ 𝑛 ) )
197 196 oveq1d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( Λ ‘ 𝑛 ) ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) = ( ( Λ ‘ 𝑛 ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) )
198 195 197 eqtrd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) = ( ( Λ ‘ 𝑛 ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) )
199 142 recnd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐴 · 𝑥 ) ∈ ℂ )
200 115 172 199 191 div32d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) = ( ( Λ ‘ 𝑛 ) · ( ( 𝐴 · 𝑥 ) / 𝑛 ) ) )
201 194 198 200 3brtr4d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ≤ ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) )
202 8 135 143 201 fsumle ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) )
203 37 recnd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℂ )
204 24 203 mulcld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 · 𝑥 ) ∈ ℂ )
205 115 172 191 divcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
206 8 204 205 fsummulc1 ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) )
207 202 206 breqtrrd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) )
208 134 136 138 139 207 letrd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) )
209 124 recnd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ )
210 91 recnd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
211 94 recnd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℂ )
212 210 211 mulcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
213 209 212 addcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℂ )
214 115 213 mulcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) ∈ ℂ )
215 115 210 mulcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
216 27 adantr ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
217 215 216 mulcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
218 8 214 217 fsumsub ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) − ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) )
219 210 216 mulcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
220 115 213 219 subdid ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) − ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) ) ) )
221 44 adantr ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ )
222 221 93 relogdivd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) = ( ( log ‘ 𝑥 ) − ( log ‘ 𝑛 ) ) )
223 222 oveq2d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( ( log ‘ 𝑥 ) − ( log ‘ 𝑛 ) ) ) )
224 210 216 211 subdid ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( ( log ‘ 𝑥 ) − ( log ‘ 𝑛 ) ) ) = ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) )
225 223 224 eqtrd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) )
226 225 oveq2d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) )
227 209 219 212 subsub3d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) = ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) ) )
228 226 227 eqtrd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) ) )
229 228 oveq2d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) ) ) )
230 115 210 216 mulassd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) = ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) ) )
231 230 oveq2d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) − ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) = ( ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) − ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) ) ) )
232 220 229 231 3eqtr4d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) − ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) )
233 232 sumeq2dv ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) − ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) )
234 fveq2 ( 𝑛 = 𝑚 → ( Λ ‘ 𝑛 ) = ( Λ ‘ 𝑚 ) )
235 oveq2 ( 𝑛 = 𝑚 → ( 𝑥 / 𝑛 ) = ( 𝑥 / 𝑚 ) )
236 235 fveq2d ( 𝑛 = 𝑚 → ( ψ ‘ ( 𝑥 / 𝑛 ) ) = ( ψ ‘ ( 𝑥 / 𝑚 ) ) )
237 234 236 oveq12d ( 𝑛 = 𝑚 → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) )
238 fveq2 ( 𝑛 = 𝑚 → ( log ‘ 𝑛 ) = ( log ‘ 𝑚 ) )
239 237 238 oveq12d ( 𝑛 = 𝑚 → ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) = ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) )
240 239 cbvsumv Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) )
241 elfznn ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) → 𝑛 ∈ ℕ )
242 241 adantl ( ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → 𝑛 ∈ ℕ )
243 242 11 syl ( ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
244 243 recnd ( ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
245 244 anasss ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
246 elfznn ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑚 ∈ ℕ )
247 246 adantl ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℕ )
248 247 119 syl ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ )
249 248 recnd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℂ )
250 247 nnrpd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℝ+ )
251 250 relogcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ )
252 251 recnd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑚 ) ∈ ℂ )
253 249 252 mulcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ )
254 253 adantrr ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ )
255 245 254 mulcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ∈ ℂ )
256 37 255 fsumfldivdiag ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
257 37 adantr ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ )
258 257 247 nndivred ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑚 ) ∈ ℝ )
259 chpcl ( ( 𝑥 / 𝑚 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑚 ) ) ∈ ℝ )
260 258 259 syl ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑚 ) ) ∈ ℝ )
261 260 recnd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑚 ) ) ∈ ℂ )
262 249 261 252 mul32d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) = ( ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) )
263 248 251 remulcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ )
264 263 recnd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ )
265 264 261 mulcomd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) = ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
266 chpval ( ( 𝑥 / 𝑚 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑚 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( Λ ‘ 𝑛 ) )
267 258 266 syl ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑚 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( Λ ‘ 𝑛 ) )
268 267 oveq1d ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
269 fzfid ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ∈ Fin )
270 269 264 244 fsummulc1 ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
271 268 270 eqtrd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
272 262 265 271 3eqtrd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
273 272 sumeq2dv ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
274 123 recnd ( ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ )
275 116 115 274 fsummulc2 ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
276 275 sumeq2dv ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
277 256 273 276 3eqtr4d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
278 240 277 syl5eq ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) )
279 115 210 211 mulassd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) = ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) )
280 279 sumeq2dv ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) )
281 278 280 oveq12d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) )
282 105 2timesd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) )
283 115 209 mulcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ∈ ℂ )
284 115 212 mulcld ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℂ )
285 8 283 284 fsumadd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) )
286 281 282 285 3eqtr4d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) )
287 115 209 212 adddid ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) )
288 287 sumeq2dv ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) )
289 286 288 eqtr4d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) )
290 92 recnd ( ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
291 8 27 290 fsummulc1 ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) )
292 289 291 oveq12d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) )
293 218 233 292 3eqtr4rd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) )
294 293 fveq2d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) = ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) )
295 25 24 203 mulassd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝐴 ) · 𝑥 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) )
296 208 294 295 3brtr4d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) ≤ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝐴 ) · 𝑥 ) )
297 110 114 44 ledivmul2d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / 𝑥 ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝐴 ) ↔ ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) ≤ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝐴 ) · 𝑥 ) ) )
298 296 297 mpbird ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / 𝑥 ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝐴 ) )
299 112 114 26 298 lediv1dd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / 𝑥 ) / ( log ‘ 𝑥 ) ) ≤ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝐴 ) / ( log ‘ 𝑥 ) ) )
300 110 recnd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) ∈ ℂ )
301 300 203 27 111 30 divdiv1d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / 𝑥 ) / ( log ‘ 𝑥 ) ) = ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
302 109 27 203 30 111 divdiv32d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / ( log ‘ 𝑥 ) ) / 𝑥 ) = ( ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) / ( log ‘ 𝑥 ) ) )
303 106 108 27 30 divsubdird ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / ( log ‘ 𝑥 ) ) = ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) ) )
304 104 105 27 30 div23d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) )
305 107 27 30 divcan4d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) )
306 304 305 oveq12d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
307 303 306 eqtrd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / ( log ‘ 𝑥 ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
308 307 oveq1d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / ( log ‘ 𝑥 ) ) / 𝑥 ) = ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) )
309 109 203 27 111 30 divdiv1d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) / ( log ‘ 𝑥 ) ) = ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
310 302 308 309 3eqtr3d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) = ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
311 310 fveq2d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) = ( abs ‘ ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
312 44 26 rpmulcld ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℝ+ )
313 312 rpcnd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℂ )
314 312 rpne0d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ≠ 0 )
315 109 313 314 absdivd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) = ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / ( abs ‘ ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
316 312 rpred ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℝ )
317 312 rpge0d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( 𝑥 · ( log ‘ 𝑥 ) ) )
318 316 317 absidd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( 𝑥 · ( log ‘ 𝑥 ) ) )
319 318 oveq2d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / ( abs ‘ ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) = ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
320 311 315 319 3eqtrd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) = ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
321 301 320 eqtr4d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / 𝑥 ) / ( log ‘ 𝑥 ) ) = ( abs ‘ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) )
322 25 24 27 30 divassd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝐴 ) / ( log ‘ 𝑥 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) )
323 299 321 322 3brtr3d ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) )
324 22 leabsd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ≤ ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) )
325 102 22 103 323 324 letrd ( ( 𝜑𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ≤ ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) )
326 325 adantrr ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ≤ ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) )
327 3 84 22 101 326 o1le ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) )