Metamath Proof Explorer


Theorem selbergb

Description: Convert eventual boundedness in selberg to boundedness on [ 1 , +oo ) . (We have to bound away from zero because the log terms diverge at zero.) (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Assertion selbergb 𝑐 ∈ ℝ+𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ 𝑐

Proof

Step Hyp Ref Expression
1 1re 1 ∈ ℝ
2 elicopnf ( 1 ∈ ℝ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) )
3 1 2 mp1i ( ⊤ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) )
4 3 simprbda ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 𝑥 ∈ ℝ )
5 4 ex ( ⊤ → ( 𝑥 ∈ ( 1 [,) +∞ ) → 𝑥 ∈ ℝ ) )
6 5 ssrdv ( ⊤ → ( 1 [,) +∞ ) ⊆ ℝ )
7 1 a1i ( ⊤ → 1 ∈ ℝ )
8 fzfid ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
9 elfznn ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
10 9 adantl ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
11 vmacl ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
12 10 11 syl ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
13 10 nnrpd ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
14 13 relogcld ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
15 4 adantr ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ )
16 15 10 nndivred ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
17 chpcl ( ( 𝑥 / 𝑛 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
18 16 17 syl ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
19 14 18 readdcld ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
20 12 19 remulcld ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
21 8 20 fsumrecl ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
22 1rp 1 ∈ ℝ+
23 22 a1i ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 1 ∈ ℝ+ )
24 3 simplbda ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 1 ≤ 𝑥 )
25 4 23 24 rpgecld ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 𝑥 ∈ ℝ+ )
26 21 25 rerpdivcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ∈ ℝ )
27 2re 2 ∈ ℝ
28 27 a1i ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 2 ∈ ℝ )
29 25 relogcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
30 28 29 remulcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℝ )
31 26 30 resubcld ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
32 31 recnd ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
33 25 ex ( ⊤ → ( 𝑥 ∈ ( 1 [,) +∞ ) → 𝑥 ∈ ℝ+ ) )
34 33 ssrdv ( ⊤ → ( 1 [,) +∞ ) ⊆ ℝ+ )
35 selberg ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)
36 35 a1i ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
37 34 36 o1res2 ( ⊤ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
38 fzfid ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( 1 ... ( ⌊ ‘ 𝑦 ) ) ∈ Fin )
39 elfznn ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) → 𝑛 ∈ ℕ )
40 39 adantl ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑛 ∈ ℕ )
41 40 11 syl ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
42 40 nnrpd ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑛 ∈ ℝ+ )
43 42 relogcld ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
44 simprl ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → 𝑦 ∈ ℝ )
45 44 adantr ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑦 ∈ ℝ )
46 45 40 nndivred ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( 𝑦 / 𝑛 ) ∈ ℝ )
47 chpcl ( ( 𝑦 / 𝑛 ) ∈ ℝ → ( ψ ‘ ( 𝑦 / 𝑛 ) ) ∈ ℝ )
48 46 47 syl ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ψ ‘ ( 𝑦 / 𝑛 ) ) ∈ ℝ )
49 43 48 readdcld ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ∈ ℝ )
50 41 49 remulcld ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) ∈ ℝ )
51 38 50 fsumrecl ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) ∈ ℝ )
52 27 a1i ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → 2 ∈ ℝ )
53 22 a1i ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → 1 ∈ ℝ+ )
54 simprr ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → 1 ≤ 𝑦 )
55 44 53 54 rpgecld ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → 𝑦 ∈ ℝ+ )
56 55 relogcld ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( log ‘ 𝑦 ) ∈ ℝ )
57 52 56 remulcld ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( 2 · ( log ‘ 𝑦 ) ) ∈ ℝ )
58 51 57 readdcld ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) + ( 2 · ( log ‘ 𝑦 ) ) ) ∈ ℝ )
59 31 adantr ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
60 59 recnd ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
61 60 abscld ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ ℝ )
62 26 adantr ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ∈ ℝ )
63 30 adantr ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℝ )
64 62 63 readdcld ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) + ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
65 fzfid ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 1 ... ( ⌊ ‘ 𝑦 ) ) ∈ Fin )
66 39 adantl ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑛 ∈ ℕ )
67 66 11 syl ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
68 66 nnrpd ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑛 ∈ ℝ+ )
69 68 relogcld ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
70 simprll ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑦 ∈ ℝ )
71 70 adantr ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑦 ∈ ℝ )
72 71 66 nndivred ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( 𝑦 / 𝑛 ) ∈ ℝ )
73 72 47 syl ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ψ ‘ ( 𝑦 / 𝑛 ) ) ∈ ℝ )
74 69 73 readdcld ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ∈ ℝ )
75 67 74 remulcld ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) ∈ ℝ )
76 65 75 fsumrecl ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) ∈ ℝ )
77 27 a1i ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 2 ∈ ℝ )
78 25 adantr ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ∈ ℝ+ )
79 4 adantr ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ∈ ℝ )
80 simprr ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 < 𝑦 )
81 79 70 80 ltled ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥𝑦 )
82 70 78 81 rpgecld ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑦 ∈ ℝ+ )
83 82 relogcld ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( log ‘ 𝑦 ) ∈ ℝ )
84 77 83 remulcld ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 2 · ( log ‘ 𝑦 ) ) ∈ ℝ )
85 76 84 readdcld ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) + ( 2 · ( log ‘ 𝑦 ) ) ) ∈ ℝ )
86 62 recnd ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ∈ ℂ )
87 63 recnd ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℂ )
88 86 87 abs2dif2d ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ ( ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) + ( abs ‘ ( 2 · ( log ‘ 𝑥 ) ) ) ) )
89 21 adantr ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
90 vmage0 ( 𝑛 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑛 ) )
91 10 90 syl ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) )
92 10 nnred ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ )
93 10 nnge1d ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ≤ 𝑛 )
94 92 93 logge0d ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( log ‘ 𝑛 ) )
95 chpge0 ( ( 𝑥 / 𝑛 ) ∈ ℝ → 0 ≤ ( ψ ‘ ( 𝑥 / 𝑛 ) ) )
96 16 95 syl ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ψ ‘ ( 𝑥 / 𝑛 ) ) )
97 14 18 94 96 addge0d ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) )
98 12 19 91 97 mulge0d ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
99 8 20 98 fsumge0 ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 0 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
100 99 adantr ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
101 89 78 100 divge0d ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) )
102 62 101 absidd ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) )
103 78 relogcld ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
104 2rp 2 ∈ ℝ+
105 rpge0 ( 2 ∈ ℝ+ → 0 ≤ 2 )
106 104 105 mp1i ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ 2 )
107 24 adantr ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 1 ≤ 𝑥 )
108 79 107 logge0d ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ ( log ‘ 𝑥 ) )
109 77 103 106 108 mulge0d ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ ( 2 · ( log ‘ 𝑥 ) ) )
110 63 109 absidd ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( 2 · ( log ‘ 𝑥 ) ) ) = ( 2 · ( log ‘ 𝑥 ) ) )
111 102 110 oveq12d ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) + ( abs ‘ ( 2 · ( log ‘ 𝑥 ) ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) + ( 2 · ( log ‘ 𝑥 ) ) ) )
112 88 111 breqtrd ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) + ( 2 · ( log ‘ 𝑥 ) ) ) )
113 22 a1i ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 1 ∈ ℝ+ )
114 79 adantr ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑥 ∈ ℝ )
115 114 66 nndivred ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
116 115 17 syl ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
117 69 116 readdcld ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
118 67 117 remulcld ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
119 65 118 fsumrecl ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
120 66 90 syl ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) )
121 66 nnred ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑛 ∈ ℝ )
122 66 nnge1d ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 1 ≤ 𝑛 )
123 121 122 logge0d ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 0 ≤ ( log ‘ 𝑛 ) )
124 115 95 syl ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 0 ≤ ( ψ ‘ ( 𝑥 / 𝑛 ) ) )
125 69 116 123 124 addge0d ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 0 ≤ ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) )
126 67 117 120 125 mulge0d ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
127 flword2 ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥𝑦 ) → ( ⌊ ‘ 𝑦 ) ∈ ( ℤ ‘ ( ⌊ ‘ 𝑥 ) ) )
128 79 70 81 127 syl3anc ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ⌊ ‘ 𝑦 ) ∈ ( ℤ ‘ ( ⌊ ‘ 𝑥 ) ) )
129 fzss2 ( ( ⌊ ‘ 𝑦 ) ∈ ( ℤ ‘ ( ⌊ ‘ 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑦 ) ) )
130 128 129 syl ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑦 ) ) )
131 65 118 126 130 fsumless ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) )
132 81 adantr ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑥𝑦 )
133 114 71 68 132 lediv1dd ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( 𝑥 / 𝑛 ) ≤ ( 𝑦 / 𝑛 ) )
134 chpwordi ( ( ( 𝑥 / 𝑛 ) ∈ ℝ ∧ ( 𝑦 / 𝑛 ) ∈ ℝ ∧ ( 𝑥 / 𝑛 ) ≤ ( 𝑦 / 𝑛 ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ≤ ( ψ ‘ ( 𝑦 / 𝑛 ) ) )
135 115 72 133 134 syl3anc ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ≤ ( ψ ‘ ( 𝑦 / 𝑛 ) ) )
136 116 73 69 135 leadd2dd ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ≤ ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) )
137 117 74 67 120 136 lemul2ad ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ≤ ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) )
138 65 118 75 137 fsumle ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) )
139 89 119 76 131 138 letrd ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) )
140 89 76 113 79 100 139 107 lediv12ad ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) / 1 ) )
141 76 recnd ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) ∈ ℂ )
142 141 div1d ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) / 1 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) )
143 140 142 breqtrd ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) )
144 78 82 logled ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 𝑥𝑦 ↔ ( log ‘ 𝑥 ) ≤ ( log ‘ 𝑦 ) ) )
145 81 144 mpbid ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( log ‘ 𝑥 ) ≤ ( log ‘ 𝑦 ) )
146 103 83 77 106 145 lemul2ad ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 2 · ( log ‘ 𝑥 ) ) ≤ ( 2 · ( log ‘ 𝑦 ) ) )
147 62 63 76 84 143 146 le2addd ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) + ( 2 · ( log ‘ 𝑥 ) ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) + ( 2 · ( log ‘ 𝑦 ) ) ) )
148 61 64 85 112 147 letrd ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) + ( 2 · ( log ‘ 𝑦 ) ) ) )
149 6 7 32 37 58 148 o1bddrp ( ⊤ → ∃ 𝑐 ∈ ℝ+𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ 𝑐 )
150 149 mptru 𝑐 ∈ ℝ+𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( log ‘ 𝑛 ) + ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ 𝑐