Proof of Theorem selberglem2
| Step | Hyp | Ref
| Expression |
| 1 | | reex 11246 |
. . . . . . 7
⊢ ℝ
∈ V |
| 2 | | rpssre 13042 |
. . . . . . 7
⊢
ℝ+ ⊆ ℝ |
| 3 | 1, 2 | ssexi 5322 |
. . . . . 6
⊢
ℝ+ ∈ V |
| 4 | 3 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℝ+ ∈ V) |
| 5 | | fzfid 14014 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin) |
| 6 | | elfznn 13593 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
| 7 | 6 | adantl 481 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
| 8 | | mucl 27184 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(μ‘𝑛) ∈
ℤ) |
| 9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈
ℤ) |
| 10 | 9 | zred 12722 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈
ℝ) |
| 11 | 10 | recnd 11289 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈
ℂ) |
| 12 | | fzfid 14014 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(1...(⌊‘(𝑥 /
𝑛))) ∈
Fin) |
| 13 | | elfznn 13593 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛))) → 𝑚 ∈
ℕ) |
| 14 | 13 | adantl 481 |
. . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ) |
| 15 | 14 | nnrpd 13075 |
. . . . . . . . . . . . 13
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℝ+) |
| 16 | 15 | relogcld 26665 |
. . . . . . . . . . . 12
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘𝑚) ∈ ℝ) |
| 17 | 16 | resqcld 14165 |
. . . . . . . . . . 11
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘𝑚)↑2) ∈ ℝ) |
| 18 | 12, 17 | fsumrecl 15770 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) ∈
ℝ) |
| 19 | | simplr 769 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+) |
| 20 | 18, 19 | rerpdivcld 13108 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) ∈ ℝ) |
| 21 | 20 | recnd 11289 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) ∈ ℂ) |
| 22 | | selberglem1.t |
. . . . . . . . . 10
⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) / 𝑛) |
| 23 | | simpr 484 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℝ+) |
| 24 | 6 | nnrpd 13075 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℝ+) |
| 25 | | rpdivcl 13060 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 / 𝑛) ∈
ℝ+) |
| 26 | 23, 24, 25 | syl2an 596 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈
ℝ+) |
| 27 | 26 | relogcld 26665 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ) |
| 28 | 27 | resqcld 14165 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ) |
| 29 | | 2re 12340 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
| 30 | | remulcl 11240 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℝ ∧ (log‘(𝑥 / 𝑛)) ∈ ℝ) → (2 ·
(log‘(𝑥 / 𝑛))) ∈
ℝ) |
| 31 | 29, 27, 30 | sylancr 587 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 ·
(log‘(𝑥 / 𝑛))) ∈
ℝ) |
| 32 | | resubcl 11573 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ ∧ (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ) → (2 − (2
· (log‘(𝑥 /
𝑛)))) ∈
ℝ) |
| 33 | 29, 31, 32 | sylancr 587 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 − (2
· (log‘(𝑥 /
𝑛)))) ∈
ℝ) |
| 34 | 28, 33 | readdcld 11290 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) ∈
ℝ) |
| 35 | 34, 7 | nndivred 12320 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) / 𝑛) ∈ ℝ) |
| 36 | 22, 35 | eqeltrid 2845 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℝ) |
| 37 | 36 | recnd 11289 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ) |
| 38 | 21, 37 | subcld 11620 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) ∈ ℂ) |
| 39 | 11, 38 | mulcld 11281 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ) |
| 40 | 5, 39 | fsumcl 15769 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ) |
| 41 | 11, 37 | mulcld 11281 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · 𝑇) ∈ ℂ) |
| 42 | 5, 41 | fsumcl 15769 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) ∈ ℂ) |
| 43 | | 2cn 12341 |
. . . . . . 7
⊢ 2 ∈
ℂ |
| 44 | | relogcl 26617 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
| 45 | 44 | adantl 481 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘𝑥) ∈ ℝ) |
| 46 | 45 | recnd 11289 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘𝑥) ∈ ℂ) |
| 47 | | mulcl 11239 |
. . . . . . 7
⊢ ((2
∈ ℂ ∧ (log‘𝑥) ∈ ℂ) → (2 ·
(log‘𝑥)) ∈
ℂ) |
| 48 | 43, 46, 47 | sylancr 587 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (2 · (log‘𝑥)) ∈ ℂ) |
| 49 | 42, 48 | subcld 11620 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))) ∈
ℂ) |
| 50 | | eqidd 2738 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))) |
| 51 | | eqidd 2738 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) |
| 52 | 4, 40, 49, 50, 51 | offval2 7717 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘f + (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))))) |
| 53 | 40, 42, 48 | addsubassd 11640 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) − (2 · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) |
| 54 | | rpcnne0 13053 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
| 55 | 54 | adantl 481 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
| 56 | 55 | simpld 494 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℂ) |
| 57 | 10 | adantr 480 |
. . . . . . . . . . . 12
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (μ‘𝑛) ∈ ℝ) |
| 58 | 57, 17 | remulcld 11291 |
. . . . . . . . . . 11
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℝ) |
| 59 | 12, 58 | fsumrecl 15770 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) ∈
ℝ) |
| 60 | 59 | recnd 11289 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) ∈
ℂ) |
| 61 | 55 | simprd 495 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ≠ 0) |
| 62 | 5, 56, 60, 61 | fsumdivc 15822 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥)) |
| 63 | 17 | recnd 11289 |
. . . . . . . . . . . 12
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘𝑚)↑2) ∈ ℂ) |
| 64 | 12, 63 | fsumcl 15769 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) ∈
ℂ) |
| 65 | 55 | adantr 480 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
| 66 | | divass 11940 |
. . . . . . . . . . 11
⊢
(((μ‘𝑛)
∈ ℂ ∧ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) →
(((μ‘𝑛) ·
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2)) / 𝑥) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥))) |
| 67 | 11, 64, 65, 66 | syl3anc 1373 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2)) / 𝑥) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥))) |
| 68 | 12, 11, 63 | fsummulc2 15820 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2)) = Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2))) |
| 69 | 68 | oveq1d 7446 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2)) / 𝑥) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥)) |
| 70 | 21, 37 | npcand 11624 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) |
| 71 | 70 | oveq2d 7447 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇)) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥))) |
| 72 | 11, 38, 37 | adddid 11285 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇)) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇))) |
| 73 | 71, 72 | eqtr3d 2779 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥)) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇))) |
| 74 | 67, 69, 73 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇))) |
| 75 | 74 | sumeq2dv 15738 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇))) |
| 76 | 5, 39, 41 | fsumadd 15776 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇))) |
| 77 | 62, 75, 76 | 3eqtrrd 2782 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥)) |
| 78 | 77 | oveq1d 7446 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) − (2 · (log‘𝑥))) = ((Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) |
| 79 | 53, 78 | eqtr3d 2779 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) = ((Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) |
| 80 | 79 | mpteq2dva 5242 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥))))) |
| 81 | 52, 80 | eqtrd 2777 |
. . 3
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘f + (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥))))) |
| 82 | | 1red 11262 |
. . . . 5
⊢ (⊤
→ 1 ∈ ℝ) |
| 83 | 5, 28 | fsumrecl 15770 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℝ) |
| 84 | 83, 23 | rerpdivcld 13108 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℝ) |
| 85 | 84 | recnd 11289 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℂ) |
| 86 | | 2cnd 12344 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 2 ∈ ℂ) |
| 87 | | 2nn0 12543 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
| 88 | | logexprlim 27269 |
. . . . . . . 8
⊢ (2 ∈
ℕ0 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥)) ⇝𝑟
(!‘2)) |
| 89 | 87, 88 | mp1i 13 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥)) ⇝𝑟
(!‘2)) |
| 90 | | 2cnd 12344 |
. . . . . . . 8
⊢ (⊤
→ 2 ∈ ℂ) |
| 91 | | rlimconst 15580 |
. . . . . . . 8
⊢
((ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ) →
(𝑥 ∈
ℝ+ ↦ 2) ⇝𝑟 2) |
| 92 | 2, 90, 91 | sylancr 587 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ 2) ⇝𝑟 2) |
| 93 | 85, 86, 89, 92 | rlimadd 15679 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ⇝𝑟
((!‘2) + 2)) |
| 94 | | rlimo1 15653 |
. . . . . 6
⊢ ((𝑥 ∈ ℝ+
↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ⇝𝑟
((!‘2) + 2) → (𝑥
∈ ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ∈ 𝑂(1)) |
| 95 | 93, 94 | syl 17 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ∈ 𝑂(1)) |
| 96 | | readdcl 11238 |
. . . . . 6
⊢
(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℝ ∧ 2 ∈ ℝ)
→ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℝ) |
| 97 | 84, 29, 96 | sylancl 586 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℝ) |
| 98 | 40 | abscld 15475 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ) |
| 99 | 97 | recnd 11289 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℂ) |
| 100 | 99 | abscld 15475 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ∈ ℝ) |
| 101 | 39 | abscld 15475 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((μ‘𝑛)
· ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ) |
| 102 | 5, 101 | fsumrecl 15770 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ) |
| 103 | 5, 39 | fsumabs 15837 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))) |
| 104 | | readdcl 11238 |
. . . . . . . . . . . 12
⊢
((((log‘(𝑥 /
𝑛))↑2) ∈ ℝ
∧ 2 ∈ ℝ) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈
ℝ) |
| 105 | 28, 29, 104 | sylancl 586 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈
ℝ) |
| 106 | 105, 19 | rerpdivcld 13108 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ∈ ℝ) |
| 107 | 5, 106 | fsumrecl 15770 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ∈ ℝ) |
| 108 | 38 | abscld 15475 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℝ) |
| 109 | 11, 38 | absmuld 15493 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((μ‘𝑛)
· ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = ((abs‘(μ‘𝑛)) ·
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))) |
| 110 | 11 | abscld 15475 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(μ‘𝑛))
∈ ℝ) |
| 111 | | 1red 11262 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℝ) |
| 112 | 38 | absge0d 15483 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) |
| 113 | | mule1 27191 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
(abs‘(μ‘𝑛))
≤ 1) |
| 114 | 7, 113 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(μ‘𝑛))
≤ 1) |
| 115 | 110, 111,
108, 112, 114 | lemul1ad 12207 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((abs‘(μ‘𝑛))
· (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (1 ·
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))) |
| 116 | 108 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ) |
| 117 | 116 | mullidd 11279 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 ·
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) |
| 118 | 115, 117 | breqtrd 5169 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((abs‘(μ‘𝑛))
· (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) |
| 119 | 109, 118 | eqbrtrd 5165 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((μ‘𝑛)
· ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) |
| 120 | 65 | simpld 494 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ) |
| 121 | 120, 38 | absmuld 15493 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = ((abs‘𝑥) · (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))) |
| 122 | 120, 21, 37 | subdid 11719 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) = ((𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) − (𝑥 · 𝑇))) |
| 123 | 65 | simprd 495 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ≠ 0) |
| 124 | 64, 120, 123 | divcan2d 12045 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) |
| 125 | 34 | recnd 11289 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) ∈
ℂ) |
| 126 | 7 | nnrpd 13075 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+) |
| 127 | | rpcnne0 13053 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℝ+
→ (𝑛 ∈ ℂ
∧ 𝑛 ≠
0)) |
| 128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) |
| 129 | | divass 11940 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℂ ∧
(((log‘(𝑥 / 𝑛))↑2) + (2 − (2
· (log‘(𝑥 /
𝑛))))) ∈ ℂ ∧
(𝑛 ∈ ℂ ∧
𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛)))))) / 𝑛) = (𝑥 · ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) / 𝑛))) |
| 130 | 22 | oveq2i 7442 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 · 𝑇) = (𝑥 · ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) / 𝑛)) |
| 131 | 129, 130 | eqtr4di 2795 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧
(((log‘(𝑥 / 𝑛))↑2) + (2 − (2
· (log‘(𝑥 /
𝑛))))) ∈ ℂ ∧
(𝑛 ∈ ℂ ∧
𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛)))))) / 𝑛) = (𝑥 · 𝑇)) |
| 132 | | div23 11941 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧
(((log‘(𝑥 / 𝑛))↑2) + (2 − (2
· (log‘(𝑥 /
𝑛))))) ∈ ℂ ∧
(𝑛 ∈ ℂ ∧
𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛)))))) / 𝑛) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
| 133 | 131, 132 | eqtr3d 2779 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
(((log‘(𝑥 / 𝑛))↑2) + (2 − (2
· (log‘(𝑥 /
𝑛))))) ∈ ℂ ∧
(𝑛 ∈ ℂ ∧
𝑛 ≠ 0)) → (𝑥 · 𝑇) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
| 134 | 120, 125,
128, 133 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · 𝑇) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
| 135 | 124, 134 | oveq12d 7449 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) − (𝑥 · 𝑇)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛)))))))) |
| 136 | 122, 135 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛)))))))) |
| 137 | 136 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))))))) |
| 138 | | rprege0 13050 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
| 139 | | absid 15335 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → (abs‘𝑥) = 𝑥) |
| 140 | 19, 138, 139 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑥) = 𝑥) |
| 141 | 140 | oveq1d 7446 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘𝑥) ·
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (𝑥 · (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))) |
| 142 | 121, 137,
141 | 3eqtr3d 2785 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛)))))))) = (𝑥 · (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))) |
| 143 | 7 | nncnd 12282 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ) |
| 144 | 143 | mullidd 11279 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛) |
| 145 | | rpre 13043 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
| 146 | 145 | adantl 481 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℝ) |
| 147 | | fznnfl 13902 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ → (𝑛 ∈
(1...(⌊‘𝑥))
↔ (𝑛 ∈ ℕ
∧ 𝑛 ≤ 𝑥))) |
| 148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥))) |
| 149 | 148 | simplbda 499 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≤ 𝑥) |
| 150 | 144, 149 | eqbrtrd 5165 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥) |
| 151 | 19 | rpred 13077 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ) |
| 152 | 111, 151,
126 | lemuldivd 13126 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛))) |
| 153 | 150, 152 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛)) |
| 154 | | log2sumbnd 27588 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 / 𝑛) ∈ ℝ+ ∧ 1 ≤
(𝑥 / 𝑛)) → (abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛)))))))) ≤
(((log‘(𝑥 / 𝑛))↑2) +
2)) |
| 155 | 26, 153, 154 | syl2anc 584 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛)))))))) ≤
(((log‘(𝑥 / 𝑛))↑2) +
2)) |
| 156 | 142, 155 | eqbrtrrd 5167 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2)) |
| 157 | 108, 105,
19 | lemuldiv2d 13127 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 · (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2) ↔
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))) |
| 158 | 156, 157 | mpbid 232 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥)) |
| 159 | 101, 108,
106, 119, 158 | letrd 11418 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((μ‘𝑛)
· ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥)) |
| 160 | 5, 101, 106, 159 | fsumle 15835 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥)) |
| 161 | 5, 105 | fsumrecl 15770 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) ∈
ℝ) |
| 162 | | remulcl 11240 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 2 ∈
ℝ) → (𝑥 ·
2) ∈ ℝ) |
| 163 | 146, 29, 162 | sylancl 586 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 · 2) ∈ ℝ) |
| 164 | 83, 163 | readdcld 11290 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) ∈
ℝ) |
| 165 | 28 | recnd 11289 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℂ) |
| 166 | | 2cnd 12344 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈
ℂ) |
| 167 | 5, 165, 166 | fsumadd 15776 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + Σ𝑛 ∈ (1...(⌊‘𝑥))2)) |
| 168 | | fsumconst 15826 |
. . . . . . . . . . . . . . . 16
⊢
(((1...(⌊‘𝑥)) ∈ Fin ∧ 2 ∈ ℂ) →
Σ𝑛 ∈
(1...(⌊‘𝑥))2 =
((♯‘(1...(⌊‘𝑥))) · 2)) |
| 169 | 5, 43, 168 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 =
((♯‘(1...(⌊‘𝑥))) · 2)) |
| 170 | 138 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) |
| 171 | | flge0nn0 13860 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
| 172 | | hashfz1 14385 |
. . . . . . . . . . . . . . . . 17
⊢
((⌊‘𝑥)
∈ ℕ0 → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥)) |
| 173 | 170, 171,
172 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥)) |
| 174 | 173 | oveq1d 7446 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((♯‘(1...(⌊‘𝑥))) · 2) =
((⌊‘𝑥) ·
2)) |
| 175 | 169, 174 | eqtrd 2777 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((⌊‘𝑥) · 2)) |
| 176 | 175 | oveq2d 7447 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + Σ𝑛 ∈ (1...(⌊‘𝑥))2) = (Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2))) |
| 177 | 167, 176 | eqtrd 2777 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2))) |
| 178 | | reflcl 13836 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ∈
ℝ) |
| 179 | 146, 178 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (⌊‘𝑥) ∈ ℝ) |
| 180 | 29 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 2 ∈ ℝ) |
| 181 | 179, 180 | remulcld 11291 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((⌊‘𝑥) · 2) ∈
ℝ) |
| 182 | | flle 13839 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ≤
𝑥) |
| 183 | 146, 182 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (⌊‘𝑥) ≤ 𝑥) |
| 184 | | 2pos 12369 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
2 |
| 185 | 29, 184 | pm3.2i 470 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℝ ∧ 0 < 2) |
| 186 | 185 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (2 ∈ ℝ ∧ 0 <
2)) |
| 187 | | lemul1 12119 |
. . . . . . . . . . . . . . 15
⊢
(((⌊‘𝑥)
∈ ℝ ∧ 𝑥
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) →
((⌊‘𝑥) ≤
𝑥 ↔
((⌊‘𝑥) ·
2) ≤ (𝑥 ·
2))) |
| 188 | 179, 146,
186, 187 | syl3anc 1373 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((⌊‘𝑥) ≤ 𝑥 ↔ ((⌊‘𝑥) · 2) ≤ (𝑥 · 2))) |
| 189 | 183, 188 | mpbid 232 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((⌊‘𝑥) · 2) ≤ (𝑥 · 2)) |
| 190 | 181, 163,
83, 189 | leadd2dd 11878 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2)) ≤
(Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2))) |
| 191 | 177, 190 | eqbrtrd 5165 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) ≤ (Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2))) |
| 192 | 161, 164,
23, 191 | lediv1dd 13135 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥)) |
| 193 | 105 | recnd 11289 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈
ℂ) |
| 194 | 5, 56, 193, 61 | fsumdivc 15822 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥)) |
| 195 | 83 | recnd 11289 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℂ) |
| 196 | 56, 86 | mulcld 11281 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 · 2) ∈ ℂ) |
| 197 | | divdir 11947 |
. . . . . . . . . . . 12
⊢
((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℂ ∧ (𝑥 · 2) ∈ ℂ
∧ (𝑥 ∈ ℂ
∧ 𝑥 ≠ 0)) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥))) |
| 198 | 195, 196,
55, 197 | syl3anc 1373 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥))) |
| 199 | 86, 56, 61 | divcan3d 12048 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((𝑥 · 2) / 𝑥) = 2) |
| 200 | 199 | oveq2d 7447 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) |
| 201 | 198, 200 | eqtrd 2777 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) |
| 202 | 192, 194,
201 | 3brtr3d 5174 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) |
| 203 | 102, 107,
97, 160, 202 | letrd 11418 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) |
| 204 | 98, 102, 97, 103, 203 | letrd 11418 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) |
| 205 | 97 | leabsd 15453 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ≤ (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))) |
| 206 | 98, 97, 100, 204, 205 | letrd 11418 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))) |
| 207 | 206 | adantrr 717 |
. . . . 5
⊢
((⊤ ∧ (𝑥
∈ ℝ+ ∧ 1 ≤ 𝑥)) → (abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))) |
| 208 | 82, 95, 97, 40, 207 | o1le 15689 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ 𝑂(1)) |
| 209 | 22 | selberglem1 27589 |
. . . 4
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈
𝑂(1) |
| 210 | | o1add 15650 |
. . . 4
⊢ (((𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈ 𝑂(1)) →
((𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘f + (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) ∈
𝑂(1)) |
| 211 | 208, 209,
210 | sylancl 586 |
. . 3
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘f + (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) ∈
𝑂(1)) |
| 212 | 81, 211 | eqeltrrd 2842 |
. 2
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1)) |
| 213 | 212 | mptru 1547 |
1
⊢ (𝑥 ∈ ℝ+
↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1) |