Metamath Proof Explorer

Theorem vmadivsumb

Description: Give a total bound on the von Mangoldt sum. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Assertion vmadivsumb ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( 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 1rp ⊢ 1 ∈ ℝ+
6 5 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 1 ∈ ℝ+ )
7 3 simplbda ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 1 ≤ 𝑥 )
8 4 6 7 rpgecld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 𝑥 ∈ ℝ+ )
9 8 ex ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 [,) +∞ ) → 𝑥 ∈ ℝ+ ) )
10 9 ssrdv ⊢ ( ⊤ → ( 1 [,) +∞ ) ⊆ ℝ+ )
11 rpssre ⊢ ℝ+ ⊆ ℝ
12 10 11 sstrdi ⊢ ( ⊤ → ( 1 [,) +∞ ) ⊆ ℝ )
13 1 a1i ⊢ ( ⊤ → 1 ∈ ℝ )
14 fzfid ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
15 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
16 15 adantl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
17 vmacl ⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
18 16 17 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
19 18 16 nndivred ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
20 14 19 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
21 8 relogcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
22 20 21 resubcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ∈ ℝ )
23 22 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ∈ ℂ )
24 vmadivsum ⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1)
25 24 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
26 10 25 o1res2 ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
27 fzfid ⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( 1 ... ( ⌊ ‘ 𝑦 ) ) ∈ Fin )
28 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) → 𝑛 ∈ ℕ )
29 28 adantl ⊢ ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑛 ∈ ℕ )
30 29 17 syl ⊢ ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
31 30 29 nndivred ⊢ ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
32 27 31 fsumrecl ⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
33 simprl ⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → 𝑦 ∈ ℝ )
34 5 a1i ⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → 1 ∈ ℝ+ )
35 simprr ⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → 1 ≤ 𝑦 )
36 33 34 35 rpgecld ⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → 𝑦 ∈ ℝ+ )
37 36 relogcld ⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( log ‘ 𝑦 ) ∈ ℝ )
38 32 37 readdcld ⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) + ( log ‘ 𝑦 ) ) ∈ ℝ )
39 22 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ∈ ℝ )
40 39 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ∈ ℂ )
41 40 abscld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ ℝ )
42 20 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
43 8 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ∈ ℝ+ )
44 43 relogcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
45 42 44 readdcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) + ( log ‘ 𝑥 ) ) ∈ ℝ )
46 38 ad2ant2r ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) + ( log ‘ 𝑦 ) ) ∈ ℝ )
47 42 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
48 44 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
49 47 48 abs2dif2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ≤ ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + ( abs ‘ ( log ‘ 𝑥 ) ) ) )
50 16 nnrpd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
51 vmage0 ⊢ ( 𝑛 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑛 ) )
52 16 51 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) )
53 18 50 52 divge0d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
54 14 19 53 fsumge0 ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 0 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
55 54 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
56 42 55 absidd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
57 21 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
58 4 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ∈ ℝ )
59 7 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 1 ≤ 𝑥 )
60 58 59 logge0d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ ( log ‘ 𝑥 ) )
61 57 60 absidd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( log ‘ 𝑥 ) ) = ( log ‘ 𝑥 ) )
62 56 61 oveq12d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + ( abs ‘ ( log ‘ 𝑥 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) + ( log ‘ 𝑥 ) ) )
63 49 62 breqtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) + ( log ‘ 𝑥 ) ) )
64 32 ad2ant2r ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
65 36 ad2ant2r ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑦 ∈ ℝ+ )
66 65 relogcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( log ‘ 𝑦 ) ∈ ℝ )
67 fzfid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 1 ... ( ⌊ ‘ 𝑦 ) ) ∈ Fin )
68 28 adantl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑛 ∈ ℕ )
69 68 17 syl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
70 69 68 nndivred ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
71 68 nnrpd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑛 ∈ ℝ+ )
72 68 51 syl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) )
73 69 71 72 divge0d ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
74 simprll ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑦 ∈ ℝ )
75 simprr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 < 𝑦 )
76 58 74 75 ltled ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ≤ 𝑦 )
77 flword2 ⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ) → ( ⌊ ‘ 𝑦 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑥 ) ) )
78 58 74 76 77 syl3anc ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ⌊ ‘ 𝑦 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑥 ) ) )
79 fzss2 ⊢ ( ( ⌊ ‘ 𝑦 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑦 ) ) )
80 78 79 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑦 ) ) )
81 67 70 73 80 fsumless ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
82 74 43 76 rpgecld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑦 ∈ ℝ+ )
83 43 82 logled ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 𝑥 ≤ 𝑦 ↔ ( log ‘ 𝑥 ) ≤ ( log ‘ 𝑦 ) ) )
84 76 83 mpbid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( log ‘ 𝑥 ) ≤ ( log ‘ 𝑦 ) )
85 42 44 64 66 81 84 le2addd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) + ( log ‘ 𝑥 ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) + ( log ‘ 𝑦 ) ) )
86 41 45 46 63 85 letrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) + ( log ‘ 𝑦 ) ) )
87 12 13 23 26 38 86 o1bddrp ⊢ ( ⊤ → ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ≤ 𝑐 )
88 87 mptru ⊢ ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ≤ 𝑐