Proof of Theorem dchrvmasumlem3
Step | Hyp | Ref
| Expression |
1 | | 1red 10976 |
. 2
⊢ (𝜑 → 1 ∈
ℝ) |
2 | | rpvmasum.z |
. . 3
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
3 | | rpvmasum.l |
. . 3
⊢ 𝐿 = (ℤRHom‘𝑍) |
4 | | rpvmasum.a |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℕ) |
5 | | rpvmasum.g |
. . 3
⊢ 𝐺 = (DChr‘𝑁) |
6 | | rpvmasum.d |
. . 3
⊢ 𝐷 = (Base‘𝐺) |
7 | | rpvmasum.1 |
. . 3
⊢ 1 =
(0g‘𝐺) |
8 | | dchrisum.b |
. . 3
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
9 | | dchrisum.n1 |
. . 3
⊢ (𝜑 → 𝑋 ≠ 1 ) |
10 | | dchrvmasum.f |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝐹 ∈
ℂ) |
11 | | dchrvmasum.g |
. . 3
⊢ (𝑚 = (𝑥 / 𝑑) → 𝐹 = 𝐾) |
12 | | dchrvmasum.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) |
13 | | dchrvmasum.t |
. . 3
⊢ (𝜑 → 𝑇 ∈ ℂ) |
14 | | dchrvmasum.1 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
(abs‘(𝐹 − 𝑇)) ≤ (𝐶 · ((log‘𝑚) / 𝑚))) |
15 | | dchrvmasum.r |
. . 3
⊢ (𝜑 → 𝑅 ∈ ℝ) |
16 | | dchrvmasum.2 |
. . 3
⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(𝐹 − 𝑇)) ≤ 𝑅) |
17 | 2, 3, 4, 5, 6, 7, 8, 9, 10, 11, 12, 13, 14, 15, 16 | dchrvmasumlem2 26646 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ 𝑂(1)) |
18 | | fzfid 13693 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘𝑥))
∈ Fin) |
19 | 11 | eleq1d 2823 |
. . . . . . 7
⊢ (𝑚 = (𝑥 / 𝑑) → (𝐹 ∈ ℂ ↔ 𝐾 ∈ ℂ)) |
20 | 10 | ralrimiva 3103 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑚 ∈ ℝ+ 𝐹 ∈ ℂ) |
21 | 20 | ad2antrr 723 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ∀𝑚 ∈
ℝ+ 𝐹
∈ ℂ) |
22 | | simpr 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
23 | | elfznn 13285 |
. . . . . . . . 9
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℕ) |
24 | 23 | nnrpd 12770 |
. . . . . . . 8
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℝ+) |
25 | | rpdivcl 12755 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
ℝ+) → (𝑥 / 𝑑) ∈
ℝ+) |
26 | 22, 24, 25 | syl2an 596 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑑) ∈
ℝ+) |
27 | 19, 21, 26 | rspcdva 3562 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝐾 ∈
ℂ) |
28 | 13 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑇 ∈
ℂ) |
29 | 27, 28 | subcld 11332 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐾 − 𝑇) ∈
ℂ) |
30 | 29 | abscld 15148 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝐾
− 𝑇)) ∈
ℝ) |
31 | 23 | adantl 482 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℕ) |
32 | 30, 31 | nndivred 12027 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝐾
− 𝑇)) / 𝑑) ∈
ℝ) |
33 | 18, 32 | fsumrecl 15446 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℝ) |
34 | 8 | ad2antrr 723 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑋 ∈ 𝐷) |
35 | | elfzelz 13256 |
. . . . . . 7
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℤ) |
36 | 35 | adantl 482 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℤ) |
37 | 5, 2, 6, 3, 34, 36 | dchrzrhcl 26393 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑋‘(𝐿‘𝑑)) ∈ ℂ) |
38 | | mucl 26290 |
. . . . . . . . 9
⊢ (𝑑 ∈ ℕ →
(μ‘𝑑) ∈
ℤ) |
39 | 31, 38 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑑)
∈ ℤ) |
40 | 39 | zred 12426 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑑)
∈ ℝ) |
41 | 40, 31 | nndivred 12027 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑑) /
𝑑) ∈
ℝ) |
42 | 41 | recnd 11003 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑑) /
𝑑) ∈
ℂ) |
43 | 37, 42 | mulcld 10995 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) ∈ ℂ) |
44 | 43, 29 | mulcld 10995 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇)) ∈ ℂ) |
45 | 18, 44 | fsumcl 15445 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇)) ∈ ℂ) |
46 | 45 | abscld 15148 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ ℝ) |
47 | 33 | recnd 11003 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℂ) |
48 | 47 | abscld 15148 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ ℝ) |
49 | 44 | abscld 15148 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ ℝ) |
50 | 18, 49 | fsumrecl 15446 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ ℝ) |
51 | 18, 44 | fsumabs 15513 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇)))) |
52 | 43 | abscld 15148 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) ∈ ℝ) |
53 | 31 | nnrecred 12024 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑑) ∈
ℝ) |
54 | 29 | absge0d 15156 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘(𝐾
− 𝑇))) |
55 | 37, 42 | absmuld 15166 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) = ((abs‘(𝑋‘(𝐿‘𝑑))) · (abs‘((μ‘𝑑) / 𝑑)))) |
56 | 37 | abscld 15148 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑋‘(𝐿‘𝑑))) ∈ ℝ) |
57 | | 1red 10976 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) |
58 | 42 | abscld 15148 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((μ‘𝑑) / 𝑑)) ∈ ℝ) |
59 | 37 | absge0d 15156 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘(𝑋‘(𝐿‘𝑑)))) |
60 | 42 | absge0d 15156 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘((μ‘𝑑) / 𝑑))) |
61 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(Base‘𝑍) =
(Base‘𝑍) |
62 | 4 | nnnn0d 12293 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
63 | 2, 61, 3 | znzrhfo 20755 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→(Base‘𝑍)) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐿:ℤ–onto→(Base‘𝑍)) |
65 | | fof 6688 |
. . . . . . . . . . . . . . 15
⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍)) |
67 | 66 | ad2antrr 723 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝐿:ℤ⟶(Base‘𝑍)) |
68 | 67, 36 | ffvelrnd 6962 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐿‘𝑑) ∈ (Base‘𝑍)) |
69 | 5, 6, 2, 61, 34, 68 | dchrabs2 26410 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑋‘(𝐿‘𝑑))) ≤ 1) |
70 | 40 | recnd 11003 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑑)
∈ ℂ) |
71 | 31 | nncnd 11989 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℂ) |
72 | 31 | nnne0d 12023 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ≠
0) |
73 | 70, 71, 72 | absdivd 15167 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((μ‘𝑑) / 𝑑)) = ((abs‘(μ‘𝑑)) / (abs‘𝑑))) |
74 | 31 | nnrpd 12770 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℝ+) |
75 | 74 | rprege0d 12779 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑑 ∈ ℝ
∧ 0 ≤ 𝑑)) |
76 | | absid 15008 |
. . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ ℝ ∧ 0 ≤
𝑑) → (abs‘𝑑) = 𝑑) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘𝑑) =
𝑑) |
78 | 77 | oveq2d 7291 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(μ‘𝑑)) / (abs‘𝑑)) = ((abs‘(μ‘𝑑)) / 𝑑)) |
79 | 73, 78 | eqtrd 2778 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((μ‘𝑑) / 𝑑)) = ((abs‘(μ‘𝑑)) / 𝑑)) |
80 | 70 | abscld 15148 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(μ‘𝑑)) ∈ ℝ) |
81 | | mule1 26297 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ ℕ →
(abs‘(μ‘𝑑))
≤ 1) |
82 | 31, 81 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(μ‘𝑑)) ≤ 1) |
83 | 80, 57, 74, 82 | lediv1dd 12830 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(μ‘𝑑)) / 𝑑) ≤ (1 / 𝑑)) |
84 | 79, 83 | eqbrtrd 5096 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((μ‘𝑑) / 𝑑)) ≤ (1 / 𝑑)) |
85 | 56, 57, 58, 53, 59, 60, 69, 84 | lemul12ad 11917 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑋‘(𝐿‘𝑑))) · (abs‘((μ‘𝑑) / 𝑑))) ≤ (1 · (1 / 𝑑))) |
86 | 53 | recnd 11003 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑑) ∈
ℂ) |
87 | 86 | mulid2d 10993 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1 · (1 / 𝑑))
= (1 / 𝑑)) |
88 | 85, 87 | breqtrd 5100 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑋‘(𝐿‘𝑑))) · (abs‘((μ‘𝑑) / 𝑑))) ≤ (1 / 𝑑)) |
89 | 55, 88 | eqbrtrd 5096 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) ≤ (1 / 𝑑)) |
90 | 52, 53, 30, 54, 89 | lemul1ad 11914 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) · (abs‘(𝐾 − 𝑇))) ≤ ((1 / 𝑑) · (abs‘(𝐾 − 𝑇)))) |
91 | 43, 29 | absmuld 15166 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) = ((abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) · (abs‘(𝐾 − 𝑇)))) |
92 | 30 | recnd 11003 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝐾
− 𝑇)) ∈
ℂ) |
93 | 92, 71, 72 | divrec2d 11755 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝐾
− 𝑇)) / 𝑑) = ((1 / 𝑑) · (abs‘(𝐾 − 𝑇)))) |
94 | 90, 91, 93 | 3brtr4d 5106 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ ((abs‘(𝐾 − 𝑇)) / 𝑑)) |
95 | 18, 49, 32, 94 | fsumle 15511 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) |
96 | 46, 50, 33, 51, 95 | letrd 11132 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) |
97 | 33 | leabsd 15126 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ≤ (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))) |
98 | 46, 33, 48, 96, 97 | letrd 11132 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ (abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))) |
99 | 98 | adantrr 714 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ (abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))) |
100 | 1, 17, 33, 45, 99 | o1le 15364 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ 𝑂(1)) |