Proof of Theorem dchrvmasumlem3
Step | Hyp | Ref
| Expression |
1 | | 1red 10713 |
. 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 26226 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ 𝑂(1)) |
18 | | fzfid 13425 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘𝑥))
∈ Fin) |
19 | 11 | eleq1d 2817 |
. . . . . . 7
⊢ (𝑚 = (𝑥 / 𝑑) → (𝐹 ∈ ℂ ↔ 𝐾 ∈ ℂ)) |
20 | 10 | ralrimiva 3096 |
. . . . . . . 8
⊢ (𝜑 → ∀𝑚 ∈ ℝ+ 𝐹 ∈ ℂ) |
21 | 20 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ∀𝑚 ∈
ℝ+ 𝐹
∈ ℂ) |
22 | | simpr 488 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑥 ∈
ℝ+) |
23 | | elfznn 13020 |
. . . . . . . . 9
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℕ) |
24 | 23 | nnrpd 12505 |
. . . . . . . 8
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℝ+) |
25 | | rpdivcl 12490 |
. . . . . . . 8
⊢ ((𝑥 ∈ ℝ+
∧ 𝑑 ∈
ℝ+) → (𝑥 / 𝑑) ∈
ℝ+) |
26 | 22, 24, 25 | syl2an 599 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑑) ∈
ℝ+) |
27 | 19, 21, 26 | rspcdva 3526 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝐾 ∈
ℂ) |
28 | 13 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑇 ∈
ℂ) |
29 | 27, 28 | subcld 11068 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐾 − 𝑇) ∈
ℂ) |
30 | 29 | abscld 14879 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝐾
− 𝑇)) ∈
ℝ) |
31 | 23 | adantl 485 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℕ) |
32 | 30, 31 | nndivred 11763 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝐾
− 𝑇)) / 𝑑) ∈
ℝ) |
33 | 18, 32 | fsumrecl 15177 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℝ) |
34 | 8 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑋 ∈ 𝐷) |
35 | | elfzelz 12991 |
. . . . . . 7
⊢ (𝑑 ∈
(1...(⌊‘𝑥))
→ 𝑑 ∈
ℤ) |
36 | 35 | adantl 485 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℤ) |
37 | 5, 2, 6, 3, 34, 36 | dchrzrhcl 25973 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑋‘(𝐿‘𝑑)) ∈ ℂ) |
38 | | mucl 25870 |
. . . . . . . . 9
⊢ (𝑑 ∈ ℕ →
(μ‘𝑑) ∈
ℤ) |
39 | 31, 38 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑑)
∈ ℤ) |
40 | 39 | zred 12161 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑑)
∈ ℝ) |
41 | 40, 31 | nndivred 11763 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑑) /
𝑑) ∈
ℝ) |
42 | 41 | recnd 10740 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((μ‘𝑑) /
𝑑) ∈
ℂ) |
43 | 37, 42 | mulcld 10732 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) ∈ ℂ) |
44 | 43, 29 | mulcld 10732 |
. . 3
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇)) ∈ ℂ) |
45 | 18, 44 | fsumcl 15176 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇)) ∈ ℂ) |
46 | 45 | abscld 14879 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ ℝ) |
47 | 33 | recnd 10740 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ∈ ℂ) |
48 | 47 | abscld 14879 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) ∈ ℝ) |
49 | 44 | abscld 14879 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ ℝ) |
50 | 18, 49 | fsumrecl 15177 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ ℝ) |
51 | 18, 44 | fsumabs 15242 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇)))) |
52 | 43 | abscld 14879 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) ∈ ℝ) |
53 | 31 | nnrecred 11760 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑑) ∈
ℝ) |
54 | 29 | absge0d 14887 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘(𝐾
− 𝑇))) |
55 | 37, 42 | absmuld 14897 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) = ((abs‘(𝑋‘(𝐿‘𝑑))) · (abs‘((μ‘𝑑) / 𝑑)))) |
56 | 37 | abscld 14879 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑋‘(𝐿‘𝑑))) ∈ ℝ) |
57 | | 1red 10713 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) |
58 | 42 | abscld 14879 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((μ‘𝑑) / 𝑑)) ∈ ℝ) |
59 | 37 | absge0d 14887 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘(𝑋‘(𝐿‘𝑑)))) |
60 | 42 | absge0d 14887 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (abs‘((μ‘𝑑) / 𝑑))) |
61 | | eqid 2738 |
. . . . . . . . . . . 12
⊢
(Base‘𝑍) =
(Base‘𝑍) |
62 | 4 | nnnn0d 12029 |
. . . . . . . . . . . . . . . 16
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
63 | 2, 61, 3 | znzrhfo 20359 |
. . . . . . . . . . . . . . . 16
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→(Base‘𝑍)) |
64 | 62, 63 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝐿:ℤ–onto→(Base‘𝑍)) |
65 | | fof 6586 |
. . . . . . . . . . . . . . 15
⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍)) |
66 | 64, 65 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍)) |
67 | 66 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝐿:ℤ⟶(Base‘𝑍)) |
68 | 67, 36 | ffvelrnd 6856 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝐿‘𝑑) ∈ (Base‘𝑍)) |
69 | 5, 6, 2, 61, 34, 68 | dchrabs2 25990 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑋‘(𝐿‘𝑑))) ≤ 1) |
70 | 40 | recnd 10740 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (μ‘𝑑)
∈ ℂ) |
71 | 31 | nncnd 11725 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℂ) |
72 | 31 | nnne0d 11759 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ≠
0) |
73 | 70, 71, 72 | absdivd 14898 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((μ‘𝑑) / 𝑑)) = ((abs‘(μ‘𝑑)) / (abs‘𝑑))) |
74 | 31 | nnrpd 12505 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ 𝑑 ∈
ℝ+) |
75 | 74 | rprege0d 12514 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (𝑑 ∈ ℝ
∧ 0 ≤ 𝑑)) |
76 | | absid 14739 |
. . . . . . . . . . . . . . 15
⊢ ((𝑑 ∈ ℝ ∧ 0 ≤
𝑑) → (abs‘𝑑) = 𝑑) |
77 | 75, 76 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘𝑑) =
𝑑) |
78 | 77 | oveq2d 7180 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(μ‘𝑑)) / (abs‘𝑑)) = ((abs‘(μ‘𝑑)) / 𝑑)) |
79 | 73, 78 | eqtrd 2773 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((μ‘𝑑) / 𝑑)) = ((abs‘(μ‘𝑑)) / 𝑑)) |
80 | 70 | abscld 14879 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(μ‘𝑑)) ∈ ℝ) |
81 | | mule1 25877 |
. . . . . . . . . . . . . 14
⊢ (𝑑 ∈ ℕ →
(abs‘(μ‘𝑑))
≤ 1) |
82 | 31, 81 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(μ‘𝑑)) ≤ 1) |
83 | 80, 57, 74, 82 | lediv1dd 12565 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(μ‘𝑑)) / 𝑑) ≤ (1 / 𝑑)) |
84 | 79, 83 | eqbrtrd 5049 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((μ‘𝑑) / 𝑑)) ≤ (1 / 𝑑)) |
85 | 56, 57, 58, 53, 59, 60, 69, 84 | lemul12ad 11653 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑋‘(𝐿‘𝑑))) · (abs‘((μ‘𝑑) / 𝑑))) ≤ (1 · (1 / 𝑑))) |
86 | 53 | recnd 10740 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1 / 𝑑) ∈
ℂ) |
87 | 86 | mulid2d 10730 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (1 · (1 / 𝑑))
= (1 / 𝑑)) |
88 | 85, 87 | breqtrd 5053 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝑋‘(𝐿‘𝑑))) · (abs‘((μ‘𝑑) / 𝑑))) ≤ (1 / 𝑑)) |
89 | 55, 88 | eqbrtrd 5049 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) ≤ (1 / 𝑑)) |
90 | 52, 53, 30, 54, 89 | lemul1ad 11650 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) · (abs‘(𝐾 − 𝑇))) ≤ ((1 / 𝑑) · (abs‘(𝐾 − 𝑇)))) |
91 | 43, 29 | absmuld 14897 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) = ((abs‘((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑))) · (abs‘(𝐾 − 𝑇)))) |
92 | 30 | recnd 10740 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝐾
− 𝑇)) ∈
ℂ) |
93 | 92, 71, 72 | divrec2d 11491 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(𝐾
− 𝑇)) / 𝑑) = ((1 / 𝑑) · (abs‘(𝐾 − 𝑇)))) |
94 | 90, 91, 93 | 3brtr4d 5059 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑑 ∈
(1...(⌊‘𝑥)))
→ (abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ ((abs‘(𝐾 − 𝑇)) / 𝑑)) |
95 | 18, 49, 32, 94 | fsumle 15240 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))(abs‘(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) |
96 | 46, 50, 33, 51, 95 | letrd 10868 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑)) |
97 | 33 | leabsd 14857 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑) ≤ (abs‘Σ𝑑 ∈ (1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))) |
98 | 46, 33, 48, 96, 97 | letrd 10868 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ (abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))) |
99 | 98 | adantrr 717 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 1 ≤
𝑥)) →
(abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ≤ (abs‘Σ𝑑 ∈
(1...(⌊‘𝑥))((abs‘(𝐾 − 𝑇)) / 𝑑))) |
100 | 1, 17, 33, 45, 99 | o1le 15095 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (𝐾 − 𝑇))) ∈ 𝑂(1)) |