Metamath Proof Explorer

Theorem selberg4lem1

Description: Lemma for selberg4 . Equation 10.4.20 of Shapiro, p. 422. (Contributed by Mario Carneiro, 30-May-2016)

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

Proof

Step Hyp Ref Expression
1 selberg4lem1.1 ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
2 selberg4lem1.2 ⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝐴 )
3 2cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℂ )
4 fzfid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
5 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
6 5 adantl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
7 vmacl ⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
8 6 7 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
9 8 6 nndivred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
10 elioore ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ )
11 10 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ )
12 1rp ⊢ 1 ∈ ℝ+
13 12 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ+ )
14 1red ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ )
15 eliooord ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
16 15 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
17 16 simpld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 𝑥 )
18 14 11 17 ltled ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ≤ 𝑥 )
19 11 13 18 rpgecld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ+ )
20 19 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ )
21 6 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
22 20 21 rpdivcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
23 22 relogcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
24 9 23 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
25 4 24 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
26 11 17 rplogcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
27 25 26 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ∈ ℝ )
28 27 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ∈ ℂ )
29 19 relogcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
30 29 rehalfcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) / 2 ) ∈ ℝ )
31 30 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) / 2 ) ∈ ℂ )
32 3 28 31 subdid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) = ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) − ( 2 · ( ( log ‘ 𝑥 ) / 2 ) ) ) )
33 29 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
34 2ne0 ⊢ 2 ≠ 0
35 34 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ≠ 0 )
36 33 3 35 divcan2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( ( log ‘ 𝑥 ) / 2 ) ) = ( log ‘ 𝑥 ) )
37 36 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) − ( 2 · ( ( log ‘ 𝑥 ) / 2 ) ) ) = ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) )
38 32 37 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) = ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) )
39 38 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 2 · ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) )
40 2re ⊢ 2 ∈ ℝ
41 40 a1i ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℝ )
42 27 30 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ∈ ℝ )
43 ioossre ⊢ ( 1 (,) +∞ ) ⊆ ℝ
44 2cn ⊢ 2 ∈ ℂ
45 o1const ⊢ ( ( ( 1 (,) +∞ ) ⊆ ℝ ∧ 2 ∈ ℂ ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 2 ) ∈ 𝑂(1) )
46 43 44 45 mp2an ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 2 ) ∈ 𝑂(1)
47 46 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 2 ) ∈ 𝑂(1) )
48 vmalogdivsum2 ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1)
49 48 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1) )
50 41 42 47 49 o1mul2 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 2 · ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ) ∈ 𝑂(1) )
51 39 50 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
52 fzfid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ Fin )
53 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) → 𝑚 ∈ ℕ )
54 53 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℕ )
55 vmacl ⊢ ( 𝑚 ∈ ℕ → ( Λ ‘ 𝑚 ) ∈ ℝ )
56 54 55 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ )
57 54 nnrpd ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℝ+ )
58 57 relogcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ )
59 11 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ )
60 59 6 nndivred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
61 60 adantr ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
62 61 54 nndivred ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( 𝑥 / 𝑛 ) / 𝑚 ) ∈ ℝ )
63 chpcl ⊢ ( ( ( 𝑥 / 𝑛 ) / 𝑚 ) ∈ ℝ → ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ∈ ℝ )
64 62 63 syl ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ∈ ℝ )
65 58 64 readdcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ∈ ℝ )
66 56 65 remulcld ⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ∈ ℝ )
67 52 66 fsumrecl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ∈ ℝ )
68 8 67 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ∈ ℝ )
69 4 68 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ∈ ℝ )
70 19 26 rpmulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℝ+ )
71 69 70 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
72 71 29 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ∈ ℝ )
73 72 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ∈ ℂ )
74 25 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
75 26 rpne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ≠ 0 )
76 74 33 75 divcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ∈ ℂ )
77 3 76 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) ∈ ℂ )
78 77 33 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ∈ ℂ )
79 71 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
80 79 77 33 nnncan2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) − ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) ) )
81 69 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ∈ ℂ )
82 11 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℂ )
83 19 rpne0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ≠ 0 )
84 81 82 33 83 75 divdiv1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) / ( log ‘ 𝑥 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
85 3 74 33 75 divassd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) = ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) )
86 84 85 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) / ( log ‘ 𝑥 ) ) − ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) ) )
87 69 19 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) ∈ ℝ )
88 87 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) ∈ ℂ )
89 3 74 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
90 88 89 33 75 divsubdird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) − ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( log ‘ 𝑥 ) ) = ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) / ( log ‘ 𝑥 ) ) − ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) )
91 83 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ≠ 0 )
92 68 59 91 redivcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) ∈ ℝ )
93 92 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) ∈ ℂ )
94 40 a1i ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 2 ∈ ℝ )
95 94 24 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
96 95 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
97 4 93 96 fsumsub ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) − ( 2 · ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 2 · ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) )
98 8 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
99 67 59 91 redivcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) ∈ ℝ )
100 99 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) ∈ ℂ )
101 2cnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 2 ∈ ℂ )
102 23 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
103 6 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ )
104 6 nnne0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≠ 0 )
105 102 103 104 divcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ∈ ℂ )
106 101 105 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ∈ ℂ )
107 98 100 106 subdid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) ) − ( ( Λ ‘ 𝑛 ) · ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) )
108 67 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ∈ ℂ )
109 82 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℂ )
110 98 108 109 91 divassd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) = ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) ) )
111 98 103 102 104 div32d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( Λ ‘ 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) )
112 111 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( 2 · ( ( Λ ‘ 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) )
113 101 98 105 mul12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( Λ ‘ 𝑛 ) · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) = ( ( Λ ‘ 𝑛 ) · ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) )
114 112 113 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( Λ ‘ 𝑛 ) · ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) )
115 110 114 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) − ( 2 · ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) ) − ( ( Λ ‘ 𝑛 ) · ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) )
116 107 115 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) = ( ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) − ( 2 · ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) )
117 116 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) − ( 2 · ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) )
118 68 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ∈ ℂ )
119 4 82 118 83 fsumdivc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) )
120 24 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
121 4 3 120 fsummulc2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 2 · ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
122 119 121 oveq12d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) − ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 2 · ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) )
123 97 117 122 3eqtr4rd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) − ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) )
124 123 oveq1d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) − ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( log ‘ 𝑥 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) )
125 90 124 eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / 𝑥 ) / ( log ‘ 𝑥 ) ) − ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) )
126 80 86 125 3eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) − ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) )
127 126 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) − ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) )
128 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
129 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐴 ∈ ℝ+ )
130 129 rpred ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐴 ∈ ℝ )
131 4 9 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
132 131 26 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ∈ ℝ )
133 1 rpcnd ⊢ ( 𝜑 → 𝐴 ∈ ℂ )
134 o1const ⊢ ( ( ( 1 (,) +∞ ) ⊆ ℝ ∧ 𝐴 ∈ ℂ ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 𝐴 ) ∈ 𝑂(1) )
135 43 133 134 sylancr ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 𝐴 ) ∈ 𝑂(1) )
136 1cnd ⊢ ( 𝜑 → 1 ∈ ℂ )
137 o1const ⊢ ( ( ( 1 (,) +∞ ) ⊆ ℝ ∧ 1 ∈ ℂ ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 1 ) ∈ 𝑂(1) )
138 43 136 137 sylancr ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 1 ) ∈ 𝑂(1) )
139 132 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ∈ ℂ )
140 1cnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℂ )
141 131 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
142 141 33 33 75 divsubdird ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / ( log ‘ 𝑥 ) ) ) )
143 141 33 subcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ∈ ℂ )
144 143 33 75 divrecd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) · ( 1 / ( log ‘ 𝑥 ) ) ) )
145 33 75 dividd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) / ( log ‘ 𝑥 ) ) = 1 )
146 145 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) − 1 ) )
147 142 144 146 3eqtr3d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) · ( 1 / ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) − 1 ) )
148 147 mpteq2dva ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) · ( 1 / ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) − 1 ) ) )
149 131 29 resubcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ∈ ℝ )
150 14 26 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 / ( log ‘ 𝑥 ) ) ∈ ℝ )
151 19 ex ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ+ ) )
152 151 ssrdv ⊢ ( 𝜑 → ( 1 (,) +∞ ) ⊆ ℝ+ )
153 vmadivsum ⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1)
154 153 a1i ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
155 152 154 o1res2 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
156 divlogrlim ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ⇝𝑟 0
157 rlimo1 ⊢ ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ⇝𝑟 0 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
158 156 157 mp1i ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
159 149 150 155 158 o1mul2 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) · ( 1 / ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
160 148 159 eqeltrrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) − 1 ) ) ∈ 𝑂(1) )
161 139 140 160 o1dif ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 1 ) ∈ 𝑂(1) ) )
162 138 161 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
163 130 132 135 162 o1mul2 ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
164 130 132 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ) ∈ ℝ )
165 23 6 nndivred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ∈ ℝ )
166 94 165 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ∈ ℝ )
167 99 166 resubcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ∈ ℝ )
168 8 167 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ∈ ℝ )
169 4 168 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ∈ ℝ )
170 169 26 rerpdivcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ∈ ℝ )
171 170 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ∈ ℂ )
172 169 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ∈ ℂ )
173 172 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) ∈ ℝ )
174 130 131 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ )
175 100 106 subcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ∈ ℂ )
176 98 175 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ∈ ℂ )
177 176 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) ∈ ℝ )
178 4 177 fsumrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) ∈ ℝ )
179 168 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ∈ ℂ )
180 4 179 fsumabs ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) )
181 130 adantr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐴 ∈ ℝ )
182 181 9 remulcld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐴 · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℝ )
183 175 abscld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ∈ ℝ )
184 181 6 nndivred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐴 / 𝑛 ) ∈ ℝ )
185 vmage0 ⊢ ( 𝑛 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑛 ) )
186 6 185 syl ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) )
187 108 109 103 91 104 divdiv2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / ( 𝑥 / 𝑛 ) ) = ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) · 𝑛 ) / 𝑥 ) )
188 108 103 109 91 div23d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) · 𝑛 ) / 𝑥 ) = ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) · 𝑛 ) )
189 187 188 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / ( 𝑥 / 𝑛 ) ) = ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) · 𝑛 ) )
190 101 105 103 mulassd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) · 𝑛 ) = ( 2 · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) · 𝑛 ) ) )
191 102 103 104 divcan1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) · 𝑛 ) = ( log ‘ ( 𝑥 / 𝑛 ) ) )
192 191 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) · 𝑛 ) ) = ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) )
193 190 192 eqtr2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) · 𝑛 ) )
194 189 193 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / ( 𝑥 / 𝑛 ) ) − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) · 𝑛 ) − ( ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) · 𝑛 ) ) )
195 100 106 103 subdird ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) · 𝑛 ) = ( ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) · 𝑛 ) − ( ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) · 𝑛 ) ) )
196 194 195 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / ( 𝑥 / 𝑛 ) ) − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) · 𝑛 ) )
197 196 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / ( 𝑥 / 𝑛 ) ) − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( abs ‘ ( ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) · 𝑛 ) ) )
198 175 103 absmuld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) · 𝑛 ) ) = ( ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) · ( abs ‘ 𝑛 ) ) )
199 6 nnred ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ )
200 21 rpge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ 𝑛 )
201 199 200 absidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ 𝑛 ) = 𝑛 )
202 201 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) · ( abs ‘ 𝑛 ) ) = ( ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) · 𝑛 ) )
203 197 198 202 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / ( 𝑥 / 𝑛 ) ) − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) · 𝑛 ) )
204 fveq2 ⊢ ( 𝑖 = 𝑚 → ( Λ ‘ 𝑖 ) = ( Λ ‘ 𝑚 ) )
205 fveq2 ⊢ ( 𝑖 = 𝑚 → ( log ‘ 𝑖 ) = ( log ‘ 𝑚 ) )
206 oveq2 ⊢ ( 𝑖 = 𝑚 → ( 𝑦 / 𝑖 ) = ( 𝑦 / 𝑚 ) )
207 206 fveq2d ⊢ ( 𝑖 = 𝑚 → ( ψ ‘ ( 𝑦 / 𝑖 ) ) = ( ψ ‘ ( 𝑦 / 𝑚 ) ) )
208 205 207 oveq12d ⊢ ( 𝑖 = 𝑚 → ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) = ( ( log ‘ 𝑚 ) + ( ψ ‘ ( 𝑦 / 𝑚 ) ) ) )
209 204 208 oveq12d ⊢ ( 𝑖 = 𝑚 → ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) = ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( 𝑦 / 𝑚 ) ) ) ) )
210 209 cbvsumv ⊢ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( 𝑦 / 𝑚 ) ) ) )
211 fveq2 ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ⌊ ‘ 𝑦 ) = ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) )
212 211 oveq2d ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( 1 ... ( ⌊ ‘ 𝑦 ) ) = ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) )
213 fvoveq1 ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ψ ‘ ( 𝑦 / 𝑚 ) ) = ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) )
214 213 oveq2d ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ( log ‘ 𝑚 ) + ( ψ ‘ ( 𝑦 / 𝑚 ) ) ) = ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) )
215 214 oveq2d ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( 𝑦 / 𝑚 ) ) ) ) = ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) )
216 215 adantr ⊢ ( ( 𝑦 = ( 𝑥 / 𝑛 ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( 𝑦 / 𝑚 ) ) ) ) = ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) )
217 212 216 sumeq12dv ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( 𝑦 / 𝑚 ) ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) )
218 210 217 eqtrid ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) )
219 id ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → 𝑦 = ( 𝑥 / 𝑛 ) )
220 218 219 oveq12d ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / ( 𝑥 / 𝑛 ) ) )
221 fveq2 ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( log ‘ 𝑦 ) = ( log ‘ ( 𝑥 / 𝑛 ) ) )
222 221 oveq2d ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( 2 · ( log ‘ 𝑦 ) ) = ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) )
223 220 222 oveq12d ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) = ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / ( 𝑥 / 𝑛 ) ) − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
224 223 fveq2d ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( abs ‘ ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) = ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / ( 𝑥 / 𝑛 ) ) − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) )
225 224 breq1d ⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ( abs ‘ ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝐴 ↔ ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / ( 𝑥 / 𝑛 ) ) − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ≤ 𝐴 ) )
226 2 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝐴 )
227 103 mullidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · 𝑛 ) = 𝑛 )
228 fznnfl ⊢ ( 𝑥 ∈ ℝ → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥 ) ) )
229 11 228 syl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥 ) ) )
230 229 simplbda ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≤ 𝑥 )
231 227 230 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · 𝑛 ) ≤ 𝑥 )
232 1red ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
233 232 59 21 lemuldivd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 · 𝑛 ) ≤ 𝑥 ↔ 1 ≤ ( 𝑥 / 𝑛 ) ) )
234 231 233 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ≤ ( 𝑥 / 𝑛 ) )
235 1re ⊢ 1 ∈ ℝ
236 elicopnf ⊢ ( 1 ∈ ℝ → ( ( 𝑥 / 𝑛 ) ∈ ( 1 [,) +∞ ) ↔ ( ( 𝑥 / 𝑛 ) ∈ ℝ ∧ 1 ≤ ( 𝑥 / 𝑛 ) ) ) )
237 235 236 ax-mp ⊢ ( ( 𝑥 / 𝑛 ) ∈ ( 1 [,) +∞ ) ↔ ( ( 𝑥 / 𝑛 ) ∈ ℝ ∧ 1 ≤ ( 𝑥 / 𝑛 ) ) )
238 60 234 237 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ( 1 [,) +∞ ) )
239 225 226 238 rspcdva ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / ( 𝑥 / 𝑛 ) ) − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ≤ 𝐴 )
240 203 239 eqbrtrrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) · 𝑛 ) ≤ 𝐴 )
241 183 181 21 lemuldivd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) · 𝑛 ) ≤ 𝐴 ↔ ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ≤ ( 𝐴 / 𝑛 ) ) )
242 240 241 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ≤ ( 𝐴 / 𝑛 ) )
243 183 184 8 186 242 lemul2ad ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) ≤ ( ( Λ ‘ 𝑛 ) · ( 𝐴 / 𝑛 ) ) )
244 98 175 absmuld ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) = ( ( abs ‘ ( Λ ‘ 𝑛 ) ) · ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) )
245 8 186 absidd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Λ ‘ 𝑛 ) ) = ( Λ ‘ 𝑛 ) )
246 245 oveq1d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( Λ ‘ 𝑛 ) ) · ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) = ( ( Λ ‘ 𝑛 ) · ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) )
247 244 246 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) = ( ( Λ ‘ 𝑛 ) · ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) )
248 133 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐴 ∈ ℂ )
249 248 98 103 104 div12d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐴 · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( ( Λ ‘ 𝑛 ) · ( 𝐴 / 𝑛 ) ) )
250 243 247 249 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) ≤ ( 𝐴 · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
251 4 177 182 250 fsumle ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝐴 · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
252 133 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐴 ∈ ℂ )
253 9 recnd ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
254 4 252 253 fsummulc2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝐴 · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
255 251 254 breqtrrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) ≤ ( 𝐴 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
256 173 178 174 180 255 letrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) ≤ ( 𝐴 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
257 173 174 26 256 lediv1dd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) / ( log ‘ 𝑥 ) ) ≤ ( ( 𝐴 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) / ( log ‘ 𝑥 ) ) )
258 252 141 33 75 divassd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝐴 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) / ( log ‘ 𝑥 ) ) = ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ) )
259 257 258 breqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) / ( log ‘ 𝑥 ) ) ≤ ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ) )
260 172 33 75 absdivd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) = ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) / ( abs ‘ ( log ‘ 𝑥 ) ) ) )
261 26 rpge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( log ‘ 𝑥 ) )
262 29 261 absidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( log ‘ 𝑥 ) ) = ( log ‘ 𝑥 ) )
263 262 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) / ( abs ‘ ( log ‘ 𝑥 ) ) ) = ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) / ( log ‘ 𝑥 ) ) )
264 260 263 eqtrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) = ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) ) / ( log ‘ 𝑥 ) ) )
265 129 rpge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ 𝐴 )
266 8 21 186 divge0d ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
267 4 9 266 fsumge0 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
268 131 26 267 divge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) )
269 130 132 265 268 mulge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ) )
270 164 269 absidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ) ) = ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ) )
271 259 264 270 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ≤ ( abs ‘ ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ) ) )
272 271 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ≤ ( abs ‘ ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ) ) )
273 128 163 164 171 272 o1le ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( ( log ‘ ( 𝑥 / 𝑛 ) ) / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
274 127 273 eqeltrd ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) − ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
275 73 78 274 o1dif ⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) )
276 51 275 mpbird ⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )