Proof of Theorem selberglem2
Step | Hyp | Ref
| Expression |
1 | | reex 10718 |
. . . . . . 7
⊢ ℝ
∈ V |
2 | | rpssre 12491 |
. . . . . . 7
⊢
ℝ+ ⊆ ℝ |
3 | 1, 2 | ssexi 5200 |
. . . . . 6
⊢
ℝ+ ∈ V |
4 | 3 | a1i 11 |
. . . . 5
⊢ (⊤
→ ℝ+ ∈ V) |
5 | | fzfid 13444 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin) |
6 | | elfznn 13039 |
. . . . . . . . . . 11
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
7 | 6 | adantl 485 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
8 | | mucl 25890 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℕ →
(μ‘𝑛) ∈
ℤ) |
9 | 7, 8 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈
ℤ) |
10 | 9 | zred 12180 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈
ℝ) |
11 | 10 | recnd 10759 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (μ‘𝑛) ∈
ℂ) |
12 | | fzfid 13444 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(1...(⌊‘(𝑥 /
𝑛))) ∈
Fin) |
13 | | elfznn 13039 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛))) → 𝑚 ∈
ℕ) |
14 | 13 | adantl 485 |
. . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ) |
15 | 14 | nnrpd 12524 |
. . . . . . . . . . . . 13
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℝ+) |
16 | 15 | relogcld 25378 |
. . . . . . . . . . . 12
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘𝑚) ∈ ℝ) |
17 | 16 | resqcld 13715 |
. . . . . . . . . . 11
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘𝑚)↑2) ∈ ℝ) |
18 | 12, 17 | fsumrecl 15196 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) ∈
ℝ) |
19 | | simplr 769 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+) |
20 | 18, 19 | rerpdivcld 12557 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) ∈ ℝ) |
21 | 20 | recnd 10759 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) ∈ ℂ) |
22 | | selberglem1.t |
. . . . . . . . . 10
⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) / 𝑛) |
23 | | simpr 488 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℝ+) |
24 | 6 | nnrpd 12524 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℝ+) |
25 | | rpdivcl 12509 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 / 𝑛) ∈
ℝ+) |
26 | 23, 24, 25 | syl2an 599 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈
ℝ+) |
27 | 26 | relogcld 25378 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘(𝑥 / 𝑛)) ∈ ℝ) |
28 | 27 | resqcld 13715 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℝ) |
29 | | 2re 11802 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
30 | | remulcl 10712 |
. . . . . . . . . . . . . 14
⊢ ((2
∈ ℝ ∧ (log‘(𝑥 / 𝑛)) ∈ ℝ) → (2 ·
(log‘(𝑥 / 𝑛))) ∈
ℝ) |
31 | 29, 27, 30 | sylancr 590 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 ·
(log‘(𝑥 / 𝑛))) ∈
ℝ) |
32 | | resubcl 11040 |
. . . . . . . . . . . . 13
⊢ ((2
∈ ℝ ∧ (2 · (log‘(𝑥 / 𝑛))) ∈ ℝ) → (2 − (2
· (log‘(𝑥 /
𝑛)))) ∈
ℝ) |
33 | 29, 31, 32 | sylancr 590 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (2 − (2
· (log‘(𝑥 /
𝑛)))) ∈
ℝ) |
34 | 28, 33 | readdcld 10760 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) ∈
ℝ) |
35 | 34, 7 | nndivred 11782 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) / 𝑛) ∈ ℝ) |
36 | 22, 35 | eqeltrid 2838 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℝ) |
37 | 36 | recnd 10759 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑇 ∈ ℂ) |
38 | 21, 37 | subcld 11087 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) ∈ ℂ) |
39 | 11, 38 | mulcld 10751 |
. . . . . 6
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ) |
40 | 5, 39 | fsumcl 15195 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ) |
41 | 11, 37 | mulcld 10751 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · 𝑇) ∈ ℂ) |
42 | 5, 41 | fsumcl 15195 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) ∈ ℂ) |
43 | | 2cn 11803 |
. . . . . . 7
⊢ 2 ∈
ℂ |
44 | | relogcl 25331 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
45 | 44 | adantl 485 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘𝑥) ∈ ℝ) |
46 | 45 | recnd 10759 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (log‘𝑥) ∈ ℂ) |
47 | | mulcl 10711 |
. . . . . . 7
⊢ ((2
∈ ℂ ∧ (log‘𝑥) ∈ ℂ) → (2 ·
(log‘𝑥)) ∈
ℂ) |
48 | 43, 46, 47 | sylancr 590 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (2 · (log‘𝑥)) ∈ ℂ) |
49 | 42, 48 | subcld 11087 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))) ∈
ℂ) |
50 | | eqidd 2740 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))) |
51 | | eqidd 2740 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) |
52 | 4, 40, 49, 50, 51 | offval2 7456 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘f + (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))))) |
53 | 40, 42, 48 | addsubassd 11107 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) − (2 · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) |
54 | | rpcnne0 12502 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
55 | 54 | adantl 485 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
56 | 55 | simpld 498 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℂ) |
57 | 10 | adantr 484 |
. . . . . . . . . . . 12
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (μ‘𝑛) ∈ ℝ) |
58 | 57, 17 | remulcld 10761 |
. . . . . . . . . . 11
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((μ‘𝑛) · ((log‘𝑚)↑2)) ∈ ℝ) |
59 | 12, 58 | fsumrecl 15196 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) ∈
ℝ) |
60 | 59 | recnd 10759 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) ∈
ℂ) |
61 | 55 | simprd 499 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ≠ 0) |
62 | 5, 56, 60, 61 | fsumdivc 15246 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥)) |
63 | 17 | recnd 10759 |
. . . . . . . . . . . 12
⊢
((((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘𝑚)↑2) ∈ ℂ) |
64 | 12, 63 | fsumcl 15195 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) ∈
ℂ) |
65 | 55 | adantr 484 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) |
66 | | divass 11406 |
. . . . . . . . . . 11
⊢
(((μ‘𝑛)
∈ ℂ ∧ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) ∈ ℂ ∧ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0)) →
(((μ‘𝑛) ·
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2)) / 𝑥) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥))) |
67 | 11, 64, 65, 66 | syl3anc 1372 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2)) / 𝑥) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥))) |
68 | 12, 11, 63 | fsummulc2 15244 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2)) = Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2))) |
69 | 68 | oveq1d 7197 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((μ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2)) / 𝑥) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥)) |
70 | 21, 37 | npcand 11091 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) |
71 | 70 | oveq2d 7198 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇)) = ((μ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥))) |
72 | 11, 38, 37 | adddid 10755 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇) + 𝑇)) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇))) |
73 | 71, 72 | eqtr3d 2776 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((μ‘𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥)) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇))) |
74 | 67, 69, 73 | 3eqtr3d 2782 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = (((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇))) |
75 | 74 | sumeq2dv 15165 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇))) |
76 | 5, 39, 41 | fsumadd 15201 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + ((μ‘𝑛) · 𝑇)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇))) |
77 | 62, 75, 76 | 3eqtrrd 2779 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥)) |
78 | 77 | oveq1d 7197 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇)) − (2 · (log‘𝑥))) = ((Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) |
79 | 53, 78 | eqtr3d 2776 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) = ((Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) |
80 | 79 | mpteq2dva 5135 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) + (Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥))))) |
81 | 52, 80 | eqtrd 2774 |
. . 3
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘f + (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) = (𝑥 ∈ ℝ+ ↦
((Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥))))) |
82 | | 1red 10732 |
. . . . 5
⊢ (⊤
→ 1 ∈ ℝ) |
83 | 5, 28 | fsumrecl 15196 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℝ) |
84 | 83, 23 | rerpdivcld 12557 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℝ) |
85 | 84 | recnd 10759 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℂ) |
86 | | 2cnd 11806 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 2 ∈ ℂ) |
87 | | 2nn0 12005 |
. . . . . . . 8
⊢ 2 ∈
ℕ0 |
88 | | logexprlim 25973 |
. . . . . . . 8
⊢ (2 ∈
ℕ0 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥)) ⇝𝑟
(!‘2)) |
89 | 87, 88 | mp1i 13 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥)) ⇝𝑟
(!‘2)) |
90 | | 2cnd 11806 |
. . . . . . . 8
⊢ (⊤
→ 2 ∈ ℂ) |
91 | | rlimconst 15003 |
. . . . . . . 8
⊢
((ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ) →
(𝑥 ∈
ℝ+ ↦ 2) ⇝𝑟 2) |
92 | 2, 90, 91 | sylancr 590 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ 2) ⇝𝑟 2) |
93 | 85, 86, 89, 92 | rlimadd 15102 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ⇝𝑟
((!‘2) + 2)) |
94 | | rlimo1 15076 |
. . . . . 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 10710 |
. . . . . 6
⊢
(((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) ∈ ℝ ∧ 2 ∈ ℝ)
→ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℝ) |
97 | 84, 29, 96 | sylancl 589 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℝ) |
98 | 40 | abscld 14898 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ) |
99 | 97 | recnd 10759 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ∈ ℂ) |
100 | 99 | abscld 14898 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) ∈ ℝ) |
101 | 39 | abscld 14898 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((μ‘𝑛)
· ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ) |
102 | 5, 101 | fsumrecl 15196 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ ℝ) |
103 | 5, 39 | fsumabs 15261 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))) |
104 | | readdcl 10710 |
. . . . . . . . . . . 12
⊢
((((log‘(𝑥 /
𝑛))↑2) ∈ ℝ
∧ 2 ∈ ℝ) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈
ℝ) |
105 | 28, 29, 104 | sylancl 589 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈
ℝ) |
106 | 105, 19 | rerpdivcld 12557 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ∈ ℝ) |
107 | 5, 106 | fsumrecl 15196 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ∈ ℝ) |
108 | 38 | abscld 14898 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℝ) |
109 | 11, 38 | absmuld 14916 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((μ‘𝑛)
· ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = ((abs‘(μ‘𝑛)) ·
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))) |
110 | 11 | abscld 14898 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(μ‘𝑛))
∈ ℝ) |
111 | | 1red 10732 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℝ) |
112 | 38 | absge0d 14906 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) |
113 | | mule1 25897 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ →
(abs‘(μ‘𝑛))
≤ 1) |
114 | 7, 113 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(μ‘𝑛))
≤ 1) |
115 | 110, 111,
108, 112, 114 | lemul1ad 11669 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((abs‘(μ‘𝑛))
· (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (1 ·
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))) |
116 | 108 | recnd 10759 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ∈ ℂ) |
117 | 116 | mulid2d 10749 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 ·
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) |
118 | 115, 117 | breqtrd 5066 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((abs‘(μ‘𝑛))
· (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) |
119 | 109, 118 | eqbrtrd 5062 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((μ‘𝑛)
· ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) |
120 | 65 | simpld 498 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℂ) |
121 | 120, 38 | absmuld 14916 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = ((abs‘𝑥) · (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))) |
122 | 120, 21, 37 | subdid 11186 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) = ((𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) − (𝑥 · 𝑇))) |
123 | 65 | simprd 499 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ≠ 0) |
124 | 64, 120, 123 | divcan2d 11508 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2)) |
125 | 34 | recnd 10759 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) ∈
ℂ) |
126 | 7 | nnrpd 12524 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+) |
127 | | rpcnne0 12502 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℝ+
→ (𝑛 ∈ ℂ
∧ 𝑛 ≠
0)) |
128 | 126, 127 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) |
129 | | divass 11406 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℂ ∧
(((log‘(𝑥 / 𝑛))↑2) + (2 − (2
· (log‘(𝑥 /
𝑛))))) ∈ ℂ ∧
(𝑛 ∈ ℂ ∧
𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛)))))) / 𝑛) = (𝑥 · ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) / 𝑛))) |
130 | 22 | oveq2i 7193 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 · 𝑇) = (𝑥 · ((((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))) / 𝑛)) |
131 | 129, 130 | eqtr4di 2792 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧
(((log‘(𝑥 / 𝑛))↑2) + (2 − (2
· (log‘(𝑥 /
𝑛))))) ∈ ℂ ∧
(𝑛 ∈ ℂ ∧
𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛)))))) / 𝑛) = (𝑥 · 𝑇)) |
132 | | div23 11407 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑥 ∈ ℂ ∧
(((log‘(𝑥 / 𝑛))↑2) + (2 − (2
· (log‘(𝑥 /
𝑛))))) ∈ ℂ ∧
(𝑛 ∈ ℂ ∧
𝑛 ≠ 0)) → ((𝑥 · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛)))))) / 𝑛) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
133 | 131, 132 | eqtr3d 2776 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 ∈ ℂ ∧
(((log‘(𝑥 / 𝑛))↑2) + (2 − (2
· (log‘(𝑥 /
𝑛))))) ∈ ℂ ∧
(𝑛 ∈ ℂ ∧
𝑛 ≠ 0)) → (𝑥 · 𝑇) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
134 | 120, 125,
128, 133 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · 𝑇) = ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))))) |
135 | 124, 134 | oveq12d 7200 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥)) − (𝑥 · 𝑇)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛)))))))) |
136 | 122, 135 | eqtrd 2774 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛)))))))) |
137 | 136 | fveq2d 6690 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑥 · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛))))))))) |
138 | | rprege0 12499 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 ≤ 𝑥)) |
139 | | absid 14758 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) → (abs‘𝑥) = 𝑥) |
140 | 19, 138, 139 | 3syl 18 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘𝑥) = 𝑥) |
141 | 140 | oveq1d 7197 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘𝑥) ·
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) = (𝑥 · (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))) |
142 | 121, 137,
141 | 3eqtr3d 2782 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛)))))))) = (𝑥 · (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)))) |
143 | 7 | nncnd 11744 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℂ) |
144 | 143 | mulid2d 10749 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) = 𝑛) |
145 | | rpre 12492 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
146 | 145 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 𝑥 ∈ ℝ) |
147 | | fznnfl 13333 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℝ → (𝑛 ∈
(1...(⌊‘𝑥))
↔ (𝑛 ∈ ℕ
∧ 𝑛 ≤ 𝑥))) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑛 ∈ (1...(⌊‘𝑥)) ↔ (𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥))) |
149 | 148 | simplbda 503 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ≤ 𝑥) |
150 | 144, 149 | eqbrtrd 5062 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1 · 𝑛) ≤ 𝑥) |
151 | 19 | rpred 12526 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ) |
152 | 111, 151,
126 | lemuldivd 12575 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((1 · 𝑛) ≤ 𝑥 ↔ 1 ≤ (𝑥 / 𝑛))) |
153 | 150, 152 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ (𝑥 / 𝑛)) |
154 | | log2sumbnd 26292 |
. . . . . . . . . . . . . 14
⊢ (((𝑥 / 𝑛) ∈ ℝ+ ∧ 1 ≤
(𝑥 / 𝑛)) → (abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛)))))))) ≤
(((log‘(𝑥 / 𝑛))↑2) +
2)) |
155 | 26, 153, 154 | syl2anc 587 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) − ((𝑥 / 𝑛) · (((log‘(𝑥 / 𝑛))↑2) + (2 − (2 ·
(log‘(𝑥 / 𝑛)))))))) ≤
(((log‘(𝑥 / 𝑛))↑2) +
2)) |
156 | 142, 155 | eqbrtrrd 5064 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 · (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2)) |
157 | 108, 105,
19 | lemuldiv2d 12576 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑥 · (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ (((log‘(𝑥 / 𝑛))↑2) + 2) ↔
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥))) |
158 | 156, 157 | mpbid 235 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇)) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥)) |
159 | 101, 108,
106, 119, 158 | letrd 10887 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((μ‘𝑛)
· ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥)) |
160 | 5, 101, 106, 159 | fsumle 15259 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥)) |
161 | 5, 105 | fsumrecl 15196 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) ∈
ℝ) |
162 | | remulcl 10712 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ ℝ ∧ 2 ∈
ℝ) → (𝑥 ·
2) ∈ ℝ) |
163 | 146, 29, 162 | sylancl 589 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 · 2) ∈ ℝ) |
164 | 83, 163 | readdcld 10760 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) ∈
ℝ) |
165 | 28 | recnd 10759 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((log‘(𝑥 / 𝑛))↑2) ∈ ℂ) |
166 | | 2cnd 11806 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 2 ∈
ℂ) |
167 | 5, 165, 166 | fsumadd 15201 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + Σ𝑛 ∈ (1...(⌊‘𝑥))2)) |
168 | | fsumconst 15250 |
. . . . . . . . . . . . . . . 16
⊢
(((1...(⌊‘𝑥)) ∈ Fin ∧ 2 ∈ ℂ) →
Σ𝑛 ∈
(1...(⌊‘𝑥))2 =
((♯‘(1...(⌊‘𝑥))) · 2)) |
169 | 5, 43, 168 | sylancl 589 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 =
((♯‘(1...(⌊‘𝑥))) · 2)) |
170 | 138 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 ∈ ℝ ∧ 0 ≤ 𝑥)) |
171 | | flge0nn0 13293 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ ∧ 0 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ0) |
172 | | hashfz1 13810 |
. . . . . . . . . . . . . . . . 17
⊢
((⌊‘𝑥)
∈ ℕ0 → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥)) |
173 | 170, 171,
172 | 3syl 18 |
. . . . . . . . . . . . . . . 16
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (♯‘(1...(⌊‘𝑥))) = (⌊‘𝑥)) |
174 | 173 | oveq1d 7197 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((♯‘(1...(⌊‘𝑥))) · 2) =
((⌊‘𝑥) ·
2)) |
175 | 169, 174 | eqtrd 2774 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))2 = ((⌊‘𝑥) · 2)) |
176 | 175 | oveq2d 7198 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + Σ𝑛 ∈ (1...(⌊‘𝑥))2) = (Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2))) |
177 | 167, 176 | eqtrd 2774 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2))) |
178 | | reflcl 13269 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ∈
ℝ) |
179 | 146, 178 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (⌊‘𝑥) ∈ ℝ) |
180 | 29 | a1i 11 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → 2 ∈ ℝ) |
181 | 179, 180 | remulcld 10761 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((⌊‘𝑥) · 2) ∈
ℝ) |
182 | | flle 13272 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ →
(⌊‘𝑥) ≤
𝑥) |
183 | 146, 182 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (⌊‘𝑥) ≤ 𝑥) |
184 | | 2pos 11831 |
. . . . . . . . . . . . . . . . 17
⊢ 0 <
2 |
185 | 29, 184 | pm3.2i 474 |
. . . . . . . . . . . . . . . 16
⊢ (2 ∈
ℝ ∧ 0 < 2) |
186 | 185 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (2 ∈ ℝ ∧ 0 <
2)) |
187 | | lemul1 11582 |
. . . . . . . . . . . . . . 15
⊢
(((⌊‘𝑥)
∈ ℝ ∧ 𝑥
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) →
((⌊‘𝑥) ≤
𝑥 ↔
((⌊‘𝑥) ·
2) ≤ (𝑥 ·
2))) |
188 | 179, 146,
186, 187 | syl3anc 1372 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((⌊‘𝑥) ≤ 𝑥 ↔ ((⌊‘𝑥) · 2) ≤ (𝑥 · 2))) |
189 | 183, 188 | mpbid 235 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((⌊‘𝑥) · 2) ≤ (𝑥 · 2)) |
190 | 181, 163,
83, 189 | leadd2dd 11345 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + ((⌊‘𝑥) · 2)) ≤
(Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2))) |
191 | 177, 190 | eqbrtrd 5062 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) ≤ (Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2))) |
192 | 161, 164,
23, 191 | lediv1dd 12584 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥)) |
193 | 105 | recnd 10759 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((log‘(𝑥 / 𝑛))↑2) + 2) ∈
ℂ) |
194 | 5, 56, 193, 61 | fsumdivc 15246 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))(((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥)) |
195 | 83 | recnd 10759 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℂ) |
196 | 56, 86 | mulcld 10751 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (𝑥 · 2) ∈ ℂ) |
197 | | divdir 11413 |
. . . . . . . . . . . 12
⊢
((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) ∈ ℂ ∧ (𝑥 · 2) ∈ ℂ
∧ (𝑥 ∈ ℂ
∧ 𝑥 ≠ 0)) →
((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥))) |
198 | 195, 196,
55, 197 | syl3anc 1372 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥))) |
199 | 86, 56, 61 | divcan3d 11511 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((𝑥 · 2) / 𝑥) = 2) |
200 | 199 | oveq2d 7198 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + ((𝑥 · 2) / 𝑥)) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) |
201 | 198, 200 | eqtrd 2774 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) + (𝑥 · 2)) / 𝑥) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) |
202 | 192, 194,
201 | 3brtr3d 5071 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((((log‘(𝑥 / 𝑛))↑2) + 2) / 𝑥) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) |
203 | 102, 107,
97, 160, 202 | letrd 10887 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) |
204 | 98, 102, 97, 103, 203 | letrd 10887 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2)) |
205 | 97 | leabsd 14876 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ ℝ+) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2) ≤ (abs‘((Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛))↑2) / 𝑥) + 2))) |
206 | 98, 97, 100, 204, 205 | letrd 10887 |
. . . . . 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 15114 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ 𝑂(1)) |
209 | 22 | selberglem1 26293 |
. . . 4
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈
𝑂(1) |
210 | | o1add 15073 |
. . . 4
⊢ (((𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∈ 𝑂(1) ∧ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥)))) ∈ 𝑂(1)) →
((𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘f + (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) ∈
𝑂(1)) |
211 | 208, 209,
210 | sylancl 589 |
. . 3
⊢ (⊤
→ ((𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((μ‘𝑛) · ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘𝑚)↑2) / 𝑥) − 𝑇))) ∘f + (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((μ‘𝑛) · 𝑇) − (2 · (log‘𝑥))))) ∈
𝑂(1)) |
212 | 81, 211 | eqeltrrd 2835 |
. 2
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1)) |
213 | 212 | mptru 1549 |
1
⊢ (𝑥 ∈ ℝ+
↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘𝑚)↑2)) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1) |