Proof of Theorem dchrvmasumlem3
Step | Hyp | Ref
| Expression |
1 | | 1red 9934 |
. 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 24987 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ 𝑂(1)) |
18 | | fzfid 12634 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘𝑥))
∈ Fin) |
19 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
20 | | elfznn 12241 |
. . . . . . . . 9
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℕ) |
21 | 20 | nnrpd 11746 |
. . . . . . . 8
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℝ+) |
22 | | rpdivcl 11732 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
ℝ+) → (𝑥 / 𝑑) ∈
ℝ+) |
23 | 19, 21, 22 | syl2an 493 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑑) ∈
ℝ+) |
24 | 10 | ralrimiva 2949 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑚 ∈ ℝ+ 𝐹 ∈ ℂ) |
25 | 24 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ∀𝑚 ∈
ℝ+ 𝐹
∈ ℂ) |
26 | 11 | eleq1d 2672 |
. . . . . . . 8
⊢ (𝑚 = (𝑥 / 𝑑) → (𝐹 ∈ ℂ ↔ 𝐾 ∈ ℂ)) |
27 | 26 | rspcv 3278 |
. . . . . . 7
⊢ ((𝑥 / 𝑑) ∈ ℝ+ →
(∀𝑚 ∈
ℝ+ 𝐹
∈ ℂ → 𝐾
∈ ℂ)) |
28 | 23, 25, 27 | sylc 63 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝐾 ∈
ℂ) |
29 | 13 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑇 ∈
ℂ) |
30 | 28, 29 | subcld 10271 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐾 − 𝑇) ∈
ℂ) |
31 | 30 | abscld 14023 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝐾
− 𝑇)) ∈
ℝ) |
32 | 20 | adantl 481 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℕ) |
33 | 31, 32 | nndivred 10946 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝐾
− 𝑇)) / 𝑑) ∈
ℝ) |
34 | 18, 33 | fsumrecl 14312 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℝ) |
35 | 8 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑋 ∈ 𝐷) |
36 | | elfzelz 12213 |
. . . . . . 7
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℤ) |
37 | 36 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℤ) |
38 | 5, 2, 6, 3, 35, 37 | dchrzrhcl 24770 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑋‘(𝐿‘𝑑)) ∈ ℂ) |
39 | | mucl 24667 |
. . . . . . . . 9
⊢ (𝑑 ∈ ℕ →
(μ‘𝑑) ∈
ℤ) |
40 | 32, 39 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑑)
∈ ℤ) |
41 | 40 | zred 11358 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑑)
∈ ℝ) |
42 | 41, 32 | nndivred 10946 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑑) /
𝑑) ∈
ℝ) |
43 | 42 | recnd 9947 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑑) /
𝑑) ∈
ℂ) |
44 | 38, 43 | mulcld 9939 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) ∈ ℂ) |
45 | 44, 30 | mulcld 9939 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇)) ∈ ℂ) |
46 | 18, 45 | fsumcl 14311 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇)) ∈ ℂ) |
47 | 46 | abscld 14023 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ ℝ) |
48 | 34 | recnd 9947 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℂ) |
49 | 48 | abscld 14023 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ ℝ) |
50 | 45 | abscld 14023 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ ℝ) |
51 | 18, 50 | fsumrecl 14312 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ ℝ) |
52 | 18, 45 | fsumabs 14374 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇)))) |
53 | 44 | abscld 14023 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) ∈ ℝ) |
54 | 32 | nnrecred 10943 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑑) ∈
ℝ) |
55 | 30 | absge0d 14031 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘(𝐾
− 𝑇))) |
56 | 38, 43 | absmuld 14041 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) = ((abs‘(𝑋‘(𝐿‘𝑑))) · (abs‘((μ‘𝑑) / 𝑑)))) |
57 | 38 | abscld 14023 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑋‘(𝐿‘𝑑))) ∈ ℝ) |
58 | | 1red 9934 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) |
59 | 43 | abscld 14023 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((μ‘𝑑) / 𝑑)) ∈ ℝ) |
60 | 38 | absge0d 14031 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘(𝑋‘(𝐿‘𝑑)))) |
61 | 43 | absge0d 14031 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘((μ‘𝑑) / 𝑑))) |
62 | | eqid 2610 |
. . . . . . . . . . . 12
⊢
(Base‘𝑍) =
(Base‘𝑍) |
63 | 4 | nnnn0d 11228 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
64 | 2, 62, 3 | znzrhfo 19715 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→(Base‘𝑍)) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐿:ℤ–onto→(Base‘𝑍)) |
66 | | fof 6028 |
. . . . . . . . . . . . . . 15
⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍)) |
67 | 65, 66 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍)) |
68 | 67 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝐿:ℤ⟶(Base‘𝑍)) |
69 | 68, 37 | ffvelrnd 6268 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐿‘𝑑) ∈ (Base‘𝑍)) |
70 | 5, 6, 2, 62, 35, 69 | dchrabs2 24787 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑋‘(𝐿‘𝑑))) ≤ 1) |
71 | 41 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑑)
∈ ℂ) |
72 | 32 | nncnd 10913 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℂ) |
73 | 32 | nnne0d 10942 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ≠
0) |
74 | 71, 72, 73 | absdivd 14042 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((μ‘𝑑) / 𝑑)) = ((abs‘(μ‘𝑑)) / (abs‘𝑑))) |
75 | 32 | nnrpd 11746 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℝ+) |
76 | 75 | rprege0d 11755 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑑 ∈ ℝ
∧ 0 ≤ 𝑑)) |
77 | | absid 13884 |
. . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ ℝ ∧ 0 ≤
𝑑) → (abs‘𝑑) = 𝑑) |
78 | 76, 77 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘𝑑) =
𝑑) |
79 | 78 | oveq2d 6565 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(μ‘𝑑)) / (abs‘𝑑)) = ((abs‘(μ‘𝑑)) / 𝑑)) |
80 | 74, 79 | eqtrd 2644 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((μ‘𝑑) / 𝑑)) = ((abs‘(μ‘𝑑)) / 𝑑)) |
81 | 71 | abscld 14023 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(μ‘𝑑)) ∈ ℝ) |
82 | | mule1 24674 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ ℕ →
(abs‘(μ‘𝑑))
≤ 1) |
83 | 32, 82 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(μ‘𝑑)) ≤ 1) |
84 | 81, 58, 75, 83 | lediv1dd 11806 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(μ‘𝑑)) / 𝑑) ≤ (1 / 𝑑)) |
85 | 80, 84 | eqbrtrd 4605 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((μ‘𝑑) / 𝑑)) ≤ (1 / 𝑑)) |
86 | 57, 58, 59, 54, 60, 61, 70, 85 | lemul12ad 10845 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑋‘(𝐿‘𝑑))) · (abs‘((μ‘𝑑) / 𝑑))) ≤ (1 · (1 / 𝑑))) |
87 | 54 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑑) ∈
ℂ) |
88 | 87 | mulid2d 9937 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1 · (1 / 𝑑))
= (1 / 𝑑)) |
89 | 86, 88 | breqtrd 4609 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑋‘(𝐿‘𝑑))) · (abs‘((μ‘𝑑) / 𝑑))) ≤ (1 / 𝑑)) |
90 | 56, 89 | eqbrtrd 4605 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) ≤ (1 / 𝑑)) |
91 | 53, 54, 31, 55, 90 | lemul1ad 10842 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) · (abs‘(𝐾 − 𝑇))) ≤ ((1 / 𝑑) · (abs‘(𝐾 − 𝑇)))) |
92 | 44, 30 | absmuld 14041 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) = ((abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) · (abs‘(𝐾 − 𝑇)))) |
93 | 31 | recnd 9947 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝐾
− 𝑇)) ∈
ℂ) |
94 | 93, 72, 73 | divrec2d 10684 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝐾
− 𝑇)) / 𝑑) = ((1 / 𝑑) · (abs‘(𝐾 − 𝑇)))) |
95 | 91, 92, 94 | 3brtr4d 4615 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ ((abs‘(𝐾 − 𝑇)) / 𝑑)) |
96 | 18, 50, 33, 95 | fsumle 14372 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) |
97 | 47, 51, 34, 52, 96 | letrd 10073 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) |
98 | 34 | leabsd 14001 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ≤ (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))) |
99 | 47, 34, 49, 97, 98 | letrd 10073 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ (abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))) |
100 | 99 | adantrr 749 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ (abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))) |
101 | 1, 17, 34, 46, 100 | o1le 14231 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ 𝑂(1)) |