| Step | Hyp | Ref
| Expression |
| 1 | | 1red 11262 |
. . 3
⊢ (⊤
→ 1 ∈ ℝ) |
| 2 | | pntrlog2bnd.r |
. . . . 5
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
| 3 | 2 | selberg34r 27615 |
. . . 4
⊢ (𝑥 ∈ (1(,)+∞) ↦
((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ 𝑂(1) |
| 4 | | elioore 13417 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1(,)+∞) →
𝑥 ∈
ℝ) |
| 5 | 4 | adantl 481 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ) |
| 6 | | 1rp 13038 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ+ |
| 7 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ+) |
| 8 | | 1red 11262 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ) |
| 9 | | eliooord 13446 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1(,)+∞) → (1
< 𝑥 ∧ 𝑥 <
+∞)) |
| 10 | 9 | adantl 481 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞)) |
| 11 | 10 | simpld 494 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 < 𝑥) |
| 12 | 8, 5, 11 | ltled 11409 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ≤ 𝑥) |
| 13 | 5, 7, 12 | rpgecld 13116 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ+) |
| 14 | 2 | pntrf 27607 |
. . . . . . . . . . 11
⊢ 𝑅:ℝ+⟶ℝ |
| 15 | 14 | ffvelcdmi 7103 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) ∈
ℝ) |
| 16 | 13, 15 | syl 17 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℝ) |
| 17 | 13 | relogcld 26665 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ) |
| 18 | 16, 17 | remulcld 11291 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑅‘𝑥) · (log‘𝑥)) ∈ ℝ) |
| 19 | | fzfid 14014 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin) |
| 20 | 13 | adantr 480 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+) |
| 21 | | elfznn 13593 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
| 22 | 21 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
| 23 | 22 | nnrpd 13075 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+) |
| 24 | 20, 23 | rpdivcld 13094 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈
ℝ+) |
| 25 | 14 | ffvelcdmi 7103 |
. . . . . . . . . . . 12
⊢ ((𝑥 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) |
| 26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) |
| 27 | | fzfid 14014 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...𝑛) ∈ Fin) |
| 28 | | dvdsssfz1 16355 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ⊆ (1...𝑛)) |
| 29 | 22, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ⊆ (1...𝑛)) |
| 30 | 27, 29 | ssfid 9301 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ∈ Fin) |
| 31 | | ssrab2 4080 |
. . . . . . . . . . . . . . . 16
⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ⊆ ℕ |
| 32 | | simpr 484 |
. . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
| 33 | 31, 32 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 𝑚 ∈ ℕ) |
| 34 | | vmacl 27161 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ →
(Λ‘𝑚) ∈
ℝ) |
| 35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (Λ‘𝑚) ∈ ℝ) |
| 36 | | dvdsdivcl 16353 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
| 37 | 22, 36 | sylan 580 |
. . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
| 38 | 31, 37 | sselid 3981 |
. . . . . . . . . . . . . . 15
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑚) ∈ ℕ) |
| 39 | | vmacl 27161 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 / 𝑚) ∈ ℕ →
(Λ‘(𝑛 / 𝑚)) ∈
ℝ) |
| 40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (Λ‘(𝑛 / 𝑚)) ∈ ℝ) |
| 41 | 35, 40 | remulcld 11291 |
. . . . . . . . . . . . 13
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℝ) |
| 42 | 30, 41 | fsumrecl 15770 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℝ) |
| 43 | | vmacl 27161 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
| 44 | 22, 43 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℝ) |
| 45 | 23 | relogcld 26665 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈
ℝ) |
| 46 | 44, 45 | remulcld 11291 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛)
· (log‘𝑛))
∈ ℝ) |
| 47 | 42, 46 | resubcld 11691 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))) ∈
ℝ) |
| 48 | 26, 47 | remulcld 11291 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈
ℝ) |
| 49 | 19, 48 | fsumrecl 15770 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈
ℝ) |
| 50 | 5, 11 | rplogcld 26671 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈
ℝ+) |
| 51 | 49, 50 | rerpdivcld 13108 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)) ∈
ℝ) |
| 52 | 18, 51 | resubcld 11691 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) ∈
ℝ) |
| 53 | 52, 13 | rerpdivcld 13108 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥) ∈ ℝ) |
| 54 | 53 | recnd 11289 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥) ∈ ℂ) |
| 55 | 54 | lo1o12 15569 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈
(1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
(abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥))) ∈
≤𝑂(1))) |
| 56 | 3, 55 | mpbii 233 |
. . 3
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥))) ∈ ≤𝑂(1)) |
| 57 | 54 | abscld 15475 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ ℝ) |
| 58 | 16 | recnd 11289 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℂ) |
| 59 | 58 | abscld 15475 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘𝑥)) ∈ ℝ) |
| 60 | 59, 17 | remulcld 11291 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈ ℝ) |
| 61 | 26 | recnd 11289 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℂ) |
| 62 | 61 | abscld 15475 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ) |
| 63 | 22 | nnred 12281 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ) |
| 64 | | pntsval.1 |
. . . . . . . . . . . 12
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) |
| 65 | 64 | pntsf 27617 |
. . . . . . . . . . 11
⊢ 𝑆:ℝ⟶ℝ |
| 66 | 65 | ffvelcdmi 7103 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ → (𝑆‘𝑛) ∈ ℝ) |
| 67 | 63, 66 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) ∈ ℝ) |
| 68 | | 1red 11262 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℝ) |
| 69 | 63, 68 | resubcld 11691 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ) |
| 70 | 65 | ffvelcdmi 7103 |
. . . . . . . . . 10
⊢ ((𝑛 − 1) ∈ ℝ
→ (𝑆‘(𝑛 − 1)) ∈
ℝ) |
| 71 | 69, 70 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℝ) |
| 72 | 67, 71 | resubcld 11691 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) ∈
ℝ) |
| 73 | 62, 72 | remulcld 11291 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℝ) |
| 74 | 19, 73 | fsumrecl 15770 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℝ) |
| 75 | 74, 50 | rerpdivcld 13108 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈
ℝ) |
| 76 | 60, 75 | resubcld 11691 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈
ℝ) |
| 77 | 76, 13 | rerpdivcld 13108 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ∈ ℝ) |
| 78 | 17 | recnd 11289 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ) |
| 79 | 58, 78 | mulcld 11281 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑅‘𝑥) · (log‘𝑥)) ∈ ℂ) |
| 80 | 49 | recnd 11289 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈
ℂ) |
| 81 | 50 | rpne0d 13082 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ≠ 0) |
| 82 | 80, 78, 81 | divcld 12043 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)) ∈
ℂ) |
| 83 | 79, 82 | subcld 11620 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) ∈
ℂ) |
| 84 | 83 | abscld 15475 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) ∈
ℝ) |
| 85 | 80 | abscld 15475 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ∈
ℝ) |
| 86 | 85, 50 | rerpdivcld 13108 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥)) ∈
ℝ) |
| 87 | 60, 86 | resubcld 11691 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥))) ∈
ℝ) |
| 88 | 48 | recnd 11289 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈
ℂ) |
| 89 | 88 | abscld 15475 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ∈
ℝ) |
| 90 | 19, 89 | fsumrecl 15770 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ∈
ℝ) |
| 91 | 19, 88 | fsumabs 15837 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ≤ Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) |
| 92 | 47 | recnd 11289 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))) ∈
ℂ) |
| 93 | 61, 92 | absmuld 15493 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (abs‘(Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) |
| 94 | 92 | abscld 15475 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚))) −
((Λ‘𝑛)
· (log‘𝑛))))
∈ ℝ) |
| 95 | 61 | absge0d 15483 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(abs‘(𝑅‘(𝑥 / 𝑛)))) |
| 96 | 42 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℂ) |
| 97 | 46 | recnd 11289 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛)
· (log‘𝑛))
∈ ℂ) |
| 98 | 96, 97 | abs2dif2d 15497 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚))) −
((Λ‘𝑛)
· (log‘𝑛))))
≤ ((abs‘Σ𝑚
∈ {𝑦 ∈ ℕ
∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚)))) +
(abs‘((Λ‘𝑛) · (log‘𝑛))))) |
| 99 | 71 | recnd 11289 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℂ) |
| 100 | 96, 97 | addcld 11280 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛))) ∈ ℂ) |
| 101 | 99, 100 | pncan2d 11622 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘(𝑛 − 1)) + (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛)))) − (𝑆‘(𝑛 − 1))) = (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛)))) |
| 102 | | elfzuz 13560 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
(ℤ≥‘1)) |
| 103 | 102 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈
(ℤ≥‘1)) |
| 104 | | elfznn 13593 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
| 105 | 104 | adantl 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
| 106 | | vmacl 27161 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℕ →
(Λ‘𝑘) ∈
ℝ) |
| 107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → (Λ‘𝑘) ∈ ℝ) |
| 108 | 105 | nnrpd 13075 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℝ+) |
| 109 | 108 | relogcld 26665 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℝ) |
| 110 | 107, 109 | remulcld 11291 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → ((Λ‘𝑘) · (log‘𝑘)) ∈ ℝ) |
| 111 | | fzfid 14014 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → (1...𝑘) ∈ Fin) |
| 112 | | dvdsssfz1 16355 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ ℕ → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ (1...𝑘)) |
| 113 | 105, 112 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ (1...𝑘)) |
| 114 | 111, 113 | ssfid 9301 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ∈ Fin) |
| 115 | | ssrab2 4080 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ |
| 116 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) |
| 117 | 115, 116 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → 𝑚 ∈ ℕ) |
| 118 | 117, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (Λ‘𝑚) ∈ ℝ) |
| 119 | | dvdsdivcl 16353 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (𝑘 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) |
| 120 | 105, 119 | sylan 580 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (𝑘 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) |
| 121 | 115, 120 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (𝑘 / 𝑚) ∈ ℕ) |
| 122 | | vmacl 27161 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 / 𝑚) ∈ ℕ →
(Λ‘(𝑘 / 𝑚)) ∈
ℝ) |
| 123 | 121, 122 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (Λ‘(𝑘 / 𝑚)) ∈ ℝ) |
| 124 | 118, 123 | remulcld 11291 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))) ∈ ℝ) |
| 125 | 114, 124 | fsumrecl 15770 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))) ∈ ℝ) |
| 126 | 110, 125 | readdcld 11290 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → (((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) ∈ ℝ) |
| 127 | 126 | recnd 11289 |
. . . . . . . . . . . . . . . . . 18
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → (((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) ∈ ℂ) |
| 128 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑛 → (Λ‘𝑘) = (Λ‘𝑛)) |
| 129 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑛 → (log‘𝑘) = (log‘𝑛)) |
| 130 | 128, 129 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑛 → ((Λ‘𝑘) · (log‘𝑘)) = ((Λ‘𝑛) · (log‘𝑛))) |
| 131 | | breq2 5147 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑛 → (𝑦 ∥ 𝑘 ↔ 𝑦 ∥ 𝑛)) |
| 132 | 131 | rabbidv 3444 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑛 → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} = {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
| 133 | | fvoveq1 7454 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑛 → (Λ‘(𝑘 / 𝑚)) = (Λ‘(𝑛 / 𝑚))) |
| 134 | 133 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑛 → ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))) = ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
| 135 | 134 | adantr 480 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 = 𝑛 ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))) = ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
| 136 | 132, 135 | sumeq12rdv 15743 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑛 → Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))) = Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
| 137 | 130, 136 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑛 → (((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) = (((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
| 138 | 103, 127,
137 | fsumm1 15787 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑘 ∈ (1...𝑛)(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) = (Σ𝑘 ∈ (1...(𝑛 − 1))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) + (((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))) |
| 139 | 64 | pntsval2 27620 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℝ → (𝑆‘𝑛) = Σ𝑘 ∈ (1...(⌊‘𝑛))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
| 140 | 63, 139 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) = Σ𝑘 ∈ (1...(⌊‘𝑛))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
| 141 | 22 | nnzd 12640 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℤ) |
| 142 | | flid 13848 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℤ →
(⌊‘𝑛) = 𝑛) |
| 143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘𝑛) = 𝑛) |
| 144 | 143 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(1...(⌊‘𝑛)) =
(1...𝑛)) |
| 145 | 144 | sumeq1d 15736 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑘 ∈
(1...(⌊‘𝑛))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) = Σ𝑘 ∈ (1...𝑛)(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
| 146 | 140, 145 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) = Σ𝑘 ∈ (1...𝑛)(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
| 147 | 64 | pntsval2 27620 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 − 1) ∈ ℝ
→ (𝑆‘(𝑛 − 1)) = Σ𝑘 ∈
(1...(⌊‘(𝑛
− 1)))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
| 148 | 69, 147 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) = Σ𝑘 ∈ (1...(⌊‘(𝑛 −
1)))(((Λ‘𝑘)
· (log‘𝑘)) +
Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
| 149 | | 1zzd 12648 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℤ) |
| 150 | 141, 149 | zsubcld 12727 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℤ) |
| 151 | | flid 13848 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 − 1) ∈ ℤ
→ (⌊‘(𝑛
− 1)) = (𝑛 −
1)) |
| 152 | 150, 151 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑛 − 1)) = (𝑛 − 1)) |
| 153 | 152 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(1...(⌊‘(𝑛
− 1))) = (1...(𝑛
− 1))) |
| 154 | 153 | sumeq1d 15736 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑘 ∈
(1...(⌊‘(𝑛
− 1)))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) = Σ𝑘 ∈ (1...(𝑛 − 1))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
| 155 | 148, 154 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) = Σ𝑘 ∈ (1...(𝑛 − 1))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
| 156 | 96, 97 | addcomd 11463 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛))) = (((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
| 157 | 155, 156 | oveq12d 7449 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘(𝑛 − 1)) + (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛)))) = (Σ𝑘 ∈ (1...(𝑛 − 1))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) + (((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))) |
| 158 | 138, 146,
157 | 3eqtr4d 2787 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) = ((𝑆‘(𝑛 − 1)) + (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛))))) |
| 159 | 158 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) = (((𝑆‘(𝑛 − 1)) + (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛)))) − (𝑆‘(𝑛 − 1)))) |
| 160 | | vmage0 27164 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℕ → 0 ≤
(Λ‘𝑚)) |
| 161 | 33, 160 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 0 ≤ (Λ‘𝑚)) |
| 162 | | vmage0 27164 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 / 𝑚) ∈ ℕ → 0 ≤
(Λ‘(𝑛 / 𝑚))) |
| 163 | 38, 162 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 0 ≤ (Λ‘(𝑛 / 𝑚))) |
| 164 | 35, 40, 161, 163 | mulge0d 11840 |
. . . . . . . . . . . . . . . . . 18
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 0 ≤ ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚)))) |
| 165 | 30, 41, 164 | fsumge0 15831 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
| 166 | 42, 165 | absidd 15461 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚)))) = Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
| 167 | | vmage0 27164 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → 0 ≤
(Λ‘𝑛)) |
| 168 | 22, 167 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(Λ‘𝑛)) |
| 169 | 22 | nnge1d 12314 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ 𝑛) |
| 170 | 63, 169 | logge0d 26672 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(log‘𝑛)) |
| 171 | 44, 45, 168, 170 | mulge0d 11840 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
((Λ‘𝑛)
· (log‘𝑛))) |
| 172 | 46, 171 | absidd 15461 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((Λ‘𝑛) · (log‘𝑛))) = ((Λ‘𝑛) · (log‘𝑛))) |
| 173 | 166, 172 | oveq12d 7449 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((abs‘Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚)))) +
(abs‘((Λ‘𝑛) · (log‘𝑛)))) = (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛)))) |
| 174 | 101, 159,
173 | 3eqtr4d 2787 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) = ((abs‘Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) + (abs‘((Λ‘𝑛) · (log‘𝑛))))) |
| 175 | 98, 174 | breqtrrd 5171 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚))) −
((Λ‘𝑛)
· (log‘𝑛))))
≤ ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) |
| 176 | 94, 72, 62, 95, 175 | lemul2ad 12208 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (abs‘(Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ≤ ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))))) |
| 177 | 93, 176 | eqbrtrd 5165 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ≤ ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))))) |
| 178 | 19, 89, 73, 177 | fsumle 15835 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ≤ Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))))) |
| 179 | 85, 90, 74, 91, 178 | letrd 11418 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ≤ Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))))) |
| 180 | 85, 74, 50, 179 | lediv1dd 13135 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥)) ≤ (Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) |
| 181 | 86, 75, 60, 180 | lesub2dd 11880 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ≤ (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥)))) |
| 182 | 58, 78 | absmuld 15493 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘((𝑅‘𝑥) · (log‘𝑥))) = ((abs‘(𝑅‘𝑥)) · (abs‘(log‘𝑥)))) |
| 183 | 5, 12 | logge0d 26672 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (log‘𝑥)) |
| 184 | 17, 183 | absidd 15461 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(log‘𝑥)) = (log‘𝑥)) |
| 185 | 184 | oveq2d 7447 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (abs‘(log‘𝑥))) = ((abs‘(𝑅‘𝑥)) · (log‘𝑥))) |
| 186 | 182, 185 | eqtrd 2777 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘((𝑅‘𝑥) · (log‘𝑥))) = ((abs‘(𝑅‘𝑥)) · (log‘𝑥))) |
| 187 | 80, 78, 81 | absdivd 15494 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) = ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) /
(abs‘(log‘𝑥)))) |
| 188 | 184 | oveq2d 7447 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) /
(abs‘(log‘𝑥)))
= ((abs‘Σ𝑛
∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥))) |
| 189 | 187, 188 | eqtrd 2777 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) = ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥))) |
| 190 | 186, 189 | oveq12d 7449 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘((𝑅‘𝑥) · (log‘𝑥))) − (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) = (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥)))) |
| 191 | 79, 82 | abs2difd 15496 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘((𝑅‘𝑥) · (log‘𝑥))) − (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) ≤ (abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))))) |
| 192 | 190, 191 | eqbrtrrd 5167 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥))) ≤ (abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))))) |
| 193 | 76, 87, 84, 181, 192 | letrd 11418 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ≤ (abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))))) |
| 194 | 76, 84, 13, 193 | lediv1dd 13135 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ≤ ((abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) / 𝑥)) |
| 195 | 52 | recnd 11289 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) ∈
ℂ) |
| 196 | 5 | recnd 11289 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℂ) |
| 197 | 13 | rpne0d 13082 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ≠ 0) |
| 198 | 195, 196,
197 | absdivd 15494 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) = ((abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) / (abs‘𝑥))) |
| 199 | 13 | rpge0d 13081 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ 𝑥) |
| 200 | 5, 199 | absidd 15461 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘𝑥) = 𝑥) |
| 201 | 200 | oveq2d 7447 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) / (abs‘𝑥)) = ((abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) / 𝑥)) |
| 202 | 198, 201 | eqtrd 2777 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) = ((abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) / 𝑥)) |
| 203 | 194, 202 | breqtrrd 5171 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ≤ (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥))) |
| 204 | 203 | adantrr 717 |
. . 3
⊢
((⊤ ∧ (𝑥
∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ≤ (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥))) |
| 205 | 1, 56, 57, 77, 204 | lo1le 15688 |
. 2
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1)) |
| 206 | 205 | mptru 1547 |
1
⊢ (𝑥 ∈ (1(,)+∞) ↦
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1) |