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) )