Step | Hyp | Ref
| Expression |
1 | | rpvmasum.z |
. 2
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
2 | | rpvmasum.l |
. 2
⊢ 𝐿 = (ℤRHom‘𝑍) |
3 | | rpvmasum.a |
. 2
⊢ (𝜑 → 𝑁 ∈ ℕ) |
4 | | rpvmasum.g |
. 2
⊢ 𝐺 = (DChr‘𝑁) |
5 | | rpvmasum.d |
. 2
⊢ 𝐷 = (Base‘𝐺) |
6 | | rpvmasum.1 |
. 2
⊢ 1 =
(0g‘𝐺) |
7 | | dchrisum.b |
. 2
⊢ (𝜑 → 𝑋 ∈ 𝐷) |
8 | | dchrisum.n1 |
. 2
⊢ (𝜑 → 𝑋 ≠ 1 ) |
9 | | fzfid 12634 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(1...(⌊‘𝑚))
∈ Fin) |
10 | | simpl 472 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝜑) |
11 | | elfznn 12241 |
. . . . 5
⊢ (𝑘 ∈
(1...(⌊‘𝑚))
→ 𝑘 ∈
ℕ) |
12 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑋 ∈ 𝐷) |
13 | | nnz 11276 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
14 | 13 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ) |
15 | 4, 1, 5, 2, 12, 14 | dchrzrhcl 24770 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑋‘(𝐿‘𝑘)) ∈ ℂ) |
16 | 10, 11, 15 | syl2an 493 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ (𝑋‘(𝐿‘𝑘)) ∈ ℂ) |
17 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝑚 ∈
ℝ+) |
18 | 11 | nnrpd 11746 |
. . . . . . . 8
⊢ (𝑘 ∈
(1...(⌊‘𝑚))
→ 𝑘 ∈
ℝ+) |
19 | | ifcl 4080 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℝ+
∧ 𝑘 ∈
ℝ+) → if(𝑆 = 0, 𝑚, 𝑘) ∈
ℝ+) |
20 | 17, 18, 19 | syl2an 493 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ if(𝑆 = 0, 𝑚, 𝑘) ∈
ℝ+) |
21 | 20 | relogcld 24173 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ (log‘if(𝑆 = 0,
𝑚, 𝑘)) ∈ ℝ) |
22 | 11 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ 𝑘 ∈
ℕ) |
23 | 21, 22 | nndivred 10946 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ ((log‘if(𝑆 =
0, 𝑚, 𝑘)) / 𝑘) ∈ ℝ) |
24 | 23 | recnd 9947 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ ((log‘if(𝑆 =
0, 𝑚, 𝑘)) / 𝑘) ∈ ℂ) |
25 | 16, 24 | mulcld 9939 |
. . 3
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ) |
26 | 9, 25 | fsumcl 14311 |
. 2
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ) |
27 | | fveq2 6103 |
. . . 4
⊢ (𝑚 = (𝑥 / 𝑑) → (⌊‘𝑚) = (⌊‘(𝑥 / 𝑑))) |
28 | 27 | oveq2d 6565 |
. . 3
⊢ (𝑚 = (𝑥 / 𝑑) → (1...(⌊‘𝑚)) = (1...(⌊‘(𝑥 / 𝑑)))) |
29 | | ifeq1 4040 |
. . . . . . 7
⊢ (𝑚 = (𝑥 / 𝑑) → if(𝑆 = 0, 𝑚, 𝑘) = if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) |
30 | 29 | fveq2d 6107 |
. . . . . 6
⊢ (𝑚 = (𝑥 / 𝑑) → (log‘if(𝑆 = 0, 𝑚, 𝑘)) = (log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘))) |
31 | 30 | oveq1d 6564 |
. . . . 5
⊢ (𝑚 = (𝑥 / 𝑑) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) = ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘)) |
32 | 31 | oveq2d 6565 |
. . . 4
⊢ (𝑚 = (𝑥 / 𝑑) → ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘))) |
33 | 32 | adantr 480 |
. . 3
⊢ ((𝑚 = (𝑥 / 𝑑) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑑)))) → ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘))) |
34 | 28, 33 | sumeq12rdv 14285 |
. 2
⊢ (𝑚 = (𝑥 / 𝑑) → Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑑)))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘))) |
35 | | dchrvmasumif.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) |
36 | | dchrvmasumif.e |
. . 3
⊢ (𝜑 → 𝐸 ∈ (0[,)+∞)) |
37 | 35, 36 | ifcld 4081 |
. 2
⊢ (𝜑 → if(𝑆 = 0, 𝐶, 𝐸) ∈ (0[,)+∞)) |
38 | | 0cn 9911 |
. . 3
⊢ 0 ∈
ℂ |
39 | | dchrvmasumif.t |
. . . 4
⊢ (𝜑 → seq1( + , 𝐾) ⇝ 𝑇) |
40 | | climcl 14078 |
. . . 4
⊢ (seq1( +
, 𝐾) ⇝ 𝑇 → 𝑇 ∈ ℂ) |
41 | 39, 40 | syl 17 |
. . 3
⊢ (𝜑 → 𝑇 ∈ ℂ) |
42 | | ifcl 4080 |
. . 3
⊢ ((0
∈ ℂ ∧ 𝑇
∈ ℂ) → if(𝑆
= 0, 0, 𝑇) ∈
ℂ) |
43 | 38, 41, 42 | sylancr 694 |
. 2
⊢ (𝜑 → if(𝑆 = 0, 0, 𝑇) ∈ ℂ) |
44 | | nnuz 11599 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
45 | | 1zzd 11285 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) |
46 | | nncn 10905 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
47 | 46 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ) |
48 | | nnne0 10930 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0) |
49 | 48 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ≠ 0) |
50 | 15, 47, 49 | divcld 10680 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑋‘(𝐿‘𝑘)) / 𝑘) ∈ ℂ) |
51 | | dchrvmasumif.f |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) |
52 | | fveq2 6103 |
. . . . . . . . . . . . . . 15
⊢ (𝑎 = 𝑘 → (𝐿‘𝑎) = (𝐿‘𝑘)) |
53 | 52 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑘 → (𝑋‘(𝐿‘𝑎)) = (𝑋‘(𝐿‘𝑘))) |
54 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑘 → 𝑎 = 𝑘) |
55 | 53, 54 | oveq12d 6567 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑘 → ((𝑋‘(𝐿‘𝑎)) / 𝑎) = ((𝑋‘(𝐿‘𝑘)) / 𝑘)) |
56 | 55 | cbvmptv 4678 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) = (𝑘 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑘)) / 𝑘)) |
57 | 51, 56 | eqtri 2632 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑘 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑘)) / 𝑘)) |
58 | 50, 57 | fmptd 6292 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶ℂ) |
59 | | ffvelrn 6265 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶ℂ ∧
𝑘 ∈ ℕ) →
(𝐹‘𝑘) ∈ ℂ) |
60 | 58, 59 | sylan 487 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) |
61 | 44, 45, 60 | serf 12691 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ) |
62 | 61 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → seq1( + , 𝐹):ℕ⟶ℂ) |
63 | | 3re 10971 |
. . . . . . . . . . 11
⊢ 3 ∈
ℝ |
64 | | elicopnf 12140 |
. . . . . . . . . . 11
⊢ (3 ∈
ℝ → (𝑚 ∈
(3[,)+∞) ↔ (𝑚
∈ ℝ ∧ 3 ≤ 𝑚))) |
65 | 63, 64 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑚 ∈ (3[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 3 ≤
𝑚))) |
66 | 65 | simprbda 651 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 𝑚 ∈
ℝ) |
67 | | 1red 9934 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 1 ∈
ℝ) |
68 | 63 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 3 ∈
ℝ) |
69 | | 1le3 11121 |
. . . . . . . . . . 11
⊢ 1 ≤
3 |
70 | 69 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 1 ≤
3) |
71 | 65 | simplbda 652 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 3 ≤ 𝑚) |
72 | 67, 68, 66, 70, 71 | letrd 10073 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 1 ≤ 𝑚) |
73 | | flge1nn 12484 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℝ ∧ 1 ≤
𝑚) →
(⌊‘𝑚) ∈
ℕ) |
74 | 66, 72, 73 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
(⌊‘𝑚) ∈
ℕ) |
75 | 74 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) →
(⌊‘𝑚) ∈
ℕ) |
76 | 62, 75 | ffvelrnd 6268 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈
ℂ) |
77 | 76 | abscld 14023 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘(seq1( +
, 𝐹)‘(⌊‘𝑚))) ∈ ℝ) |
78 | | simpl 472 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 𝜑) |
79 | | 0red 9920 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 0 ∈
ℝ) |
80 | | 3pos 10991 |
. . . . . . . . . . 11
⊢ 0 <
3 |
81 | 80 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 0 <
3) |
82 | 79, 68, 66, 81, 71 | ltletrd 10076 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 0 < 𝑚) |
83 | 66, 82 | elrpd 11745 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 𝑚 ∈
ℝ+) |
84 | 78, 83 | jca 553 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (𝜑 ∧ 𝑚 ∈
ℝ+)) |
85 | | elrege0 12149 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (0[,)+∞) ↔
(𝐶 ∈ ℝ ∧ 0
≤ 𝐶)) |
86 | 85 | simplbi 475 |
. . . . . . . . 9
⊢ (𝐶 ∈ (0[,)+∞) →
𝐶 ∈
ℝ) |
87 | 35, 86 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℝ) |
88 | | rerpdivcl 11737 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ ∧ 𝑚 ∈ ℝ+)
→ (𝐶 / 𝑚) ∈
ℝ) |
89 | 87, 88 | sylan 487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → (𝐶 / 𝑚) ∈ ℝ) |
90 | 84, 89 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (𝐶 / 𝑚) ∈ ℝ) |
91 | 90 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (𝐶 / 𝑚) ∈ ℝ) |
92 | 83 | relogcld 24173 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
(log‘𝑚) ∈
ℝ) |
93 | 66, 72 | logge0d 24180 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 0 ≤
(log‘𝑚)) |
94 | 92, 93 | jca 553 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
((log‘𝑚) ∈
ℝ ∧ 0 ≤ (log‘𝑚))) |
95 | 94 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((log‘𝑚) ∈ ℝ ∧ 0 ≤
(log‘𝑚))) |
96 | | oveq2 6557 |
. . . . . . . 8
⊢ (𝑆 = 0 → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 0)) |
97 | 61 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → seq1( + ,
𝐹):ℕ⟶ℂ) |
98 | 97, 74 | ffvelrnd 6268 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (seq1( + ,
𝐹)‘(⌊‘𝑚)) ∈ ℂ) |
99 | 98 | subid1d 10260 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → ((seq1( + ,
𝐹)‘(⌊‘𝑚)) − 0) = (seq1( + , 𝐹)‘(⌊‘𝑚))) |
100 | 96, 99 | sylan9eqr 2666 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆) = (seq1( + , 𝐹)‘(⌊‘𝑚))) |
101 | 100 | fveq2d 6107 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘((seq1(
+ , 𝐹)‘(⌊‘𝑚)) − 𝑆)) = (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))) |
102 | | 1re 9918 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
103 | | elicopnf 12140 |
. . . . . . . . . 10
⊢ (1 ∈
ℝ → (𝑚 ∈
(1[,)+∞) ↔ (𝑚
∈ ℝ ∧ 1 ≤ 𝑚))) |
104 | 102, 103 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑚 ∈ (1[,)+∞) ↔
(𝑚 ∈ ℝ ∧ 1
≤ 𝑚)) |
105 | 66, 72, 104 | sylanbrc 695 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 𝑚 ∈
(1[,)+∞)) |
106 | | dchrvmasumif.1 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦)) |
107 | 106 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → ∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦)) |
108 | | fveq2 6103 |
. . . . . . . . . . . . 13
⊢ (𝑦 = 𝑚 → (⌊‘𝑦) = (⌊‘𝑚)) |
109 | 108 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑦 = 𝑚 → (seq1( + , 𝐹)‘(⌊‘𝑦)) = (seq1( + , 𝐹)‘(⌊‘𝑚))) |
110 | 109 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑦 = 𝑚 → ((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆)) |
111 | 110 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑚 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆))) |
112 | | oveq2 6557 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑚 → (𝐶 / 𝑦) = (𝐶 / 𝑚)) |
113 | 111, 112 | breq12d 4596 |
. . . . . . . . 9
⊢ (𝑦 = 𝑚 → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆)) ≤ (𝐶 / 𝑚))) |
114 | 113 | rspcv 3278 |
. . . . . . . 8
⊢ (𝑚 ∈ (1[,)+∞) →
(∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦) → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆)) ≤ (𝐶 / 𝑚))) |
115 | 105, 107,
114 | sylc 63 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆)) ≤ (𝐶 / 𝑚)) |
116 | 115 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘((seq1(
+ , 𝐹)‘(⌊‘𝑚)) − 𝑆)) ≤ (𝐶 / 𝑚)) |
117 | 101, 116 | eqbrtrrd 4607 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘(seq1( +
, 𝐹)‘(⌊‘𝑚))) ≤ (𝐶 / 𝑚)) |
118 | | lemul2a 10757 |
. . . . 5
⊢
((((abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))) ∈ ℝ ∧ (𝐶 / 𝑚) ∈ ℝ ∧ ((log‘𝑚) ∈ ℝ ∧ 0 ≤
(log‘𝑚))) ∧
(abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))) ≤ (𝐶 / 𝑚)) → ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))) ≤ ((log‘𝑚) · (𝐶 / 𝑚))) |
119 | 77, 91, 95, 117, 118 | syl31anc 1321 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((log‘𝑚) · (abs‘(seq1( + ,
𝐹)‘(⌊‘𝑚)))) ≤ ((log‘𝑚) · (𝐶 / 𝑚))) |
120 | | iftrue 4042 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 = 0 → if(𝑆 = 0, 𝑚, 𝑘) = 𝑚) |
121 | 120 | fveq2d 6107 |
. . . . . . . . . . . . . 14
⊢ (𝑆 = 0 → (log‘if(𝑆 = 0, 𝑚, 𝑘)) = (log‘𝑚)) |
122 | 121 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ (𝑆 = 0 → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) = ((log‘𝑚) / 𝑘)) |
123 | 122 | ad2antlr 759 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) = ((log‘𝑚) / 𝑘)) |
124 | 123 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑚) / 𝑘))) |
125 | 16 | adantlr 747 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (𝑋‘(𝐿‘𝑘)) ∈ ℂ) |
126 | | relogcl 24126 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℝ+
→ (log‘𝑚) ∈
ℝ) |
127 | 126 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(log‘𝑚) ∈
ℝ) |
128 | 127 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(log‘𝑚) ∈
ℂ) |
129 | 128 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (log‘𝑚) ∈
ℂ) |
130 | 11 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → 𝑘 ∈ ℕ) |
131 | 130 | nncnd 10913 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → 𝑘 ∈ ℂ) |
132 | 130 | nnne0d 10942 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → 𝑘 ≠ 0) |
133 | 125, 129,
131, 132 | div12d 10716 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑚) / 𝑘)) = ((log‘𝑚) · ((𝑋‘(𝐿‘𝑘)) / 𝑘))) |
134 | 124, 133 | eqtrd 2644 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((log‘𝑚) · ((𝑋‘(𝐿‘𝑘)) / 𝑘))) |
135 | 134 | sumeq2dv 14281 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = Σ𝑘 ∈ (1...(⌊‘𝑚))((log‘𝑚) · ((𝑋‘(𝐿‘𝑘)) / 𝑘))) |
136 | | iftrue 4042 |
. . . . . . . . . . 11
⊢ (𝑆 = 0 → if(𝑆 = 0, 0, 𝑇) = 0) |
137 | 136 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑆 = 0 → (Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − 0)) |
138 | 26 | subid1d 10260 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − 0) = Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) |
139 | 137, 138 | sylan9eqr 2666 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) |
140 | | ovex 6577 |
. . . . . . . . . . . . . 14
⊢ ((𝑋‘(𝐿‘𝑘)) / 𝑘) ∈ V |
141 | 55, 51, 140 | fvmpt 6191 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = ((𝑋‘(𝐿‘𝑘)) / 𝑘)) |
142 | 22, 141 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ (𝐹‘𝑘) = ((𝑋‘(𝐿‘𝑘)) / 𝑘)) |
143 | 58 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝐹:ℕ⟶ℂ) |
144 | 143, 11, 59 | syl2an 493 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ (𝐹‘𝑘) ∈
ℂ) |
145 | 142, 144 | eqeltrrd 2689 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ ((𝑋‘(𝐿‘𝑘)) / 𝑘) ∈ ℂ) |
146 | 9, 128, 145 | fsummulc2 14358 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
((log‘𝑚) ·
Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) / 𝑘)) = Σ𝑘 ∈ (1...(⌊‘𝑚))((log‘𝑚) · ((𝑋‘(𝐿‘𝑘)) / 𝑘))) |
147 | 146 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → ((log‘𝑚) · Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) / 𝑘)) = Σ𝑘 ∈ (1...(⌊‘𝑚))((log‘𝑚) · ((𝑋‘(𝐿‘𝑘)) / 𝑘))) |
148 | 135, 139,
147 | 3eqtr4d 2654 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = ((log‘𝑚) · Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) / 𝑘))) |
149 | 84, 148 | sylan 487 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = ((log‘𝑚) · Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) / 𝑘))) |
150 | 84, 142 | sylan 487 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ (𝐹‘𝑘) = ((𝑋‘(𝐿‘𝑘)) / 𝑘)) |
151 | 74, 44 | syl6eleq 2698 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
(⌊‘𝑚) ∈
(ℤ≥‘1)) |
152 | 78, 11, 50 | syl2an 493 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ ((𝑋‘(𝐿‘𝑘)) / 𝑘) ∈ ℂ) |
153 | 150, 151,
152 | fsumser 14308 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) / 𝑘) = (seq1( + , 𝐹)‘(⌊‘𝑚))) |
154 | 153 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) / 𝑘) = (seq1( + , 𝐹)‘(⌊‘𝑚))) |
155 | 154 | oveq2d 6565 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((log‘𝑚) · Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) / 𝑘)) = ((log‘𝑚) · (seq1( + , 𝐹)‘(⌊‘𝑚)))) |
156 | 149, 155 | eqtrd 2644 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = ((log‘𝑚) · (seq1( + , 𝐹)‘(⌊‘𝑚)))) |
157 | 156 | fveq2d 6107 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) = (abs‘((log‘𝑚) · (seq1( + , 𝐹)‘(⌊‘𝑚))))) |
158 | 126 | ad2antlr 759 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (log‘𝑚) ∈
ℝ) |
159 | 158 | recnd 9947 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (log‘𝑚) ∈
ℂ) |
160 | 84, 159 | sylan 487 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (log‘𝑚) ∈
ℂ) |
161 | 160, 76 | absmuld 14041 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) →
(abs‘((log‘𝑚)
· (seq1( + , 𝐹)‘(⌊‘𝑚)))) = ((abs‘(log‘𝑚)) · (abs‘(seq1( +
, 𝐹)‘(⌊‘𝑚))))) |
162 | 92, 93 | absidd 14009 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
(abs‘(log‘𝑚)) =
(log‘𝑚)) |
163 | 162 | oveq1d 6564 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
((abs‘(log‘𝑚))
· (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))) = ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))))) |
164 | 163 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) →
((abs‘(log‘𝑚))
· (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))) = ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))))) |
165 | 157, 161,
164 | 3eqtrd 2648 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) = ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))))) |
166 | | iftrue 4042 |
. . . . . . . 8
⊢ (𝑆 = 0 → if(𝑆 = 0, 𝐶, 𝐸) = 𝐶) |
167 | 166 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → if(𝑆 = 0, 𝐶, 𝐸) = 𝐶) |
168 | 167 | oveq1d 6564 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)) = (𝐶 · ((log‘𝑚) / 𝑚))) |
169 | 87 | recnd 9947 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℂ) |
170 | 169 | ad2antrr 758 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → 𝐶 ∈ ℂ) |
171 | | rpcnne0 11726 |
. . . . . . . 8
⊢ (𝑚 ∈ ℝ+
→ (𝑚 ∈ ℂ
∧ 𝑚 ≠
0)) |
172 | 171 | ad2antlr 759 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) |
173 | | div12 10586 |
. . . . . . 7
⊢ ((𝐶 ∈ ℂ ∧
(log‘𝑚) ∈
ℂ ∧ (𝑚 ∈
ℂ ∧ 𝑚 ≠ 0))
→ (𝐶 ·
((log‘𝑚) / 𝑚)) = ((log‘𝑚) · (𝐶 / 𝑚))) |
174 | 170, 159,
172, 173 | syl3anc 1318 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (𝐶 · ((log‘𝑚) / 𝑚)) = ((log‘𝑚) · (𝐶 / 𝑚))) |
175 | 168, 174 | eqtrd 2644 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)) = ((log‘𝑚) · (𝐶 / 𝑚))) |
176 | 84, 175 | sylan 487 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)) = ((log‘𝑚) · (𝐶 / 𝑚))) |
177 | 119, 165,
176 | 3brtr4d 4615 |
. . 3
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚))) |
178 | | dchrvmasumif.2 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ (3[,)+∞)(abs‘((seq1( + ,
𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦))) |
179 | 108 | fveq2d 6107 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑚 → (seq1( + , 𝐾)‘(⌊‘𝑦)) = (seq1( + , 𝐾)‘(⌊‘𝑚))) |
180 | 179 | oveq1d 6564 |
. . . . . . . . 9
⊢ (𝑦 = 𝑚 → ((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇) = ((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) |
181 | 180 | fveq2d 6107 |
. . . . . . . 8
⊢ (𝑦 = 𝑚 → (abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) = (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇))) |
182 | | fveq2 6103 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑚 → (log‘𝑦) = (log‘𝑚)) |
183 | | id 22 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑚 → 𝑦 = 𝑚) |
184 | 182, 183 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑦 = 𝑚 → ((log‘𝑦) / 𝑦) = ((log‘𝑚) / 𝑚)) |
185 | 184 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑦 = 𝑚 → (𝐸 · ((log‘𝑦) / 𝑦)) = (𝐸 · ((log‘𝑚) / 𝑚))) |
186 | 181, 185 | breq12d 4596 |
. . . . . . 7
⊢ (𝑦 = 𝑚 → ((abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦)) ↔ (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) ≤ (𝐸 · ((log‘𝑚) / 𝑚)))) |
187 | 186 | rspccva 3281 |
. . . . . 6
⊢
((∀𝑦 ∈
(3[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦)) ∧ 𝑚 ∈ (3[,)+∞)) →
(abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) ≤ (𝐸 · ((log‘𝑚) / 𝑚))) |
188 | 178, 187 | sylan 487 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
(abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) ≤ (𝐸 · ((log‘𝑚) / 𝑚))) |
189 | 188 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) →
(abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) ≤ (𝐸 · ((log‘𝑚) / 𝑚))) |
190 | | fveq2 6103 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑘 → (log‘𝑎) = (log‘𝑘)) |
191 | 190, 54 | oveq12d 6567 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑘 → ((log‘𝑎) / 𝑎) = ((log‘𝑘) / 𝑘)) |
192 | 53, 191 | oveq12d 6567 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑘 → ((𝑋‘(𝐿‘𝑎)) · ((log‘𝑎) / 𝑎)) = ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘))) |
193 | | dchrvmasumif.g |
. . . . . . . . . 10
⊢ 𝐾 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · ((log‘𝑎) / 𝑎))) |
194 | | ovex 6577 |
. . . . . . . . . 10
⊢ ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘)) ∈ V |
195 | 192, 193,
194 | fvmpt 6191 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝐾‘𝑘) = ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘))) |
196 | 11, 195 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈
(1...(⌊‘𝑚))
→ (𝐾‘𝑘) = ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘))) |
197 | | ifnefalse 4048 |
. . . . . . . . . . . . 13
⊢ (𝑆 ≠ 0 → if(𝑆 = 0, 𝑚, 𝑘) = 𝑘) |
198 | 197 | fveq2d 6107 |
. . . . . . . . . . . 12
⊢ (𝑆 ≠ 0 →
(log‘if(𝑆 = 0, 𝑚, 𝑘)) = (log‘𝑘)) |
199 | 198 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑆 ≠ 0 →
((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) = ((log‘𝑘) / 𝑘)) |
200 | 199 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑆 ≠ 0 → ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘))) |
201 | 200 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘))) |
202 | 201 | eqcomd 2616 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘)) = ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) |
203 | 196, 202 | sylan9eqr 2666 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ (𝐾‘𝑘) = ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) |
204 | 151 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) →
(⌊‘𝑚) ∈
(ℤ≥‘1)) |
205 | | nnrp 11718 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
206 | 205 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+) |
207 | 206 | relogcld 24173 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (log‘𝑘) ∈
ℝ) |
208 | 207 | recnd 9947 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (log‘𝑘) ∈
ℂ) |
209 | 208, 47, 49 | divcld 10680 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((log‘𝑘) / 𝑘) ∈ ℂ) |
210 | 15, 209 | mulcld 9939 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘)) ∈ ℂ) |
211 | 192 | cbvmptv 4678 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · ((log‘𝑎) / 𝑎))) = (𝑘 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘))) |
212 | 193, 211 | eqtri 2632 |
. . . . . . . . . . 11
⊢ 𝐾 = (𝑘 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘))) |
213 | 210, 212 | fmptd 6292 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾:ℕ⟶ℂ) |
214 | 213 | ad2antrr 758 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → 𝐾:ℕ⟶ℂ) |
215 | | ffvelrn 6265 |
. . . . . . . . 9
⊢ ((𝐾:ℕ⟶ℂ ∧
𝑘 ∈ ℕ) →
(𝐾‘𝑘) ∈ ℂ) |
216 | 214, 11, 215 | syl2an 493 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ (𝐾‘𝑘) ∈
ℂ) |
217 | 203, 216 | eqeltrrd 2689 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ) |
218 | 203, 204,
217 | fsumser 14308 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = (seq1( + , 𝐾)‘(⌊‘𝑚))) |
219 | | ifnefalse 4048 |
. . . . . . 7
⊢ (𝑆 ≠ 0 → if(𝑆 = 0, 0, 𝑇) = 𝑇) |
220 | 219 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → if(𝑆 = 0, 0, 𝑇) = 𝑇) |
221 | 218, 220 | oveq12d 6567 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → (Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = ((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) |
222 | 221 | fveq2d 6107 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) = (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇))) |
223 | | ifnefalse 4048 |
. . . . . 6
⊢ (𝑆 ≠ 0 → if(𝑆 = 0, 𝐶, 𝐸) = 𝐸) |
224 | 223 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → if(𝑆 = 0, 𝐶, 𝐸) = 𝐸) |
225 | 224 | oveq1d 6564 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)) = (𝐸 · ((log‘𝑚) / 𝑚))) |
226 | 189, 222,
225 | 3brtr4d 4615 |
. . 3
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚))) |
227 | 177, 226 | pm2.61dane 2869 |
. 2
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚))) |
228 | | fzfid 12634 |
. . . 4
⊢ (𝜑 → (1...2) ∈
Fin) |
229 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → 𝑋 ∈ 𝐷) |
230 | | elfzelz 12213 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...2) → 𝑘 ∈
ℤ) |
231 | 230 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈ ℤ) |
232 | 4, 1, 5, 2, 229, 231 | dchrzrhcl 24770 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → (𝑋‘(𝐿‘𝑘)) ∈ ℂ) |
233 | 232 | abscld 14023 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → (abs‘(𝑋‘(𝐿‘𝑘))) ∈ ℝ) |
234 | 63, 80 | elrpii 11711 |
. . . . . . 7
⊢ 3 ∈
ℝ+ |
235 | | relogcl 24126 |
. . . . . . 7
⊢ (3 ∈
ℝ+ → (log‘3) ∈ ℝ) |
236 | 234, 235 | ax-mp 5 |
. . . . . 6
⊢
(log‘3) ∈ ℝ |
237 | | elfznn 12241 |
. . . . . . 7
⊢ (𝑘 ∈ (1...2) → 𝑘 ∈
ℕ) |
238 | 237 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈ ℕ) |
239 | | nndivre 10933 |
. . . . . 6
⊢
(((log‘3) ∈ ℝ ∧ 𝑘 ∈ ℕ) → ((log‘3) /
𝑘) ∈
ℝ) |
240 | 236, 238,
239 | sylancr 694 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → ((log‘3) /
𝑘) ∈
ℝ) |
241 | 233, 240 | remulcld 9949 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) ∈
ℝ) |
242 | 228, 241 | fsumrecl 14312 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) ∈
ℝ) |
243 | 43 | abscld 14023 |
. . 3
⊢ (𝜑 → (abs‘if(𝑆 = 0, 0, 𝑇)) ∈ ℝ) |
244 | 242, 243 | readdcld 9948 |
. 2
⊢ (𝜑 → (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇))) ∈ ℝ) |
245 | | simpl 472 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 𝜑) |
246 | 63 | rexri 9976 |
. . . . . . . . . . 11
⊢ 3 ∈
ℝ* |
247 | | elico2 12108 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ 3 ∈ ℝ*) → (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 3))) |
248 | 102, 246,
247 | mp2an 704 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤
𝑚 ∧ 𝑚 < 3)) |
249 | 248 | simp1bi 1069 |
. . . . . . . . 9
⊢ (𝑚 ∈ (1[,)3) → 𝑚 ∈
ℝ) |
250 | 249 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 𝑚 ∈ ℝ) |
251 | | 0red 9920 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ∈
ℝ) |
252 | | 1red 9934 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 1 ∈
ℝ) |
253 | | 0lt1 10429 |
. . . . . . . . . 10
⊢ 0 <
1 |
254 | 253 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 <
1) |
255 | 248 | simp2bi 1070 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (1[,)3) → 1 ≤
𝑚) |
256 | 255 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 1 ≤ 𝑚) |
257 | 251, 252,
250, 254, 256 | ltletrd 10076 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 < 𝑚) |
258 | 250, 257 | elrpd 11745 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 𝑚 ∈ ℝ+) |
259 | 245, 258 | jca 553 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (𝜑 ∧ 𝑚 ∈
ℝ+)) |
260 | 43 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → if(𝑆 = 0, 0, 𝑇) ∈ ℂ) |
261 | 26, 260 | subcld 10271 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) ∈ ℂ) |
262 | 259, 261 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) ∈ ℂ) |
263 | 262 | abscld 14023 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ∈ ℝ) |
264 | 259, 26 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ) |
265 | 264 | abscld 14023 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
(abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
266 | 243 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (abs‘if(𝑆 = 0, 0, 𝑇)) ∈ ℝ) |
267 | 265, 266 | readdcld 9948 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
((abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) + (abs‘if(𝑆 = 0, 0, 𝑇))) ∈ ℝ) |
268 | 242 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → Σ𝑘 ∈
(1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) ∈
ℝ) |
269 | 268, 266 | readdcld 9948 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (Σ𝑘 ∈
(1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇))) ∈ ℝ) |
270 | 26, 260 | abs2dif2d 14045 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ ((abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) + (abs‘if(𝑆 = 0, 0, 𝑇)))) |
271 | 259, 270 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ ((abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) + (abs‘if(𝑆 = 0, 0, 𝑇)))) |
272 | 25 | abscld 14023 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ (abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
273 | 9, 272 | fsumrecl 14312 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
Σ𝑘 ∈
(1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
274 | 259, 273 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → Σ𝑘 ∈
(1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
275 | 9, 25 | fsumabs 14374 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))) |
276 | 259, 275 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
(abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))) |
277 | | fzfid 12634 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → (1...2)
∈ Fin) |
278 | 232 | adantlr 747 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (𝑋‘(𝐿‘𝑘)) ∈ ℂ) |
279 | 17 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑚 ∈
ℝ+) |
280 | 237 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈
ℕ) |
281 | 280 | nnrpd 11746 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈
ℝ+) |
282 | 279, 281 | ifcld 4081 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → if(𝑆 = 0, 𝑚, 𝑘) ∈
ℝ+) |
283 | 282 | relogcld 24173 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
(log‘if(𝑆 = 0, 𝑚, 𝑘)) ∈ ℝ) |
284 | 283, 280 | nndivred 10946 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ∈ ℝ) |
285 | 284 | recnd 9947 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ∈ ℂ) |
286 | 278, 285 | mulcld 9939 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ) |
287 | 286 | abscld 14023 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
288 | 277, 287 | fsumrecl 14312 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
Σ𝑘 ∈
(1...2)(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
289 | 259, 288 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → Σ𝑘 ∈
(1...2)(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
290 | | fzfid 12634 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (1...2) ∈
Fin) |
291 | 259, 286 | sylan 487 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ) |
292 | 291 | abscld 14023 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
293 | 291 | absge0d 14031 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 0 ≤
(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))) |
294 | 250 | flcld 12461 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (⌊‘𝑚) ∈
ℤ) |
295 | | 2z 11286 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
296 | 295 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 2 ∈
ℤ) |
297 | 248 | simp3bi 1071 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (1[,)3) → 𝑚 < 3) |
298 | 297 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 𝑚 < 3) |
299 | | 3z 11287 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
ℤ |
300 | | fllt 12469 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℝ ∧ 3 ∈
ℤ) → (𝑚 < 3
↔ (⌊‘𝑚)
< 3)) |
301 | 250, 299,
300 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (𝑚 < 3 ↔ (⌊‘𝑚) < 3)) |
302 | 298, 301 | mpbid 221 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (⌊‘𝑚) < 3) |
303 | | df-3 10957 |
. . . . . . . . . . . 12
⊢ 3 = (2 +
1) |
304 | 302, 303 | syl6breq 4624 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (⌊‘𝑚) < (2 + 1)) |
305 | | rpre 11715 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℝ+
→ 𝑚 ∈
ℝ) |
306 | 305 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝑚 ∈
ℝ) |
307 | 306 | flcld 12461 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(⌊‘𝑚) ∈
ℤ) |
308 | | zleltp1 11305 |
. . . . . . . . . . . . 13
⊢
(((⌊‘𝑚)
∈ ℤ ∧ 2 ∈ ℤ) → ((⌊‘𝑚) ≤ 2 ↔
(⌊‘𝑚) < (2 +
1))) |
309 | 307, 295,
308 | sylancl 693 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
((⌊‘𝑚) ≤ 2
↔ (⌊‘𝑚)
< (2 + 1))) |
310 | 259, 309 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → ((⌊‘𝑚) ≤ 2 ↔
(⌊‘𝑚) < (2 +
1))) |
311 | 304, 310 | mpbird 246 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (⌊‘𝑚) ≤ 2) |
312 | | eluz2 11569 |
. . . . . . . . . 10
⊢ (2 ∈
(ℤ≥‘(⌊‘𝑚)) ↔ ((⌊‘𝑚) ∈ ℤ ∧ 2 ∈ ℤ ∧
(⌊‘𝑚) ≤
2)) |
313 | 294, 296,
311, 312 | syl3anbrc 1239 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 2 ∈
(ℤ≥‘(⌊‘𝑚))) |
314 | | fzss2 12252 |
. . . . . . . . 9
⊢ (2 ∈
(ℤ≥‘(⌊‘𝑚)) → (1...(⌊‘𝑚)) ⊆
(1...2)) |
315 | 313, 314 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
(1...(⌊‘𝑚))
⊆ (1...2)) |
316 | 290, 292,
293, 315 | fsumless 14369 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → Σ𝑘 ∈
(1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))) |
317 | 241 | adantlr 747 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) ∈
ℝ) |
318 | 278, 285 | absmuld 14041 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) = ((abs‘(𝑋‘(𝐿‘𝑘))) · (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))) |
319 | 259, 318 | sylan 487 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) = ((abs‘(𝑋‘(𝐿‘𝑘))) · (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))) |
320 | 259, 284 | sylan 487 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ∈ ℝ) |
321 | 259, 283 | sylan 487 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (log‘if(𝑆 = 0, 𝑚, 𝑘)) ∈ ℝ) |
322 | | log1 24136 |
. . . . . . . . . . . . . 14
⊢
(log‘1) = 0 |
323 | | elfzle1 12215 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (1...2) → 1 ≤
𝑘) |
324 | | breq2 4587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = if(𝑆 = 0, 𝑚, 𝑘) → (1 ≤ 𝑚 ↔ 1 ≤ if(𝑆 = 0, 𝑚, 𝑘))) |
325 | | breq2 4587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = if(𝑆 = 0, 𝑚, 𝑘) → (1 ≤ 𝑘 ↔ 1 ≤ if(𝑆 = 0, 𝑚, 𝑘))) |
326 | 324, 325 | ifboth 4074 |
. . . . . . . . . . . . . . . 16
⊢ ((1 ≤
𝑚 ∧ 1 ≤ 𝑘) → 1 ≤ if(𝑆 = 0, 𝑚, 𝑘)) |
327 | 256, 323,
326 | syl2an 493 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 1 ≤ if(𝑆 = 0, 𝑚, 𝑘)) |
328 | | 1rp 11712 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ+ |
329 | | logleb 24153 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℝ+ ∧ if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ+) → (1 ≤
if(𝑆 = 0, 𝑚, 𝑘) ↔ (log‘1) ≤
(log‘if(𝑆 = 0, 𝑚, 𝑘)))) |
330 | 328, 282,
329 | sylancr 694 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (1 ≤
if(𝑆 = 0, 𝑚, 𝑘) ↔ (log‘1) ≤
(log‘if(𝑆 = 0, 𝑚, 𝑘)))) |
331 | 259, 330 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (1 ≤ if(𝑆 = 0, 𝑚, 𝑘) ↔ (log‘1) ≤
(log‘if(𝑆 = 0, 𝑚, 𝑘)))) |
332 | 327, 331 | mpbid 221 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (log‘1) ≤
(log‘if(𝑆 = 0, 𝑚, 𝑘))) |
333 | 322, 332 | syl5eqbrr 4619 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 0 ≤
(log‘if(𝑆 = 0, 𝑚, 𝑘))) |
334 | 281 | rpregt0d 11754 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (𝑘 ∈ ℝ ∧ 0 <
𝑘)) |
335 | 259, 334 | sylan 487 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (𝑘 ∈ ℝ ∧ 0 < 𝑘)) |
336 | | divge0 10771 |
. . . . . . . . . . . . 13
⊢
((((log‘if(𝑆 =
0, 𝑚, 𝑘)) ∈ ℝ ∧ 0 ≤
(log‘if(𝑆 = 0, 𝑚, 𝑘))) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤
((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) |
337 | 321, 333,
335, 336 | syl21anc 1317 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 0 ≤
((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) |
338 | 320, 337 | absidd 14009 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) →
(abs‘((log‘if(𝑆
= 0, 𝑚, 𝑘)) / 𝑘)) = ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) |
339 | 338, 320 | eqeltrd 2688 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) →
(abs‘((log‘if(𝑆
= 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℝ) |
340 | 240 | adantlr 747 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((log‘3) /
𝑘) ∈
ℝ) |
341 | 233 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
(abs‘(𝑋‘(𝐿‘𝑘))) ∈ ℝ) |
342 | 278 | absge0d 14031 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 0 ≤
(abs‘(𝑋‘(𝐿‘𝑘)))) |
343 | 341, 342 | jca 553 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
((abs‘(𝑋‘(𝐿‘𝑘))) ∈ ℝ ∧ 0 ≤
(abs‘(𝑋‘(𝐿‘𝑘))))) |
344 | 259, 343 | sylan 487 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿‘𝑘))) ∈ ℝ ∧ 0 ≤
(abs‘(𝑋‘(𝐿‘𝑘))))) |
345 | 297 | ad2antlr 759 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 𝑚 < 3) |
346 | 280 | nnred 10912 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈
ℝ) |
347 | | 2re 10967 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
348 | 347 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 2 ∈
ℝ) |
349 | 63 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 3 ∈
ℝ) |
350 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (1...2) → 𝑘 ≤ 2) |
351 | 350 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 ≤ 2) |
352 | | 2lt3 11072 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 <
3 |
353 | 352 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 2 <
3) |
354 | 346, 348,
349, 351, 353 | lelttrd 10074 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 < 3) |
355 | 259, 354 | sylan 487 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 𝑘 < 3) |
356 | | breq1 4586 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = if(𝑆 = 0, 𝑚, 𝑘) → (𝑚 < 3 ↔ if(𝑆 = 0, 𝑚, 𝑘) < 3)) |
357 | | breq1 4586 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = if(𝑆 = 0, 𝑚, 𝑘) → (𝑘 < 3 ↔ if(𝑆 = 0, 𝑚, 𝑘) < 3)) |
358 | 356, 357 | ifboth 4074 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 < 3 ∧ 𝑘 < 3) → if(𝑆 = 0, 𝑚, 𝑘) < 3) |
359 | 345, 355,
358 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → if(𝑆 = 0, 𝑚, 𝑘) < 3) |
360 | 282 | rpred 11748 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ) |
361 | | ltle 10005 |
. . . . . . . . . . . . . . . 16
⊢
((if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ ∧ 3 ∈ ℝ)
→ (if(𝑆 = 0, 𝑚, 𝑘) < 3 → if(𝑆 = 0, 𝑚, 𝑘) ≤ 3)) |
362 | 360, 63, 361 | sylancl 693 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
(if(𝑆 = 0, 𝑚, 𝑘) < 3 → if(𝑆 = 0, 𝑚, 𝑘) ≤ 3)) |
363 | 259, 362 | sylan 487 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (if(𝑆 = 0, 𝑚, 𝑘) < 3 → if(𝑆 = 0, 𝑚, 𝑘) ≤ 3)) |
364 | 359, 363 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → if(𝑆 = 0, 𝑚, 𝑘) ≤ 3) |
365 | | logleb 24153 |
. . . . . . . . . . . . . . 15
⊢
((if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ+ ∧ 3 ∈
ℝ+) → (if(𝑆 = 0, 𝑚, 𝑘) ≤ 3 ↔ (log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3))) |
366 | 282, 234,
365 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
(if(𝑆 = 0, 𝑚, 𝑘) ≤ 3 ↔ (log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3))) |
367 | 259, 366 | sylan 487 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (if(𝑆 = 0, 𝑚, 𝑘) ≤ 3 ↔ (log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3))) |
368 | 364, 367 | mpbid 221 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3)) |
369 | 236 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
(log‘3) ∈ ℝ) |
370 | 283, 369,
281 | lediv1d 11794 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
((log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3) ↔
((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ≤ ((log‘3) / 𝑘))) |
371 | 259, 370 | sylan 487 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3) ↔
((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ≤ ((log‘3) / 𝑘))) |
372 | 368, 371 | mpbid 221 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ≤ ((log‘3) / 𝑘)) |
373 | 338, 372 | eqbrtrd 4605 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) →
(abs‘((log‘if(𝑆
= 0, 𝑚, 𝑘)) / 𝑘)) ≤ ((log‘3) / 𝑘)) |
374 | | lemul2a 10757 |
. . . . . . . . . 10
⊢
((((abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℝ ∧ ((log‘3) /
𝑘) ∈ ℝ ∧
((abs‘(𝑋‘(𝐿‘𝑘))) ∈ ℝ ∧ 0 ≤
(abs‘(𝑋‘(𝐿‘𝑘))))) ∧ (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ≤ ((log‘3) / 𝑘)) → ((abs‘(𝑋‘(𝐿‘𝑘))) · (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ ((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘))) |
375 | 339, 340,
344, 373, 374 | syl31anc 1321 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿‘𝑘))) · (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ ((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘))) |
376 | 319, 375 | eqbrtrd 4605 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ ((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘))) |
377 | 290, 292,
317, 376 | fsumle 14372 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → Σ𝑘 ∈
(1...2)(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘))) |
378 | 274, 289,
268, 316, 377 | letrd 10073 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → Σ𝑘 ∈
(1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘))) |
379 | 265, 274,
268, 276, 378 | letrd 10073 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
(abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘))) |
380 | 26 | abscld 14023 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
381 | 242 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
Σ𝑘 ∈
(1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) ∈
ℝ) |
382 | 260 | abscld 14023 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(abs‘if(𝑆 = 0, 0,
𝑇)) ∈
ℝ) |
383 | 380, 381,
382 | leadd1d 10500 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
((abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) ↔
((abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) + (abs‘if(𝑆 = 0, 0, 𝑇))) ≤ (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇))))) |
384 | 259, 383 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
((abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) ↔
((abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) + (abs‘if(𝑆 = 0, 0, 𝑇))) ≤ (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇))))) |
385 | 379, 384 | mpbid 221 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
((abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) + (abs‘if(𝑆 = 0, 0, 𝑇))) ≤ (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇)))) |
386 | 263, 267,
269, 271, 385 | letrd 10073 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇)))) |
387 | 386 | ralrimiva 2949 |
. 2
⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇)))) |
388 | 1, 2, 3, 4, 5, 6, 7, 8, 26, 34, 37, 43, 227, 244, 387 | dchrvmasumlem3 24988 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑑)))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)))) ∈ 𝑂(1)) |