Metamath Proof Explorer


Theorem selberg3lem2

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

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

Proof

Step Hyp Ref Expression
1 1re 1 ∈ ℝ
2 elicopnf ( 1 ∈ ℝ → ( 𝑦 ∈ ( 1 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) )
3 1 2 ax-mp ( 𝑦 ∈ ( 1 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) )
4 3 simplbi ( 𝑦 ∈ ( 1 [,) +∞ ) → 𝑦 ∈ ℝ )
5 4 ssriv ( 1 [,) +∞ ) ⊆ ℝ
6 5 a1i ( ⊤ → ( 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 12 14 remulcld ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ )
16 8 15 fsumrecl ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ )
17 4 adantl ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → 𝑦 ∈ ℝ )
18 chpcl ( 𝑦 ∈ ℝ → ( ψ ‘ 𝑦 ) ∈ ℝ )
19 17 18 syl ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → ( ψ ‘ 𝑦 ) ∈ ℝ )
20 1rp 1 ∈ ℝ+
21 20 a1i ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → 1 ∈ ℝ+ )
22 3 simprbi ( 𝑦 ∈ ( 1 [,) +∞ ) → 1 ≤ 𝑦 )
23 22 adantl ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → 1 ≤ 𝑦 )
24 17 21 23 rpgecld ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → 𝑦 ∈ ℝ+ )
25 24 relogcld ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → ( log ‘ 𝑦 ) ∈ ℝ )
26 19 25 remulcld ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ∈ ℝ )
27 16 26 resubcld ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ∈ ℝ )
28 27 24 rerpdivcld ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ∈ ℝ )
29 28 recnd ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ∈ ℂ )
30 24 ex ( ⊤ → ( 𝑦 ∈ ( 1 [,) +∞ ) → 𝑦 ∈ ℝ+ ) )
31 30 ssrdv ( ⊤ → ( 1 [,) +∞ ) ⊆ ℝ+ )
32 selberg2lem ( 𝑦 ∈ ℝ+ ↦ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ∈ 𝑂(1)
33 32 a1i ( ⊤ → ( 𝑦 ∈ ℝ+ ↦ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ∈ 𝑂(1) )
34 31 33 o1res2 ( ⊤ → ( 𝑦 ∈ ( 1 [,) +∞ ) ↦ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ∈ 𝑂(1) )
35 fzfid ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
36 elfznn ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑚 ∈ ℕ )
37 36 adantl ( ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℕ )
38 37 11 syl ( ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ )
39 37 nnrpd ( ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℝ+ )
40 39 relogcld ( ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ )
41 38 40 remulcld ( ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ )
42 35 41 fsumrecl ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ )
43 chpcl ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) ∈ ℝ )
44 43 ad2antrl ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) → ( ψ ‘ 𝑥 ) ∈ ℝ )
45 simprl ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
46 20 a1i ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) → 1 ∈ ℝ+ )
47 simprr ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) → 1 ≤ 𝑥 )
48 45 46 47 rpgecld ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ+ )
49 48 relogcld ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
50 44 49 remulcld ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) → ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ )
51 42 50 readdcld ( ( ⊤ ∧ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
52 27 adantr ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ∈ ℝ )
53 52 recnd ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ∈ ℂ )
54 24 adantr ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → 𝑦 ∈ ℝ+ )
55 54 rpcnd ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → 𝑦 ∈ ℂ )
56 54 rpne0d ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → 𝑦 ≠ 0 )
57 53 55 56 absdivd ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) = ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) / ( abs ‘ 𝑦 ) ) )
58 17 adantr ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → 𝑦 ∈ ℝ )
59 54 rpge0d ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → 0 ≤ 𝑦 )
60 58 59 absidd ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( abs ‘ 𝑦 ) = 𝑦 )
61 60 oveq2d ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) / ( abs ‘ 𝑦 ) ) = ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) / 𝑦 ) )
62 57 61 eqtrd ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) = ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) / 𝑦 ) )
63 53 abscld ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) ∈ ℝ )
64 63 54 rerpdivcld ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) / 𝑦 ) ∈ ℝ )
65 42 ad2ant2r ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ )
66 simprll ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → 𝑥 ∈ ℝ )
67 66 43 syl ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( ψ ‘ 𝑥 ) ∈ ℝ )
68 simprr ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → 𝑦 < 𝑥 )
69 58 66 68 ltled ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → 𝑦𝑥 )
70 66 54 69 rpgecld ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → 𝑥 ∈ ℝ+ )
71 70 relogcld ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
72 67 71 remulcld ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ )
73 65 72 readdcld ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
74 20 a1i ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → 1 ∈ ℝ+ )
75 53 absge0d ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → 0 ≤ ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) )
76 23 adantr ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → 1 ≤ 𝑦 )
77 74 54 63 75 76 lediv2ad ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) / 𝑦 ) ≤ ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) / 1 ) )
78 63 recnd ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) ∈ ℂ )
79 78 div1d ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) / 1 ) = ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) )
80 77 79 breqtrd ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) / 𝑦 ) ≤ ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) )
81 16 adantr ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ )
82 58 18 syl ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( ψ ‘ 𝑦 ) ∈ ℝ )
83 54 relogcld ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( log ‘ 𝑦 ) ∈ ℝ )
84 82 83 remulcld ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ∈ ℝ )
85 81 84 readdcld ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ∈ ℝ )
86 81 recnd ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ )
87 26 adantr ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ∈ ℝ )
88 87 recnd ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ∈ ℂ )
89 86 88 abs2dif2d ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) ≤ ( ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( abs ‘ ( ( ψ ‘ 𝑦 ) · ( 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 12 14 91 94 mulge0d ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 0 ≤ ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) )
96 8 15 95 fsumge0 ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) → 0 ≤ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) )
97 96 adantr ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → 0 ≤ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) )
98 81 97 absidd ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) )
99 chpge0 ( 𝑦 ∈ ℝ → 0 ≤ ( ψ ‘ 𝑦 ) )
100 58 99 syl ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → 0 ≤ ( ψ ‘ 𝑦 ) )
101 58 76 logge0d ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → 0 ≤ ( log ‘ 𝑦 ) )
102 82 83 100 101 mulge0d ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → 0 ≤ ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) )
103 87 102 absidd ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( abs ‘ ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) = ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) )
104 98 103 oveq12d ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( ( abs ‘ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( abs ‘ ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) )
105 89 104 breqtrd ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) )
106 fzfid ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
107 36 adantl ( ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℕ )
108 107 11 syl ( ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ )
109 107 nnrpd ( ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℝ+ )
110 109 relogcld ( ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ )
111 108 110 remulcld ( ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ )
112 107 90 syl ( ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( Λ ‘ 𝑚 ) )
113 107 nnred ( ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℝ )
114 107 nnge1d ( ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ≤ 𝑚 )
115 113 114 logge0d ( ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( log ‘ 𝑚 ) )
116 108 110 112 115 mulge0d ( ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) )
117 flword2 ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑦𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ( ℤ ‘ ( ⌊ ‘ 𝑦 ) ) )
118 58 66 69 117 syl3anc ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( ⌊ ‘ 𝑥 ) ∈ ( ℤ ‘ ( ⌊ ‘ 𝑦 ) ) )
119 fzss2 ( ( ⌊ ‘ 𝑥 ) ∈ ( ℤ ‘ ( ⌊ ‘ 𝑦 ) ) → ( 1 ... ( ⌊ ‘ 𝑦 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
120 118 119 syl ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑦 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
121 106 111 116 120 fsumless ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ≤ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) )
122 chpwordi ( ( 𝑦 ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ 𝑦𝑥 ) → ( ψ ‘ 𝑦 ) ≤ ( ψ ‘ 𝑥 ) )
123 58 66 69 122 syl3anc ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( ψ ‘ 𝑦 ) ≤ ( ψ ‘ 𝑥 ) )
124 54 70 logled ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( 𝑦𝑥 ↔ ( log ‘ 𝑦 ) ≤ ( log ‘ 𝑥 ) ) )
125 69 124 mpbid ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( log ‘ 𝑦 ) ≤ ( log ‘ 𝑥 ) )
126 82 67 83 71 100 101 123 125 lemul12ad ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ≤ ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) )
127 81 84 65 72 121 126 le2addd ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
128 63 85 73 105 127 letrd ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
129 64 63 73 80 128 letrd ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) ) / 𝑦 ) ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
130 62 129 eqbrtrd ( ( ( ⊤ ∧ 𝑦 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ∧ 𝑦 < 𝑥 ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) )
131 6 7 29 34 51 130 o1bddrp ( ⊤ → ∃ 𝑐 ∈ ℝ+𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ≤ 𝑐 )
132 131 mptru 𝑐 ∈ ℝ+𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ≤ 𝑐
133 simpl ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ≤ 𝑐 ) → 𝑐 ∈ ℝ+ )
134 simpr ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ≤ 𝑐 ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ≤ 𝑐 )
135 133 134 selberg3lem1 ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ≤ 𝑐 ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) )
136 135 rexlimiva ( ∃ 𝑐 ∈ ℝ+𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ≤ 𝑐 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) )
137 132 136 ax-mp ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1)