Proof of Theorem 2vmadivsumlem
| Step | Hyp | Ref
| Expression |
| 1 | | vmalogdivsum2 27582 |
. . 3
⊢ (𝑥 ∈ (1(,)+∞) ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1) |
| 2 | 1 | a1i 11 |
. 2
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈
𝑂(1)) |
| 3 | | fzfid 14014 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(1...(⌊‘𝑥))
∈ Fin) |
| 4 | | elfznn 13593 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
| 5 | 4 | adantl 481 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
| 6 | | vmacl 27161 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
| 7 | 5, 6 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
| 8 | 7, 5 | nndivred 12320 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℝ) |
| 9 | | fzfid 14014 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin) |
| 10 | | elfznn 13593 |
. . . . . . . . . . . 12
⊢ (𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛))) → 𝑚 ∈
ℕ) |
| 11 | 10 | adantl 481 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → 𝑚 ∈
ℕ) |
| 12 | | vmacl 27161 |
. . . . . . . . . . 11
⊢ (𝑚 ∈ ℕ →
(Λ‘𝑚) ∈
ℝ) |
| 13 | 11, 12 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
(Λ‘𝑚) ∈
ℝ) |
| 14 | 13, 11 | nndivred 12320 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
((Λ‘𝑚) / 𝑚) ∈
ℝ) |
| 15 | 9, 14 | fsumrecl 15770 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) / 𝑚) ∈ ℝ) |
| 16 | 8, 15 | remulcld 11291 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) / 𝑚)) ∈ ℝ) |
| 17 | 3, 16 | fsumrecl 15770 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) ∈ ℝ) |
| 18 | | elioore 13417 |
. . . . . . . 8
⊢ (𝑥 ∈ (1(,)+∞) →
𝑥 ∈
ℝ) |
| 19 | 18 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈
ℝ) |
| 20 | | eliooord 13446 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1(,)+∞) → (1
< 𝑥 ∧ 𝑥 <
+∞)) |
| 21 | 20 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞)) |
| 22 | 21 | simpld 494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥) |
| 23 | 19, 22 | rplogcld 26671 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ∈
ℝ+) |
| 24 | 17, 23 | rerpdivcld 13108 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) ∈ ℝ) |
| 25 | | 1rp 13038 |
. . . . . . . . 9
⊢ 1 ∈
ℝ+ |
| 26 | 25 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈
ℝ+) |
| 27 | | 1red 11262 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈
ℝ) |
| 28 | 27, 19, 22 | ltled 11409 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ≤ 𝑥) |
| 29 | 19, 26, 28 | rpgecld 13116 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈
ℝ+) |
| 30 | 29 | relogcld 26665 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ∈
ℝ) |
| 31 | 30 | rehalfcld 12513 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((log‘𝑥) / 2) ∈
ℝ) |
| 32 | 24, 31 | resubcld 11691 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℝ) |
| 33 | 32 | recnd 11289 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℂ) |
| 34 | 29 | adantr 480 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ+) |
| 35 | 5 | nnrpd 13075 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
| 36 | 34, 35 | rpdivcld 13094 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ+) |
| 37 | 36 | relogcld 26665 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘(𝑥 /
𝑛)) ∈
ℝ) |
| 38 | 8, 37 | remulcld 11291 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) ·
(log‘(𝑥 / 𝑛))) ∈
ℝ) |
| 39 | 3, 38 | fsumrecl 15770 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℝ) |
| 40 | 39, 23 | rerpdivcld 13108 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) ∈ ℝ) |
| 41 | 40, 31 | resubcld 11691 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℝ) |
| 42 | 41 | recnd 11289 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)) ∈ ℂ) |
| 43 | 17 | recnd 11289 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) ∈ ℂ) |
| 44 | 39 | recnd 11289 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) ∈ ℂ) |
| 45 | 30 | recnd 11289 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ∈
ℂ) |
| 46 | 23 | rpne0d 13082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ≠
0) |
| 47 | 43, 44, 45, 46 | divsubdird 12082 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)))) |
| 48 | 8 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℂ) |
| 49 | 15 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) / 𝑚) ∈ ℂ) |
| 50 | 37 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘(𝑥 /
𝑛)) ∈
ℂ) |
| 51 | 48, 49, 50 | subdid 11719 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) = ((((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) |
| 52 | 51 | sumeq2dv 15738 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) |
| 53 | 16 | recnd 11289 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) / 𝑚)) ∈ ℂ) |
| 54 | 38 | recnd 11289 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) ·
(log‘(𝑥 / 𝑛))) ∈
ℂ) |
| 55 | 3, 53, 54 | fsumsub 15824 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − (((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) |
| 56 | 52, 55 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))))) |
| 57 | 56 | oveq1d 7446 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) |
| 58 | 24 | recnd 11289 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) ∈ ℂ) |
| 59 | 40 | recnd 11289 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) ∈ ℂ) |
| 60 | 31 | recnd 11289 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((log‘𝑥) / 2) ∈
ℂ) |
| 61 | 58, 59, 60 | nnncan2d 11655 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)))) |
| 62 | 47, 57, 61 | 3eqtr4d 2787 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) = (((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)))) |
| 63 | 62 | mpteq2dva 5242 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) = (𝑥 ∈ (1(,)+∞) ↦
(((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))))) |
| 64 | | 1red 11262 |
. . . . 5
⊢ (𝜑 → 1 ∈
ℝ) |
| 65 | 3, 8 | fsumrecl 15770 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℝ) |
| 66 | 65, 23 | rerpdivcld 13108 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) ∈ ℝ) |
| 67 | | 2vmadivsum.1 |
. . . . . . . 8
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
| 68 | 67 | rpred 13077 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
| 69 | 68 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐴 ∈
ℝ) |
| 70 | | ioossre 13448 |
. . . . . . . 8
⊢
(1(,)+∞) ⊆ ℝ |
| 71 | | 1cnd 11256 |
. . . . . . . 8
⊢ (𝜑 → 1 ∈
ℂ) |
| 72 | | o1const 15656 |
. . . . . . . 8
⊢
(((1(,)+∞) ⊆ ℝ ∧ 1 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦
1) ∈ 𝑂(1)) |
| 73 | 70, 71, 72 | sylancr 587 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 1) ∈
𝑂(1)) |
| 74 | 66 | recnd 11289 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) ∈ ℂ) |
| 75 | | 1cnd 11256 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈
ℂ) |
| 76 | 65 | recnd 11289 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ) |
| 77 | 76, 45, 45, 46 | divsubdird 12082 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − ((log‘𝑥) / (log‘𝑥)))) |
| 78 | 76, 45 | subcld 11620 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℂ) |
| 79 | 78, 45, 46 | divrecd 12046 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) |
| 80 | 45, 46 | dividd 12041 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((log‘𝑥) /
(log‘𝑥)) =
1) |
| 81 | 80 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − ((log‘𝑥) / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) |
| 82 | 77, 79, 81 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥))) = ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) |
| 83 | 82 | mpteq2dva 5242 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1))) |
| 84 | 65, 30 | resubcld 11691 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℝ) |
| 85 | 27, 23 | rerpdivcld 13108 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (1 /
(log‘𝑥)) ∈
ℝ) |
| 86 | 29 | ex 412 |
. . . . . . . . . . . 12
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) → 𝑥 ∈
ℝ+)) |
| 87 | 86 | ssrdv 3989 |
. . . . . . . . . . 11
⊢ (𝜑 → (1(,)+∞) ⊆
ℝ+) |
| 88 | | vmadivsum 27526 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) |
| 89 | 88 | a1i 11 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) |
| 90 | 87, 89 | o1res2 15599 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) |
| 91 | | divlogrlim 26677 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ (1(,)+∞) ↦
(1 / (log‘𝑥)))
⇝𝑟 0 |
| 92 | | rlimo1 15653 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ (1(,)+∞) ↦
(1 / (log‘𝑥)))
⇝𝑟 0 → (𝑥 ∈ (1(,)+∞) ↦ (1 /
(log‘𝑥))) ∈
𝑂(1)) |
| 93 | 91, 92 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (1 /
(log‘𝑥))) ∈
𝑂(1)) |
| 94 | 84, 85, 90, 93 | o1mul2 15661 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (1 / (log‘𝑥)))) ∈
𝑂(1)) |
| 95 | 83, 94 | eqeltrrd 2842 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) − 1)) ∈
𝑂(1)) |
| 96 | 74, 75, 95 | o1dif 15666 |
. . . . . . 7
⊢ (𝜑 → ((𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
1) ∈ 𝑂(1))) |
| 97 | 73, 96 | mpbird 257 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) ∈ 𝑂(1)) |
| 98 | 68 | recnd 11289 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℂ) |
| 99 | | o1const 15656 |
. . . . . . 7
⊢
(((1(,)+∞) ⊆ ℝ ∧ 𝐴 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈
𝑂(1)) |
| 100 | 70, 98, 99 | sylancr 587 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈
𝑂(1)) |
| 101 | 66, 69, 97, 100 | o1mul2 15661 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴)) ∈ 𝑂(1)) |
| 102 | 66, 69 | remulcld 11291 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴) ∈ ℝ) |
| 103 | 15, 37 | resubcld 11691 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))) ∈ ℝ) |
| 104 | 8, 103 | remulcld 11291 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ) |
| 105 | 3, 104 | fsumrecl 15770 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ) |
| 106 | 105 | recnd 11289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℂ) |
| 107 | 106, 45, 46 | divcld 12043 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥)) ∈ ℂ) |
| 108 | 106 | abscld 15475 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ∈ ℝ) |
| 109 | 65, 69 | remulcld 11291 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) ∈ ℝ) |
| 110 | 104 | recnd 11289 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℂ) |
| 111 | 110 | abscld 15475 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ∈ ℝ) |
| 112 | 3, 111 | fsumrecl 15770 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ∈ ℝ) |
| 113 | 3, 110 | fsumabs 15837 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))))) |
| 114 | 69 | adantr 480 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝐴 ∈
ℝ) |
| 115 | 8, 114 | remulcld 11291 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) · 𝐴) ∈
ℝ) |
| 116 | 103 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))) ∈ ℂ) |
| 117 | 48, 116 | absmuld 15493 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) = ((abs‘((Λ‘𝑛) / 𝑛)) · (abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))))) |
| 118 | | vmage0 27164 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ → 0 ≤
(Λ‘𝑛)) |
| 119 | 5, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (Λ‘𝑛)) |
| 120 | 7, 35, 119 | divge0d 13117 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ ((Λ‘𝑛) / 𝑛)) |
| 121 | 8, 120 | absidd 15461 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Λ‘𝑛) / 𝑛)) = ((Λ‘𝑛) / 𝑛)) |
| 122 | 121 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((Λ‘𝑛) / 𝑛)) · (abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) = (((Λ‘𝑛) / 𝑛) · (abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))))) |
| 123 | 117, 122 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) = (((Λ‘𝑛) / 𝑛) · (abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))))) |
| 124 | 116 | abscld 15475 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ∈ ℝ) |
| 125 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑚 → (Λ‘𝑖) = (Λ‘𝑚)) |
| 126 | | id 22 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑖 = 𝑚 → 𝑖 = 𝑚) |
| 127 | 125, 126 | oveq12d 7449 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑖 = 𝑚 → ((Λ‘𝑖) / 𝑖) = ((Λ‘𝑚) / 𝑚)) |
| 128 | 127 | cbvsumv 15732 |
. . . . . . . . . . . . . . . . . 18
⊢
Σ𝑖 ∈
(1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) = Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) / 𝑚) |
| 129 | | fveq2 6906 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑥 / 𝑛) → (⌊‘𝑦) = (⌊‘(𝑥 / 𝑛))) |
| 130 | 129 | oveq2d 7447 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝑥 / 𝑛) → (1...(⌊‘𝑦)) = (1...(⌊‘(𝑥 / 𝑛)))) |
| 131 | 130 | sumeq1d 15736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (𝑥 / 𝑛) → Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) / 𝑚) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) |
| 132 | 128, 131 | eqtrid 2789 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑥 / 𝑛) → Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) |
| 133 | | fveq2 6906 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑦 = (𝑥 / 𝑛) → (log‘𝑦) = (log‘(𝑥 / 𝑛))) |
| 134 | 132, 133 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 = (𝑥 / 𝑛) → (Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) |
| 135 | 134 | fveq2d 6910 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 = (𝑥 / 𝑛) → (abs‘(Σ𝑖 ∈
(1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) |
| 136 | 135 | breq1d 5153 |
. . . . . . . . . . . . . 14
⊢ (𝑦 = (𝑥 / 𝑛) → ((abs‘(Σ𝑖 ∈
(1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) ≤ 𝐴 ↔ (abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ≤ 𝐴)) |
| 137 | | 2vmadivsum.2 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → ∀𝑦 ∈
(1[,)+∞)(abs‘(Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) ≤ 𝐴) |
| 138 | 137 | ad2antrr 726 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ∀𝑦 ∈
(1[,)+∞)(abs‘(Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) / 𝑖) − (log‘𝑦))) ≤ 𝐴) |
| 139 | 36 | rpred 13077 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ) |
| 140 | 5 | nncnd 12282 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℂ) |
| 141 | 140 | mullidd 11279 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 · 𝑛) =
𝑛) |
| 142 | | fznnfl 13902 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ → (𝑛 ∈
(1...(⌊‘𝑥))
↔ (𝑛 ∈ ℕ
∧ 𝑛 ≤ 𝑥))) |
| 143 | 19, 142 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑛 ∈
(1...(⌊‘𝑥))
↔ (𝑛 ∈ ℕ
∧ 𝑛 ≤ 𝑥))) |
| 144 | 143 | simplbda 499 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ≤ 𝑥) |
| 145 | 141, 144 | eqbrtrd 5165 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 · 𝑛) ≤
𝑥) |
| 146 | | 1red 11262 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) |
| 147 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ) |
| 148 | 146, 147,
35 | lemuldivd 13126 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 · 𝑛) ≤
𝑥 ↔ 1 ≤ (𝑥 / 𝑛))) |
| 149 | 145, 148 | mpbid 232 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ≤ (𝑥 / 𝑛)) |
| 150 | | 1re 11261 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
| 151 | | elicopnf 13485 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℝ → ((𝑥 / 𝑛) ∈ (1[,)+∞) ↔
((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛)))) |
| 152 | 150, 151 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 / 𝑛) ∈ (1[,)+∞) ↔ ((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛))) |
| 153 | 139, 149,
152 | sylanbrc 583 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
(1[,)+∞)) |
| 154 | 136, 138,
153 | rspcdva 3623 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) ≤ 𝐴) |
| 155 | 124, 114,
8, 120, 154 | lemul2ad 12208 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) ·
(abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ (((Λ‘𝑛) / 𝑛) · 𝐴)) |
| 156 | 123, 155 | eqbrtrd 5165 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ (((Λ‘𝑛) / 𝑛) · 𝐴)) |
| 157 | 3, 111, 115, 156 | fsumle 15835 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · 𝐴)) |
| 158 | 98 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐴 ∈
ℂ) |
| 159 | 3, 158, 48 | fsummulc1 15821 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · 𝐴)) |
| 160 | 157, 159 | breqtrrd 5171 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴)) |
| 161 | 108, 112,
109, 113, 160 | letrd 11418 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴)) |
| 162 | 108, 109,
23, 161 | lediv1dd 13135 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) / (log‘𝑥)) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) / (log‘𝑥))) |
| 163 | 106, 45, 46 | absdivd 15494 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) / (abs‘(log‘𝑥)))) |
| 164 | 23 | rpge0d 13081 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤
(log‘𝑥)) |
| 165 | 30, 164 | absidd 15461 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(log‘𝑥)) =
(log‘𝑥)) |
| 166 | 165 | oveq2d 7447 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) / (abs‘(log‘𝑥))) = ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) / (log‘𝑥))) |
| 167 | 163, 166 | eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) = ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛))))) / (log‘𝑥))) |
| 168 | 3, 8, 120 | fsumge0 15831 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛)) |
| 169 | 65, 23, 168 | divge0d 13117 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥))) |
| 170 | 67 | adantr 480 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐴 ∈
ℝ+) |
| 171 | 170 | rpge0d 13081 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ 𝐴) |
| 172 | 66, 69, 169, 171 | mulge0d 11840 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴)) |
| 173 | 102, 172 | absidd 15461 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘((Σ𝑛
∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴)) |
| 174 | 76, 158, 45, 46 | div23d 12080 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) / (log‘𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴)) |
| 175 | 173, 174 | eqtr4d 2780 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘((Σ𝑛
∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) / (log‘𝑥))) |
| 176 | 162, 167,
175 | 3brtr4d 5175 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ≤ (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴))) |
| 177 | 176 | adantrr 717 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ≤ (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) / (log‘𝑥)) · 𝐴))) |
| 178 | 64, 101, 102, 107, 177 | o1le 15689 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚) − (log‘(𝑥 / 𝑛)))) / (log‘𝑥))) ∈ 𝑂(1)) |
| 179 | 63, 178 | eqeltrrd 2842 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦
(((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2)))) ∈
𝑂(1)) |
| 180 | 33, 42, 179 | o1dif 15666 |
. 2
⊢ (𝜑 → ((𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (log‘(𝑥 / 𝑛))) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈
𝑂(1))) |
| 181 | 2, 180 | mpbird 257 |
1
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) / 𝑚)) / (log‘𝑥)) − ((log‘𝑥) / 2))) ∈
𝑂(1)) |