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)