Step | Hyp | Ref
| Expression |
1 | | 1red 10720 |
. 2
⊢ (𝜑 → 1 ∈
ℝ) |
2 | | 2re 11790 |
. . . 4
⊢ 2 ∈
ℝ |
3 | | fzfid 13432 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘𝑥))
∈ Fin) |
4 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
5 | | elfznn 13027 |
. . . . . . . . 9
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
6 | 5 | nnrpd 12512 |
. . . . . . . 8
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℝ+) |
7 | | rpdivcl 12497 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 / 𝑛) ∈
ℝ+) |
8 | 4, 6, 7 | syl2an 599 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ+) |
9 | 8 | relogcld 25366 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘(𝑥 /
𝑛)) ∈
ℝ) |
10 | | simplr 769 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ+) |
11 | 9, 10 | rerpdivcld 12545 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑛)) / 𝑥) ∈ ℝ) |
12 | 3, 11 | fsumrecl 15184 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ) |
13 | | remulcl 10700 |
. . . 4
⊢ ((2
∈ ℝ ∧ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ) → (2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ) |
14 | 2, 12, 13 | sylancr 590 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2
· Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ) |
15 | | mulog2sumlem2.r |
. . . . . 6
⊢ 𝑅 = (((1 / 2) + (γ +
(abs‘𝐿))) +
Σ𝑚 ∈
(1...2)((log‘(e / 𝑚))
/ 𝑚)) |
16 | | halfre 11930 |
. . . . . . . 8
⊢ (1 / 2)
∈ ℝ |
17 | | emre 25743 |
. . . . . . . . 9
⊢ γ
∈ ℝ |
18 | | mulog2sumlem.1 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝐹 ⇝𝑟 𝐿) |
19 | | rlimcl 14950 |
. . . . . . . . . . 11
⊢ (𝐹 ⇝𝑟
𝐿 → 𝐿 ∈ ℂ) |
20 | 18, 19 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐿 ∈ ℂ) |
21 | 20 | abscld 14886 |
. . . . . . . . 9
⊢ (𝜑 → (abs‘𝐿) ∈
ℝ) |
22 | | readdcl 10698 |
. . . . . . . . 9
⊢ ((γ
∈ ℝ ∧ (abs‘𝐿) ∈ ℝ) → (γ +
(abs‘𝐿)) ∈
ℝ) |
23 | 17, 21, 22 | sylancr 590 |
. . . . . . . 8
⊢ (𝜑 → (γ +
(abs‘𝐿)) ∈
ℝ) |
24 | | readdcl 10698 |
. . . . . . . 8
⊢ (((1 / 2)
∈ ℝ ∧ (γ + (abs‘𝐿)) ∈ ℝ) → ((1 / 2) +
(γ + (abs‘𝐿)))
∈ ℝ) |
25 | 16, 23, 24 | sylancr 590 |
. . . . . . 7
⊢ (𝜑 → ((1 / 2) + (γ +
(abs‘𝐿))) ∈
ℝ) |
26 | | fzfid 13432 |
. . . . . . . 8
⊢ (𝜑 → (1...2) ∈
Fin) |
27 | | epr 15653 |
. . . . . . . . . . 11
⊢ e ∈
ℝ+ |
28 | | elfznn 13027 |
. . . . . . . . . . . . 13
⊢ (𝑚 ∈ (1...2) → 𝑚 ∈
ℕ) |
29 | 28 | adantl 485 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℕ) |
30 | 29 | nnrpd 12512 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℝ+) |
31 | | rpdivcl 12497 |
. . . . . . . . . . 11
⊢ ((e
∈ ℝ+ ∧ 𝑚 ∈ ℝ+) → (e /
𝑚) ∈
ℝ+) |
32 | 27, 30, 31 | sylancr 590 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (e / 𝑚) ∈
ℝ+) |
33 | 32 | relogcld 25366 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (log‘(e / 𝑚)) ∈
ℝ) |
34 | 33, 29 | nndivred 11770 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → ((log‘(e /
𝑚)) / 𝑚) ∈ ℝ) |
35 | 26, 34 | fsumrecl 15184 |
. . . . . . 7
⊢ (𝜑 → Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚) ∈ ℝ) |
36 | 25, 35 | readdcld 10748 |
. . . . . 6
⊢ (𝜑 → (((1 / 2) + (γ +
(abs‘𝐿))) +
Σ𝑚 ∈
(1...2)((log‘(e / 𝑚))
/ 𝑚)) ∈
ℝ) |
37 | 15, 36 | eqeltrid 2837 |
. . . . 5
⊢ (𝜑 → 𝑅 ∈ ℝ) |
38 | | remulcl 10700 |
. . . . 5
⊢ ((𝑅 ∈ ℝ ∧ 2 ∈
ℝ) → (𝑅 ·
2) ∈ ℝ) |
39 | 37, 2, 38 | sylancl 589 |
. . . 4
⊢ (𝜑 → (𝑅 · 2) ∈
ℝ) |
40 | 39 | adantr 484 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 · 2) ∈
ℝ) |
41 | 2 | a1i 11 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈
ℝ) |
42 | | rpssre 12479 |
. . . . 5
⊢
ℝ+ ⊆ ℝ |
43 | | 2cnd 11794 |
. . . . 5
⊢ (𝜑 → 2 ∈
ℂ) |
44 | | o1const 15067 |
. . . . 5
⊢
((ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ) →
(𝑥 ∈
ℝ+ ↦ 2) ∈ 𝑂(1)) |
45 | 42, 43, 44 | sylancr 590 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ 2) ∈
𝑂(1)) |
46 | | logfacrlim2 25962 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ⇝𝑟
1 |
47 | | rlimo1 15064 |
. . . . 5
⊢ ((𝑥 ∈ ℝ+
↦ Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ⇝𝑟 1 →
(𝑥 ∈
ℝ+ ↦ Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ 𝑂(1)) |
48 | 46, 47 | mp1i 13 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ 𝑂(1)) |
49 | 41, 12, 45, 48 | o1mul2 15072 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (2
· Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥))) ∈ 𝑂(1)) |
50 | 39 | recnd 10747 |
. . . 4
⊢ (𝜑 → (𝑅 · 2) ∈
ℂ) |
51 | | o1const 15067 |
. . . 4
⊢
((ℝ+ ⊆ ℝ ∧ (𝑅 · 2) ∈ ℂ) → (𝑥 ∈ ℝ+
↦ (𝑅 · 2))
∈ 𝑂(1)) |
52 | 42, 50, 51 | sylancr 590 |
. . 3
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ (𝑅 · 2)) ∈
𝑂(1)) |
53 | 14, 40, 49, 52 | o1add2 15071 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦ ((2
· Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈
𝑂(1)) |
54 | 14, 40 | readdcld 10748 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2
· Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈
ℝ) |
55 | 5 | adantl 485 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
56 | | mucl 25878 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(μ‘𝑛) ∈
ℤ) |
57 | 55, 56 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℤ) |
58 | 57 | zred 12168 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℝ) |
59 | 58, 55 | nndivred 11770 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛) /
𝑛) ∈
ℝ) |
60 | 59 | recnd 10747 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛) /
𝑛) ∈
ℂ) |
61 | | mulog2sumlem2.t |
. . . . . 6
⊢ 𝑇 = ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿)) |
62 | 9 | recnd 10747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘(𝑥 /
𝑛)) ∈
ℂ) |
63 | 62 | sqcld 13600 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑛))↑2) ∈
ℂ) |
64 | 63 | halfcld 11961 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((log‘(𝑥 /
𝑛))↑2) / 2) ∈
ℂ) |
65 | | remulcl 10700 |
. . . . . . . . . 10
⊢ ((γ
∈ ℝ ∧ (log‘(𝑥 / 𝑛)) ∈ ℝ) → (γ ·
(log‘(𝑥 / 𝑛))) ∈
ℝ) |
66 | 17, 9, 65 | sylancr 590 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (γ · (log‘(𝑥 / 𝑛))) ∈ ℝ) |
67 | 66 | recnd 10747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (γ · (log‘(𝑥 / 𝑛))) ∈ ℂ) |
68 | 20 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝐿 ∈
ℂ) |
69 | 67, 68 | subcld 11075 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((γ · (log‘(𝑥 / 𝑛))) − 𝐿) ∈ ℂ) |
70 | 64, 69 | addcld 10738 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((((log‘(𝑥 /
𝑛))↑2) / 2) +
((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ∈ ℂ) |
71 | 61, 70 | eqeltrid 2837 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑇 ∈
ℂ) |
72 | 60, 71 | mulcld 10739 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) · 𝑇) ∈
ℂ) |
73 | 3, 72 | fsumcl 15183 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) ∈ ℂ) |
74 | | relogcl 25319 |
. . . . 5
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
75 | 74 | adantl 485 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℝ) |
76 | 75 | recnd 10747 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℂ) |
77 | 73, 76 | subcld 11075 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)) ∈ ℂ) |
78 | 77 | abscld 14886 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ ℝ) |
79 | 78 | adantrr 717 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ ℝ) |
80 | 54 | adantrr 717 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → ((2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈
ℝ) |
81 | 54 | recnd 10747 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2
· Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ∈
ℂ) |
82 | 81 | abscld 14886 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈
ℝ) |
83 | 82 | adantrr 717 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (abs‘((2
· Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) ∈
ℝ) |
84 | 57 | zcnd 12169 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑛)
∈ ℂ) |
85 | | fzfid 13432 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin) |
86 | | elfznn 13027 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛))) → 𝑚 ∈
ℕ) |
87 | | nnrp 12483 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈ ℕ → 𝑚 ∈
ℝ+) |
88 | | rpdivcl 12497 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝑥 / 𝑛) ∈ ℝ+ ∧ 𝑚 ∈ ℝ+)
→ ((𝑥 / 𝑛) / 𝑚) ∈
ℝ+) |
89 | 8, 87, 88 | syl2an 599 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ ((𝑥 / 𝑛) / 𝑚) ∈
ℝ+) |
90 | 89 | relogcld 25366 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ (log‘((𝑥 /
𝑛) / 𝑚)) ∈ ℝ) |
91 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ 𝑚 ∈
ℕ) |
92 | 90, 91 | nndivred 11770 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ ((log‘((𝑥 /
𝑛) / 𝑚)) / 𝑚) ∈ ℝ) |
93 | 92 | recnd 10747 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ ((log‘((𝑥 /
𝑛) / 𝑚)) / 𝑚) ∈ ℂ) |
94 | 86, 93 | sylan2 596 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ) |
95 | 85, 94 | fsumcl 15183 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ) |
96 | 71, 95 | subcld 11075 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑇 −
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ) |
97 | 55 | nncnd 11732 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℂ) |
98 | 55 | nnne0d 11766 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ≠
0) |
99 | 84, 96, 97, 98 | div23d 11531 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛)
· (𝑇 −
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (((μ‘𝑛) / 𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) |
100 | 60, 71, 95 | subdid 11174 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) · (𝑇 − Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = ((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) |
101 | 99, 100 | eqtrd 2773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛)
· (𝑇 −
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = ((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) |
102 | 101 | sumeq2dv 15153 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = Σ𝑛 ∈ (1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) |
103 | 60, 95 | mulcld 10739 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ) |
104 | 3, 72, 103 | fsumsub 15236 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((((μ‘𝑛) / 𝑛) · 𝑇) − (((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) |
105 | 102, 104 | eqtrd 2773 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) |
106 | 105 | adantrr 717 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) |
107 | 85, 60, 94 | fsummulc2 15232 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) |
108 | 84 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ (μ‘𝑛)
∈ ℂ) |
109 | 97, 98 | jca 515 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ∈ ℂ
∧ 𝑛 ≠
0)) |
110 | 109 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ (𝑛 ∈ ℂ
∧ 𝑛 ≠
0)) |
111 | | div23 11395 |
. . . . . . . . . . . . . . . . 17
⊢
(((μ‘𝑛)
∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) / 𝑛) = (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) |
112 | | divass 11394 |
. . . . . . . . . . . . . . . . 17
⊢
(((μ‘𝑛)
∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) / 𝑛) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛))) |
113 | 111, 112 | eqtr3d 2775 |
. . . . . . . . . . . . . . . 16
⊢
(((μ‘𝑛)
∈ ℂ ∧ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛))) |
114 | 108, 93, 110, 113 | syl3anc 1372 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ (((μ‘𝑛) /
𝑛) ·
((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛))) |
115 | 90 | recnd 10747 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ (log‘((𝑥 /
𝑛) / 𝑚)) ∈ ℂ) |
116 | 91 | nnrpd 12512 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ 𝑚 ∈
ℝ+) |
117 | | rpcnne0 12490 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ ℝ+
→ (𝑚 ∈ ℂ
∧ 𝑚 ≠
0)) |
118 | 116, 117 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ (𝑚 ∈ ℂ
∧ 𝑚 ≠
0)) |
119 | | divdiv1 11429 |
. . . . . . . . . . . . . . . . . 18
⊢
(((log‘((𝑥 /
𝑛) / 𝑚)) ∈ ℂ ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) → (((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛))) |
120 | 115, 118,
110, 119 | syl3anc 1372 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ (((log‘((𝑥 /
𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘((𝑥 / 𝑛) / 𝑚)) / (𝑚 · 𝑛))) |
121 | | rpre 12480 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑥 ∈ ℝ+
→ 𝑥 ∈
ℝ) |
122 | 121 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) |
123 | 122 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ) |
124 | 123 | recnd 10747 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℂ) |
125 | 124 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ 𝑥 ∈
ℂ) |
126 | | divdiv1 11429 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑥 ∈ ℂ ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0) ∧ (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) → ((𝑥 / 𝑛) / 𝑚) = (𝑥 / (𝑛 · 𝑚))) |
127 | 125, 110,
118, 126 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ ((𝑥 / 𝑛) / 𝑚) = (𝑥 / (𝑛 · 𝑚))) |
128 | 127 | fveq2d 6678 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ (log‘((𝑥 /
𝑛) / 𝑚)) = (log‘(𝑥 / (𝑛 · 𝑚)))) |
129 | 91 | nncnd 11732 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ 𝑚 ∈
ℂ) |
130 | 97 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ 𝑛 ∈
ℂ) |
131 | 129, 130 | mulcomd 10740 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ (𝑚 · 𝑛) = (𝑛 · 𝑚)) |
132 | 128, 131 | oveq12d 7188 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ ((log‘((𝑥 /
𝑛) / 𝑚)) / (𝑚 · 𝑛)) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))) |
133 | 120, 132 | eqtrd 2773 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ (((log‘((𝑥 /
𝑛) / 𝑚)) / 𝑚) / 𝑛) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))) |
134 | 133 | oveq2d 7186 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ ((μ‘𝑛)
· (((log‘((𝑥 /
𝑛) / 𝑚)) / 𝑚) / 𝑛)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))) |
135 | 114, 134 | eqtrd 2773 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ (((μ‘𝑛) /
𝑛) ·
((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))) |
136 | 86, 135 | sylan2 596 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
(((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))) |
137 | 136 | sumeq2dv 15153 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(((μ‘𝑛) / 𝑛) · ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))) |
138 | 107, 137 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((μ‘𝑛) /
𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))) |
139 | 138 | sumeq2dv 15153 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))) |
140 | | oveq2 7178 |
. . . . . . . . . . . . . 14
⊢ (𝑘 = (𝑛 · 𝑚) → (𝑥 / 𝑘) = (𝑥 / (𝑛 · 𝑚))) |
141 | 140 | fveq2d 6678 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑛 · 𝑚) → (log‘(𝑥 / 𝑘)) = (log‘(𝑥 / (𝑛 · 𝑚)))) |
142 | | id 22 |
. . . . . . . . . . . . 13
⊢ (𝑘 = (𝑛 · 𝑚) → 𝑘 = (𝑛 · 𝑚)) |
143 | 141, 142 | oveq12d 7188 |
. . . . . . . . . . . 12
⊢ (𝑘 = (𝑛 · 𝑚) → ((log‘(𝑥 / 𝑘)) / 𝑘) = ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚))) |
144 | 143 | oveq2d 7186 |
. . . . . . . . . . 11
⊢ (𝑘 = (𝑛 · 𝑚) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = ((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))) |
145 | 4 | rpred 12514 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ) |
146 | | ssrab2 3969 |
. . . . . . . . . . . . . . . 16
⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ |
147 | | simprr 773 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) |
148 | 146, 147 | sseldi 3875 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑛 ∈ ℕ) |
149 | 148, 56 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℤ) |
150 | 149 | zred 12168 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (μ‘𝑛) ∈ ℝ) |
151 | | elfznn 13027 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈
(1...(⌊‘𝑥))
→ 𝑘 ∈
ℕ) |
152 | 151 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → 𝑘 ∈ ℕ) |
153 | 152 | nnrpd 12512 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → 𝑘 ∈ ℝ+) |
154 | | rpdivcl 12497 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑥 ∈ ℝ+
∧ 𝑘 ∈
ℝ+) → (𝑥 / 𝑘) ∈
ℝ+) |
155 | 4, 153, 154 | syl2an 599 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (𝑥 / 𝑘) ∈
ℝ+) |
156 | 155 | relogcld 25366 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → (log‘(𝑥 / 𝑘)) ∈ ℝ) |
157 | 151 | ad2antrl 728 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → 𝑘 ∈ ℕ) |
158 | 156, 157 | nndivred 11770 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((log‘(𝑥 / 𝑘)) / 𝑘) ∈ ℝ) |
159 | 150, 158 | remulcld 10749 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) ∈ ℝ) |
160 | 159 | recnd 10747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑘 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘})) → ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) ∈ ℂ) |
161 | 144, 145,
160 | dvdsflsumcom 25925 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((μ‘𝑛) · ((log‘(𝑥 / (𝑛 · 𝑚))) / (𝑛 · 𝑚)))) |
162 | 139, 161 | eqtr4d 2776 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘))) |
163 | 162 | adantrr 717 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑘 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘))) |
164 | | oveq2 7178 |
. . . . . . . . . . 11
⊢ (𝑘 = 1 → (𝑥 / 𝑘) = (𝑥 / 1)) |
165 | 164 | fveq2d 6678 |
. . . . . . . . . 10
⊢ (𝑘 = 1 → (log‘(𝑥 / 𝑘)) = (log‘(𝑥 / 1))) |
166 | | id 22 |
. . . . . . . . . 10
⊢ (𝑘 = 1 → 𝑘 = 1) |
167 | 165, 166 | oveq12d 7188 |
. . . . . . . . 9
⊢ (𝑘 = 1 → ((log‘(𝑥 / 𝑘)) / 𝑘) = ((log‘(𝑥 / 1)) / 1)) |
168 | | fzfid 13432 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(1...(⌊‘𝑥))
∈ Fin) |
169 | | fz1ssnn 13029 |
. . . . . . . . . 10
⊢
(1...(⌊‘𝑥)) ⊆ ℕ |
170 | 169 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(1...(⌊‘𝑥))
⊆ ℕ) |
171 | 122 | adantrr 717 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 𝑥 ∈
ℝ) |
172 | | simprr 773 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 1 ≤ 𝑥) |
173 | | flge1nn 13282 |
. . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℝ ∧ 1 ≤
𝑥) →
(⌊‘𝑥) ∈
ℕ) |
174 | 171, 172,
173 | syl2anc 587 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(⌊‘𝑥) ∈
ℕ) |
175 | | nnuz 12363 |
. . . . . . . . . . 11
⊢ ℕ =
(ℤ≥‘1) |
176 | 174, 175 | eleqtrdi 2843 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(⌊‘𝑥) ∈
(ℤ≥‘1)) |
177 | | eluzfz1 13005 |
. . . . . . . . . 10
⊢
((⌊‘𝑥)
∈ (ℤ≥‘1) → 1 ∈
(1...(⌊‘𝑥))) |
178 | 176, 177 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → 1 ∈
(1...(⌊‘𝑥))) |
179 | 151 | nnrpd 12512 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈
(1...(⌊‘𝑥))
→ 𝑘 ∈
ℝ+) |
180 | 4, 179, 154 | syl2an 599 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑘) ∈
ℝ+) |
181 | 180 | relogcld 25366 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ (log‘(𝑥 /
𝑘)) ∈
ℝ) |
182 | 169 | a1i 11 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘𝑥))
⊆ ℕ) |
183 | 182 | sselda 3877 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ 𝑘 ∈
ℕ) |
184 | 181, 183 | nndivred 11770 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑘)) / 𝑘) ∈ ℝ) |
185 | 184 | recnd 10747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑘)) / 𝑘) ∈ ℂ) |
186 | 185 | adantlrr 721 |
. . . . . . . . 9
⊢ (((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) ∧ 𝑘 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑘)) / 𝑘) ∈ ℂ) |
187 | 167, 168,
170, 178, 186 | musumsum 25929 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑘 ∈
(1...(⌊‘𝑥))Σ𝑛 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((μ‘𝑛) · ((log‘(𝑥 / 𝑘)) / 𝑘)) = ((log‘(𝑥 / 1)) / 1)) |
188 | 4 | rpcnd 12516 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℂ) |
189 | 188 | div1d 11486 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑥 / 1) = 𝑥) |
190 | 189 | fveq2d 6678 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘(𝑥 / 1)) =
(log‘𝑥)) |
191 | 190 | oveq1d 7185 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘(𝑥 / 1)) / 1) =
((log‘𝑥) /
1)) |
192 | 76 | div1d 11486 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) / 1) =
(log‘𝑥)) |
193 | 191, 192 | eqtrd 2773 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘(𝑥 / 1)) / 1) =
(log‘𝑥)) |
194 | 193 | adantrr 717 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
((log‘(𝑥 / 1)) / 1) =
(log‘𝑥)) |
195 | 163, 187,
194 | 3eqtrd 2777 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = (log‘𝑥)) |
196 | 195 | oveq2d 7186 |
. . . . . 6
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) |
197 | 106, 196 | eqtrd 2773 |
. . . . 5
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) |
198 | 197 | fveq2d 6678 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) = (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥)))) |
199 | | ere 15534 |
. . . . . . . . 9
⊢ e ∈
ℝ |
200 | 199 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → e ∈
ℝ) |
201 | | 1re 10719 |
. . . . . . . . 9
⊢ 1 ∈
ℝ |
202 | | 1lt2 11887 |
. . . . . . . . . 10
⊢ 1 <
2 |
203 | | egt2lt3 15651 |
. . . . . . . . . . 11
⊢ (2 < e
∧ e < 3) |
204 | 203 | simpli 487 |
. . . . . . . . . 10
⊢ 2 <
e |
205 | 201, 2, 199 | lttri 10844 |
. . . . . . . . . 10
⊢ ((1 <
2 ∧ 2 < e) → 1 < e) |
206 | 202, 204,
205 | mp2an 692 |
. . . . . . . . 9
⊢ 1 <
e |
207 | 201, 199,
206 | ltleii 10841 |
. . . . . . . 8
⊢ 1 ≤
e |
208 | 200, 207 | jctir 524 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (e ∈
ℝ ∧ 1 ≤ e)) |
209 | 37 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑅 ∈
ℝ) |
210 | 16 | a1i 11 |
. . . . . . . . . . . 12
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
211 | | 1rp 12476 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ+ |
212 | | rphalfcl 12499 |
. . . . . . . . . . . . . 14
⊢ (1 ∈
ℝ+ → (1 / 2) ∈ ℝ+) |
213 | 211, 212 | ax-mp 5 |
. . . . . . . . . . . . 13
⊢ (1 / 2)
∈ ℝ+ |
214 | | rpge0 12485 |
. . . . . . . . . . . . 13
⊢ ((1 / 2)
∈ ℝ+ → 0 ≤ (1 / 2)) |
215 | 213, 214 | mp1i 13 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ (1 /
2)) |
216 | 17 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → γ ∈
ℝ) |
217 | | 0re 10721 |
. . . . . . . . . . . . . . 15
⊢ 0 ∈
ℝ |
218 | | emgt0 25744 |
. . . . . . . . . . . . . . 15
⊢ 0 <
γ |
219 | 217, 17, 218 | ltleii 10841 |
. . . . . . . . . . . . . 14
⊢ 0 ≤
γ |
220 | 219 | a1i 11 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤
γ) |
221 | 20 | absge0d 14894 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 0 ≤ (abs‘𝐿)) |
222 | 216, 21, 220, 221 | addge0d 11294 |
. . . . . . . . . . . 12
⊢ (𝜑 → 0 ≤ (γ +
(abs‘𝐿))) |
223 | 210, 23, 215, 222 | addge0d 11294 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ ((1 / 2) + (γ
+ (abs‘𝐿)))) |
224 | | log1 25329 |
. . . . . . . . . . . . . 14
⊢
(log‘1) = 0 |
225 | 29 | nncnd 11732 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℂ) |
226 | 225 | mulid2d 10737 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (1 · 𝑚) = 𝑚) |
227 | 30 | rpred 12514 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ∈ ℝ) |
228 | 2 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 2 ∈
ℝ) |
229 | 199 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → e ∈
ℝ) |
230 | | elfzle2 13002 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈ (1...2) → 𝑚 ≤ 2) |
231 | 230 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ≤ 2) |
232 | 2, 199, 204 | ltleii 10841 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ≤
e |
233 | 232 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 2 ≤
e) |
234 | 227, 228,
229, 231, 233 | letrd 10875 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 𝑚 ≤ e) |
235 | 226, 234 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (1 · 𝑚) ≤ e) |
236 | | 1red 10720 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 1 ∈
ℝ) |
237 | 236, 229,
30 | lemuldivd 12563 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → ((1 · 𝑚) ≤ e ↔ 1 ≤ (e /
𝑚))) |
238 | 235, 237 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 1 ≤ (e / 𝑚)) |
239 | | logleb 25346 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℝ+ ∧ (e / 𝑚) ∈ ℝ+) → (1 ≤
(e / 𝑚) ↔
(log‘1) ≤ (log‘(e / 𝑚)))) |
240 | 211, 32, 239 | sylancr 590 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (1 ≤ (e / 𝑚) ↔ (log‘1) ≤
(log‘(e / 𝑚)))) |
241 | 238, 240 | mpbid 235 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (log‘1) ≤
(log‘(e / 𝑚))) |
242 | 224, 241 | eqbrtrrid 5066 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 0 ≤ (log‘(e
/ 𝑚))) |
243 | 33, 30, 242 | divge0d 12554 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → 0 ≤ ((log‘(e
/ 𝑚)) / 𝑚)) |
244 | 26, 34, 243 | fsumge0 15243 |
. . . . . . . . . . 11
⊢ (𝜑 → 0 ≤ Σ𝑚 ∈ (1...2)((log‘(e /
𝑚)) / 𝑚)) |
245 | 25, 35, 223, 244 | addge0d 11294 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (((1 / 2) +
(γ + (abs‘𝐿)))
+ Σ𝑚 ∈
(1...2)((log‘(e / 𝑚))
/ 𝑚))) |
246 | 245, 15 | breqtrrdi 5072 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ 𝑅) |
247 | 246 | adantr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 0 ≤
𝑅) |
248 | 209, 247 | jca 515 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 ∈ ℝ ∧ 0 ≤
𝑅)) |
249 | 84, 96 | mulcld 10739 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑛)
· (𝑇 −
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℂ) |
250 | | remulcl 10700 |
. . . . . . . 8
⊢ ((2
∈ ℝ ∧ ((log‘(𝑥 / 𝑛)) / 𝑥) ∈ ℝ) → (2 ·
((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ) |
251 | 2, 11, 250 | sylancr 590 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) ∈ ℝ) |
252 | 2 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 2 ∈ ℝ) |
253 | | 0le2 11818 |
. . . . . . . . 9
⊢ 0 ≤
2 |
254 | 253 | a1i 11 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ 2) |
255 | 97 | mulid2d 10737 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 · 𝑛) =
𝑛) |
256 | | fznnfl 13321 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ → (𝑛 ∈
(1...(⌊‘𝑥))
↔ (𝑛 ∈ ℕ
∧ 𝑛 ≤ 𝑥))) |
257 | 122, 256 | syl 17 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑛 ∈
(1...(⌊‘𝑥))
↔ (𝑛 ∈ ℕ
∧ 𝑛 ≤ 𝑥))) |
258 | 257 | simplbda 503 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ≤ 𝑥) |
259 | 255, 258 | eqbrtrd 5052 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 · 𝑛) ≤
𝑥) |
260 | | 1red 10720 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) |
261 | 55 | nnrpd 12512 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
262 | 260, 123,
261 | lemuldivd 12563 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 · 𝑛) ≤
𝑥 ↔ 1 ≤ (𝑥 / 𝑛))) |
263 | 259, 262 | mpbid 235 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ≤ (𝑥 / 𝑛)) |
264 | | logleb 25346 |
. . . . . . . . . . . 12
⊢ ((1
∈ ℝ+ ∧ (𝑥 / 𝑛) ∈ ℝ+) → (1 ≤
(𝑥 / 𝑛) ↔ (log‘1) ≤ (log‘(𝑥 / 𝑛)))) |
265 | 211, 8, 264 | sylancr 590 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 ≤ (𝑥 / 𝑛) ↔ (log‘1) ≤
(log‘(𝑥 / 𝑛)))) |
266 | 263, 265 | mpbid 235 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘1) ≤ (log‘(𝑥 / 𝑛))) |
267 | 224, 266 | eqbrtrrid 5066 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (log‘(𝑥
/ 𝑛))) |
268 | | rpregt0 12486 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
269 | 268 | ad2antlr 727 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ∈ ℝ
∧ 0 < 𝑥)) |
270 | | divge0 11587 |
. . . . . . . . 9
⊢
((((log‘(𝑥 /
𝑛)) ∈ ℝ ∧ 0
≤ (log‘(𝑥 / 𝑛))) ∧ (𝑥 ∈ ℝ ∧ 0 < 𝑥)) → 0 ≤
((log‘(𝑥 / 𝑛)) / 𝑥)) |
271 | 9, 267, 269, 270 | syl21anc 837 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ ((log‘(𝑥 / 𝑛)) / 𝑥)) |
272 | 252, 11, 254, 271 | mulge0d 11295 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (2 · ((log‘(𝑥 / 𝑛)) / 𝑥))) |
273 | 249 | abscld 14886 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ) |
274 | 273 | adantr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ e ≤ (𝑥 / 𝑛)) →
(abs‘((μ‘𝑛)
· (𝑇 −
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ) |
275 | 96 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ e ≤ (𝑥 / 𝑛)) → (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℂ) |
276 | 275 | abscld 14886 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ) |
277 | 261 | rpred 12514 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ) |
278 | 251, 277 | remulcld 10749 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) ∈ ℝ) |
279 | 278 | adantr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ e ≤ (𝑥 / 𝑛)) → ((2 ·
((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) ∈ ℝ) |
280 | 84, 96 | absmuld 14904 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) = ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))) |
281 | 84 | abscld 14886 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(μ‘𝑛)) ∈ ℝ) |
282 | 96 | abscld 14886 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑇
− Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ) |
283 | 96 | absge0d 14894 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘(𝑇
− Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) |
284 | | mule1 25885 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(abs‘(μ‘𝑛))
≤ 1) |
285 | 55, 284 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(μ‘𝑛)) ≤ 1) |
286 | 281, 260,
282, 283, 285 | lemul1ad 11657 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (1 · (abs‘(𝑇 − Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))))) |
287 | 282 | recnd 10747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑇
− Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℂ) |
288 | 287 | mulid2d 10737 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) = (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) |
289 | 286, 288 | breqtrd 5056 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(μ‘𝑛)) · (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) |
290 | 280, 289 | eqbrtrd 5052 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) |
291 | 290 | adantr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ e ≤ (𝑥 / 𝑛)) →
(abs‘((μ‘𝑛)
· (𝑇 −
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) |
292 | | logdivsum.1 |
. . . . . . . . . 10
⊢ 𝐹 = (𝑦 ∈ ℝ+ ↦
(Σ𝑖 ∈
(1...(⌊‘𝑦))((log‘𝑖) / 𝑖) − (((log‘𝑦)↑2) / 2))) |
293 | 18 | ad3antrrr 730 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ e ≤ (𝑥 / 𝑛)) → 𝐹 ⇝𝑟 𝐿) |
294 | 8 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ e ≤ (𝑥 / 𝑛)) → (𝑥 / 𝑛) ∈
ℝ+) |
295 | | simpr 488 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ e ≤ (𝑥 / 𝑛)) → e ≤ (𝑥 / 𝑛)) |
296 | 292, 293,
294, 295 | mulog2sumlem1 26270 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ e ≤ (𝑥 / 𝑛)) →
(abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿)))) ≤ (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)))) |
297 | 71, 95 | abssubd 14903 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑇
− Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇))) |
298 | 297 | adantr 484 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇))) |
299 | 61 | oveq2i 7181 |
. . . . . . . . . . 11
⊢
(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))) |
300 | 299 | fveq2i 6677 |
. . . . . . . . . 10
⊢
(abs‘(Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − 𝑇)) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿)))) |
301 | 298, 300 | eqtrdi 2789 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) = (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) − ((((log‘(𝑥 / 𝑛))↑2) / 2) + ((γ ·
(log‘(𝑥 / 𝑛))) − 𝐿))))) |
302 | | 2cnd 11794 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 2 ∈ ℂ) |
303 | 11 | recnd 10747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑛)) / 𝑥) ∈ ℂ) |
304 | 302, 303,
97 | mulassd 10742 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))) |
305 | | rpcnne0 12490 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℝ+
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
306 | 305 | ad2antlr 727 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) |
307 | | divdiv2 11430 |
. . . . . . . . . . . . . 14
⊢
(((log‘(𝑥 /
𝑛)) ∈ ℂ ∧
(𝑥 ∈ ℂ ∧
𝑥 ≠ 0) ∧ (𝑛 ∈ ℂ ∧ 𝑛 ≠ 0)) →
((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥)) |
308 | 62, 306, 109, 307 | syl3anc 1372 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥)) |
309 | | div23 11395 |
. . . . . . . . . . . . . 14
⊢
(((log‘(𝑥 /
𝑛)) ∈ ℂ ∧
𝑛 ∈ ℂ ∧
(𝑥 ∈ ℂ ∧
𝑥 ≠ 0)) →
(((log‘(𝑥 / 𝑛)) · 𝑛) / 𝑥) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛)) |
310 | 62, 97, 306, 309 | syl3anc 1372 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((log‘(𝑥 /
𝑛)) · 𝑛) / 𝑥) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛)) |
311 | 308, 310 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑛)) / (𝑥 / 𝑛)) = (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛)) |
312 | 311 | oveq2d 7186 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛))) = (2 · (((log‘(𝑥 / 𝑛)) / 𝑥) · 𝑛))) |
313 | 304, 312 | eqtr4d 2776 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)))) |
314 | 313 | adantr 484 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ e ≤ (𝑥 / 𝑛)) → ((2 ·
((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛) = (2 · ((log‘(𝑥 / 𝑛)) / (𝑥 / 𝑛)))) |
315 | 296, 301,
314 | 3brtr4d 5062 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ e ≤ (𝑥 / 𝑛)) → (abs‘(𝑇 − Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛)) |
316 | 274, 276,
279, 291, 315 | letrd 10875 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ e ≤ (𝑥 / 𝑛)) →
(abs‘((μ‘𝑛)
· (𝑇 −
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ ((2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) · 𝑛)) |
317 | 273 | adantr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘((μ‘𝑛)
· (𝑇 −
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ∈ ℝ) |
318 | 282 | adantr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘(𝑇 −
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ) |
319 | 37 | ad3antrrr 730 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → 𝑅 ∈
ℝ) |
320 | 290 | adantr 484 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘((μ‘𝑛)
· (𝑇 −
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ (abs‘(𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) |
321 | 71 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → 𝑇 ∈
ℂ) |
322 | 321 | abscld 14886 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘𝑇) ∈
ℝ) |
323 | 95 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℂ) |
324 | 323 | abscld 14886 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ∈ ℝ) |
325 | 322, 324 | readdcld 10748 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
((abs‘𝑇) +
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ∈ ℝ) |
326 | 321, 323 | abs2dif2d 14908 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘(𝑇 −
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ ((abs‘𝑇) + (abs‘Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) |
327 | 25 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → ((1 / 2) +
(γ + (abs‘𝐿)))
∈ ℝ) |
328 | 35 | ad3antrrr 730 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈ (1...2)((log‘(e /
𝑚)) / 𝑚) ∈ ℝ) |
329 | 61 | fveq2i 6677 |
. . . . . . . . . . . 12
⊢
(abs‘𝑇) =
(abs‘((((log‘(𝑥
/ 𝑛))↑2) / 2) +
((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) |
330 | 329, 322 | eqeltrrid 2838 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘((((log‘(𝑥
/ 𝑛))↑2) / 2) +
((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ∈ ℝ) |
331 | 64 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(((log‘(𝑥 / 𝑛))↑2) / 2) ∈
ℂ) |
332 | 331 | abscld 14886 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘(((log‘(𝑥
/ 𝑛))↑2) / 2)) ∈
ℝ) |
333 | 69 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → ((γ
· (log‘(𝑥 /
𝑛))) − 𝐿) ∈
ℂ) |
334 | 333 | abscld 14886 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ∈ ℝ) |
335 | 332, 334 | readdcld 10748 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
((abs‘(((log‘(𝑥
/ 𝑛))↑2) / 2)) +
(abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ∈ ℝ) |
336 | 331, 333 | abstrid 14906 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘((((log‘(𝑥
/ 𝑛))↑2) / 2) +
((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ≤ ((abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) + (abs‘((γ
· (log‘(𝑥 /
𝑛))) − 𝐿)))) |
337 | 16 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → (1 / 2) ∈
ℝ) |
338 | 23 | ad3antrrr 730 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → (γ +
(abs‘𝐿)) ∈
ℝ) |
339 | 9 | resqcld 13703 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑛))↑2) ∈
ℝ) |
340 | 339 | rehalfcld 11963 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((log‘(𝑥 /
𝑛))↑2) / 2) ∈
ℝ) |
341 | 9 | sqge0d 13704 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ ((log‘(𝑥 / 𝑛))↑2)) |
342 | | 2pos 11819 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 0 <
2 |
343 | 2, 342 | pm3.2i 474 |
. . . . . . . . . . . . . . . . . . 19
⊢ (2 ∈
ℝ ∧ 0 < 2) |
344 | 343 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (2 ∈ ℝ ∧ 0 < 2)) |
345 | | divge0 11587 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((log‘(𝑥 /
𝑛))↑2) ∈ ℝ
∧ 0 ≤ ((log‘(𝑥
/ 𝑛))↑2)) ∧ (2
∈ ℝ ∧ 0 < 2)) → 0 ≤ (((log‘(𝑥 / 𝑛))↑2) / 2)) |
346 | 339, 341,
344, 345 | syl21anc 837 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (((log‘(𝑥 / 𝑛))↑2) / 2)) |
347 | 340, 346 | absidd 14872 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((log‘(𝑥 / 𝑛))↑2) / 2)) = (((log‘(𝑥 / 𝑛))↑2) / 2)) |
348 | 347 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘(((log‘(𝑥
/ 𝑛))↑2) / 2)) =
(((log‘(𝑥 / 𝑛))↑2) /
2)) |
349 | 8 | rpred 12514 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ) |
350 | | ltle 10807 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ e ∈ ℝ)
→ ((𝑥 / 𝑛) < e → (𝑥 / 𝑛) ≤ e)) |
351 | 349, 199,
350 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝑥 / 𝑛) < e → (𝑥 / 𝑛) ≤ e)) |
352 | 351 | imp 410 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ≤ e) |
353 | 8 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ∈
ℝ+) |
354 | | logleb 25346 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝑥 / 𝑛) ∈ ℝ+ ∧ e ∈
ℝ+) → ((𝑥 / 𝑛) ≤ e ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘e))) |
355 | 353, 27, 354 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → ((𝑥 / 𝑛) ≤ e ↔ (log‘(𝑥 / 𝑛)) ≤ (log‘e))) |
356 | 352, 355 | mpbid 235 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(log‘(𝑥 / 𝑛)) ≤
(log‘e)) |
357 | | loge 25330 |
. . . . . . . . . . . . . . . . . . 19
⊢
(log‘e) = 1 |
358 | 356, 357 | breqtrdi 5071 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(log‘(𝑥 / 𝑛)) ≤ 1) |
359 | | 0le1 11241 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ 0 ≤
1 |
360 | 359 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ 1) |
361 | 9, 260, 267, 360 | le2sqd 13712 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((log‘(𝑥 /
𝑛)) ≤ 1 ↔
((log‘(𝑥 / 𝑛))↑2) ≤
(1↑2))) |
362 | 361 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
((log‘(𝑥 / 𝑛)) ≤ 1 ↔
((log‘(𝑥 / 𝑛))↑2) ≤
(1↑2))) |
363 | 358, 362 | mpbid 235 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
((log‘(𝑥 / 𝑛))↑2) ≤
(1↑2)) |
364 | | sq1 13650 |
. . . . . . . . . . . . . . . . 17
⊢
(1↑2) = 1 |
365 | 363, 364 | breqtrdi 5071 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
((log‘(𝑥 / 𝑛))↑2) ≤
1) |
366 | 339 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
((log‘(𝑥 / 𝑛))↑2) ∈
ℝ) |
367 | | 1red 10720 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → 1 ∈
ℝ) |
368 | 343 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → (2 ∈
ℝ ∧ 0 < 2)) |
369 | | lediv1 11583 |
. . . . . . . . . . . . . . . . 17
⊢
((((log‘(𝑥 /
𝑛))↑2) ∈ ℝ
∧ 1 ∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) →
(((log‘(𝑥 / 𝑛))↑2) ≤ 1 ↔
(((log‘(𝑥 / 𝑛))↑2) / 2) ≤ (1 /
2))) |
370 | 366, 367,
368, 369 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(((log‘(𝑥 / 𝑛))↑2) ≤ 1 ↔
(((log‘(𝑥 / 𝑛))↑2) / 2) ≤ (1 /
2))) |
371 | 365, 370 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(((log‘(𝑥 / 𝑛))↑2) / 2) ≤ (1 /
2)) |
372 | 348, 371 | eqbrtrd 5052 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘(((log‘(𝑥
/ 𝑛))↑2) / 2)) ≤ (1
/ 2)) |
373 | 68 | abscld 14886 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘𝐿) ∈
ℝ) |
374 | 66, 373 | readdcld 10748 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿)) ∈ ℝ) |
375 | 374 | adantr 484 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → ((γ
· (log‘(𝑥 /
𝑛))) + (abs‘𝐿)) ∈
ℝ) |
376 | 67 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → (γ
· (log‘(𝑥 /
𝑛))) ∈
ℂ) |
377 | 20 | ad3antrrr 730 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → 𝐿 ∈
ℂ) |
378 | 376, 377 | abs2dif2d 14908 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ≤ ((abs‘(γ ·
(log‘(𝑥 / 𝑛)))) + (abs‘𝐿))) |
379 | 17 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ γ ∈ ℝ) |
380 | 219 | a1i 11 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ γ) |
381 | 379, 9, 380, 267 | mulge0d 11295 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (γ · (log‘(𝑥 / 𝑛)))) |
382 | 66, 381 | absidd 14872 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(γ · (log‘(𝑥 / 𝑛)))) = (γ · (log‘(𝑥 / 𝑛)))) |
383 | 382 | adantr 484 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘(γ · (log‘(𝑥 / 𝑛)))) = (γ · (log‘(𝑥 / 𝑛)))) |
384 | 383 | oveq1d 7185 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
((abs‘(γ · (log‘(𝑥 / 𝑛)))) + (abs‘𝐿)) = ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿))) |
385 | 378, 384 | breqtrd 5056 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ≤ ((γ · (log‘(𝑥 / 𝑛))) + (abs‘𝐿))) |
386 | 66 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → (γ
· (log‘(𝑥 /
𝑛))) ∈
ℝ) |
387 | 17 | a1i 11 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → γ ∈
ℝ) |
388 | 377 | abscld 14886 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘𝐿) ∈
ℝ) |
389 | 9 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(log‘(𝑥 / 𝑛)) ∈
ℝ) |
390 | 387, 218 | jctir 524 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → (γ ∈
ℝ ∧ 0 < γ)) |
391 | | lemul2 11571 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((log‘(𝑥 /
𝑛)) ∈ ℝ ∧ 1
∈ ℝ ∧ (γ ∈ ℝ ∧ 0 < γ)) →
((log‘(𝑥 / 𝑛)) ≤ 1 ↔ (γ
· (log‘(𝑥 /
𝑛))) ≤ (γ ·
1))) |
392 | 389, 367,
390, 391 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
((log‘(𝑥 / 𝑛)) ≤ 1 ↔ (γ
· (log‘(𝑥 /
𝑛))) ≤ (γ ·
1))) |
393 | 358, 392 | mpbid 235 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → (γ
· (log‘(𝑥 /
𝑛))) ≤ (γ ·
1)) |
394 | 17 | recni 10733 |
. . . . . . . . . . . . . . . . . 18
⊢ γ
∈ ℂ |
395 | 394 | mulid1i 10723 |
. . . . . . . . . . . . . . . . 17
⊢ (γ
· 1) = γ |
396 | 393, 395 | breqtrdi 5071 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → (γ
· (log‘(𝑥 /
𝑛))) ≤
γ) |
397 | 386, 387,
388, 396 | leadd1dd 11332 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → ((γ
· (log‘(𝑥 /
𝑛))) + (abs‘𝐿)) ≤ (γ +
(abs‘𝐿))) |
398 | 334, 375,
338, 385, 397 | letrd 10875 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿)) ≤ (γ + (abs‘𝐿))) |
399 | 332, 334,
337, 338, 372, 398 | le2addd 11337 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
((abs‘(((log‘(𝑥
/ 𝑛))↑2) / 2)) +
(abs‘((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ≤ ((1 / 2) + (γ +
(abs‘𝐿)))) |
400 | 330, 335,
327, 336, 399 | letrd 10875 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘((((log‘(𝑥
/ 𝑛))↑2) / 2) +
((γ · (log‘(𝑥 / 𝑛))) − 𝐿))) ≤ ((1 / 2) + (γ +
(abs‘𝐿)))) |
401 | 329, 400 | eqbrtrid 5065 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘𝑇) ≤ ((1 / 2)
+ (γ + (abs‘𝐿)))) |
402 | 86, 92 | sylan2 596 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ) |
403 | 85, 402 | fsumrecl 15184 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ) |
404 | 403 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ) |
405 | 86, 90 | sylan2 596 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
(log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ) |
406 | 86, 129 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → 𝑚 ∈
ℂ) |
407 | 406 | mulid2d 10737 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → (1 ·
𝑚) = 𝑚) |
408 | | fznnfl 13321 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑥 / 𝑛) ∈ ℝ → (𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛))) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (𝑥 / 𝑛)))) |
409 | 349, 408 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛))) ↔ (𝑚 ∈ ℕ ∧ 𝑚 ≤ (𝑥 / 𝑛)))) |
410 | 409 | simplbda 503 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → 𝑚 ≤ (𝑥 / 𝑛)) |
411 | 407, 410 | eqbrtrd 5052 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → (1 ·
𝑚) ≤ (𝑥 / 𝑛)) |
412 | | 1red 10720 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → 1 ∈
ℝ) |
413 | 349 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → (𝑥 / 𝑛) ∈ ℝ) |
414 | 116 | rpregt0d 12520 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈ ℕ)
→ (𝑚 ∈ ℝ
∧ 0 < 𝑚)) |
415 | 86, 414 | sylan2 596 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → (𝑚 ∈ ℝ ∧ 0 <
𝑚)) |
416 | | lemuldiv 11598 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((1
∈ ℝ ∧ (𝑥 /
𝑛) ∈ ℝ ∧
(𝑚 ∈ ℝ ∧ 0
< 𝑚)) → ((1
· 𝑚) ≤ (𝑥 / 𝑛) ↔ 1 ≤ ((𝑥 / 𝑛) / 𝑚))) |
417 | 412, 413,
415, 416 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → ((1 ·
𝑚) ≤ (𝑥 / 𝑛) ↔ 1 ≤ ((𝑥 / 𝑛) / 𝑚))) |
418 | 411, 417 | mpbid 235 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → 1 ≤ ((𝑥 / 𝑛) / 𝑚)) |
419 | 86, 89 | sylan2 596 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → ((𝑥 / 𝑛) / 𝑚) ∈
ℝ+) |
420 | | logleb 25346 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((1
∈ ℝ+ ∧ ((𝑥 / 𝑛) / 𝑚) ∈ ℝ+) → (1 ≤
((𝑥 / 𝑛) / 𝑚) ↔ (log‘1) ≤
(log‘((𝑥 / 𝑛) / 𝑚)))) |
421 | 211, 419,
420 | sylancr 590 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → (1 ≤
((𝑥 / 𝑛) / 𝑚) ↔ (log‘1) ≤
(log‘((𝑥 / 𝑛) / 𝑚)))) |
422 | 418, 421 | mpbid 235 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → (log‘1)
≤ (log‘((𝑥 / 𝑛) / 𝑚))) |
423 | 224, 422 | eqbrtrrid 5066 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → 0 ≤
(log‘((𝑥 / 𝑛) / 𝑚))) |
424 | | divge0 11587 |
. . . . . . . . . . . . . . . 16
⊢
((((log‘((𝑥 /
𝑛) / 𝑚)) ∈ ℝ ∧ 0 ≤
(log‘((𝑥 / 𝑛) / 𝑚))) ∧ (𝑚 ∈ ℝ ∧ 0 < 𝑚)) → 0 ≤
((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) |
425 | 405, 423,
415, 424 | syl21anc 837 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → 0 ≤
((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) |
426 | 85, 402, 425 | fsumge0 15243 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) |
427 | 426 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → 0 ≤
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) |
428 | 404, 427 | absidd 14872 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) |
429 | | fzfid 13432 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(1...(⌊‘(𝑥 /
𝑛))) ∈
Fin) |
430 | 349 | flcld 13259 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (⌊‘(𝑥 /
𝑛)) ∈
ℤ) |
431 | 430 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(⌊‘(𝑥 / 𝑛)) ∈
ℤ) |
432 | | 2z 12095 |
. . . . . . . . . . . . . . . . . . 19
⊢ 2 ∈
ℤ |
433 | 432 | a1i 11 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → 2 ∈
ℤ) |
434 | 349 | adantr 484 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) ∈ ℝ) |
435 | 199 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → e ∈
ℝ) |
436 | | 3re 11796 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 3 ∈
ℝ |
437 | 436 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → 3 ∈
ℝ) |
438 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) < e) |
439 | 203 | simpri 489 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ e <
3 |
440 | 439 | a1i 11 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → e <
3) |
441 | 434, 435,
437, 438, 440 | lttrd 10879 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → (𝑥 / 𝑛) < 3) |
442 | | 3z 12096 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 3 ∈
ℤ |
443 | | fllt 13267 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ 3 ∈ ℤ)
→ ((𝑥 / 𝑛) < 3 ↔
(⌊‘(𝑥 / 𝑛)) < 3)) |
444 | 434, 442,
443 | sylancl 589 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → ((𝑥 / 𝑛) < 3 ↔ (⌊‘(𝑥 / 𝑛)) < 3)) |
445 | 441, 444 | mpbid 235 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(⌊‘(𝑥 / 𝑛)) < 3) |
446 | | df-3 11780 |
. . . . . . . . . . . . . . . . . . . 20
⊢ 3 = (2 +
1) |
447 | 445, 446 | breqtrdi 5071 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(⌊‘(𝑥 / 𝑛)) < (2 +
1)) |
448 | | zleltp1 12114 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⌊‘(𝑥
/ 𝑛)) ∈ ℤ ∧
2 ∈ ℤ) → ((⌊‘(𝑥 / 𝑛)) ≤ 2 ↔ (⌊‘(𝑥 / 𝑛)) < (2 + 1))) |
449 | 431, 432,
448 | sylancl 589 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
((⌊‘(𝑥 / 𝑛)) ≤ 2 ↔
(⌊‘(𝑥 / 𝑛)) < (2 +
1))) |
450 | 447, 449 | mpbird 260 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(⌊‘(𝑥 / 𝑛)) ≤ 2) |
451 | | eluz2 12330 |
. . . . . . . . . . . . . . . . . 18
⊢ (2 ∈
(ℤ≥‘(⌊‘(𝑥 / 𝑛))) ↔ ((⌊‘(𝑥 / 𝑛)) ∈ ℤ ∧ 2 ∈ ℤ
∧ (⌊‘(𝑥 /
𝑛)) ≤
2)) |
452 | 431, 433,
450, 451 | syl3anbrc 1344 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → 2 ∈
(ℤ≥‘(⌊‘(𝑥 / 𝑛)))) |
453 | | fzss2 13038 |
. . . . . . . . . . . . . . . . 17
⊢ (2 ∈
(ℤ≥‘(⌊‘(𝑥 / 𝑛))) → (1...(⌊‘(𝑥 / 𝑛))) ⊆ (1...2)) |
454 | 452, 453 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(1...(⌊‘(𝑥 /
𝑛))) ⊆
(1...2)) |
455 | 454 | sselda 3877 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → 𝑚 ∈
(1...2)) |
456 | 34 | ad5ant15 759 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) →
((log‘(e / 𝑚)) /
𝑚) ∈
ℝ) |
457 | 455, 456 | syldan 594 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → ((log‘(e
/ 𝑚)) / 𝑚) ∈ ℝ) |
458 | 429, 457 | fsumrecl 15184 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘(e / 𝑚)) / 𝑚) ∈ ℝ) |
459 | 92 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) →
((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ) |
460 | 86, 459 | sylan2 596 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ∈ ℝ) |
461 | 352 | adantr 484 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑥 / 𝑛) ≤ e) |
462 | 434 | adantr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑥 / 𝑛) ∈ ℝ) |
463 | 199 | a1i 11 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → e ∈
ℝ) |
464 | 30 | rpregt0d 12520 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝜑 ∧ 𝑚 ∈ (1...2)) → (𝑚 ∈ ℝ ∧ 0 < 𝑚)) |
465 | 464 | ad5ant15 759 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (𝑚 ∈ ℝ ∧ 0 <
𝑚)) |
466 | | lediv1 11583 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝑥 / 𝑛) ∈ ℝ ∧ e ∈ ℝ ∧
(𝑚 ∈ ℝ ∧ 0
< 𝑚)) → ((𝑥 / 𝑛) ≤ e ↔ ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚))) |
467 | 462, 463,
465, 466 | syl3anc 1372 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) ≤ e ↔ ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚))) |
468 | 461, 467 | mpbid 235 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚)) |
469 | 89 | adantlr 715 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) → ((𝑥 / 𝑛) / 𝑚) ∈
ℝ+) |
470 | 28, 469 | sylan2 596 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → ((𝑥 / 𝑛) / 𝑚) ∈
ℝ+) |
471 | 32 | ad5ant15 759 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (e /
𝑚) ∈
ℝ+) |
472 | 470, 471 | logled 25370 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → (((𝑥 / 𝑛) / 𝑚) ≤ (e / 𝑚) ↔ (log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚)))) |
473 | 468, 472 | mpbid 235 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) →
(log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚))) |
474 | 90 | adantlr 715 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ ℕ) →
(log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ) |
475 | 28, 474 | sylan2 596 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) →
(log‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ) |
476 | 33 | ad5ant15 759 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) →
(log‘(e / 𝑚)) ∈
ℝ) |
477 | | lediv1 11583 |
. . . . . . . . . . . . . . . . 17
⊢
(((log‘((𝑥 /
𝑛) / 𝑚)) ∈ ℝ ∧ (log‘(e / 𝑚)) ∈ ℝ ∧ (𝑚 ∈ ℝ ∧ 0 <
𝑚)) →
((log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚)) ↔ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚))) |
478 | 475, 476,
465, 477 | syl3anc 1372 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) →
((log‘((𝑥 / 𝑛) / 𝑚)) ≤ (log‘(e / 𝑚)) ↔ ((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚))) |
479 | 473, 478 | mpbid 235 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) →
((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚)) |
480 | 455, 479 | syldan 594 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ ((log‘(e / 𝑚)) / 𝑚)) |
481 | 429, 460,
457, 480 | fsumle 15247 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘(e / 𝑚)) / 𝑚)) |
482 | | fzfid 13432 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → (1...2) ∈
Fin) |
483 | 243 | ad5ant15 759 |
. . . . . . . . . . . . . 14
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) ∧ 𝑚 ∈ (1...2)) → 0 ≤
((log‘(e / 𝑚)) /
𝑚)) |
484 | 482, 456,
483, 454 | fsumless 15244 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘(e / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)) |
485 | 404, 458,
328, 481, 484 | letrd 10875 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚) ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)) |
486 | 428, 485 | eqbrtrd 5052 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)) ≤ Σ𝑚 ∈ (1...2)((log‘(e / 𝑚)) / 𝑚)) |
487 | 322, 324,
327, 328, 401, 486 | le2addd 11337 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
((abs‘𝑇) +
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ (((1 / 2) + (γ +
(abs‘𝐿))) +
Σ𝑚 ∈
(1...2)((log‘(e / 𝑚))
/ 𝑚))) |
488 | 487, 15 | breqtrrdi 5072 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
((abs‘𝑇) +
(abs‘Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ 𝑅) |
489 | 318, 325,
319, 326, 488 | letrd 10875 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘(𝑇 −
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) ≤ 𝑅) |
490 | 317, 318,
319, 320, 489 | letrd 10875 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ (𝑥 / 𝑛) < e) →
(abs‘((μ‘𝑛)
· (𝑇 −
Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚)))) ≤ 𝑅) |
491 | 4, 208, 248, 249, 251, 272, 316, 490 | fsumharmonic 25749 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · ((log‘e) +
1)))) |
492 | | 2cnd 11794 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 ∈
ℂ) |
493 | 3, 492, 303 | fsummulc2 15232 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (2
· Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥))) |
494 | | df-2 11779 |
. . . . . . . . . 10
⊢ 2 = (1 +
1) |
495 | 357 | oveq1i 7180 |
. . . . . . . . . 10
⊢
((log‘e) + 1) = (1 + 1) |
496 | 494, 495 | eqtr4i 2764 |
. . . . . . . . 9
⊢ 2 =
((log‘e) + 1) |
497 | 496 | a1i 11 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 2 =
((log‘e) + 1)) |
498 | 497 | oveq2d 7186 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝑅 · 2) = (𝑅 · ((log‘e) +
1))) |
499 | 493, 498 | oveq12d 7188 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2
· Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(2 · ((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · ((log‘e) +
1)))) |
500 | 491, 499 | breqtrrd 5058 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) ≤ ((2 · Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) |
501 | 500 | adantrr 717 |
. . . 4
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) · (𝑇 − Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((log‘((𝑥 / 𝑛) / 𝑚)) / 𝑚))) / 𝑛)) ≤ ((2 · Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) |
502 | 198, 501 | eqbrtrrd 5054 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ≤ ((2 · Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2))) |
503 | 54 | leabsd 14864 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((2
· Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ≤ (abs‘((2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)))) |
504 | 503 | adantrr 717 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) → ((2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)) ≤ (abs‘((2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)))) |
505 | 79, 80, 83, 502, 504 | letrd 10875 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ≤ (abs‘((2 · Σ𝑛 ∈
(1...(⌊‘𝑥))((log‘(𝑥 / 𝑛)) / 𝑥)) + (𝑅 · 2)))) |
506 | 1, 53, 54, 77, 505 | o1le 15102 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))(((μ‘𝑛) / 𝑛) · 𝑇) − (log‘𝑥))) ∈ 𝑂(1)) |