| 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 14014 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(1...(⌊‘𝑚))
∈ Fin) |
| 10 | | simpl 482 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝜑) |
| 11 | | elfznn 13593 |
. . . . 5
⊢ (𝑘 ∈
(1...(⌊‘𝑚))
→ 𝑘 ∈
ℕ) |
| 12 | 7 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑋 ∈ 𝐷) |
| 13 | | nnz 12634 |
. . . . . . 7
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℤ) |
| 14 | 13 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℤ) |
| 15 | 4, 1, 5, 2, 12, 14 | dchrzrhcl 27289 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑋‘(𝐿‘𝑘)) ∈ ℂ) |
| 16 | 10, 11, 15 | syl2an 596 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ (𝑋‘(𝐿‘𝑘)) ∈ ℂ) |
| 17 | | simpr 484 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝑚 ∈
ℝ+) |
| 18 | 11 | nnrpd 13075 |
. . . . . . . 8
⊢ (𝑘 ∈
(1...(⌊‘𝑚))
→ 𝑘 ∈
ℝ+) |
| 19 | | ifcl 4571 |
. . . . . . . 8
⊢ ((𝑚 ∈ ℝ+
∧ 𝑘 ∈
ℝ+) → if(𝑆 = 0, 𝑚, 𝑘) ∈
ℝ+) |
| 20 | 17, 18, 19 | syl2an 596 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ if(𝑆 = 0, 𝑚, 𝑘) ∈
ℝ+) |
| 21 | 20 | relogcld 26665 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ (log‘if(𝑆 = 0,
𝑚, 𝑘)) ∈ ℝ) |
| 22 | 11 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ 𝑘 ∈
ℕ) |
| 23 | 21, 22 | nndivred 12320 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ ((log‘if(𝑆 =
0, 𝑚, 𝑘)) / 𝑘) ∈ ℝ) |
| 24 | 23 | recnd 11289 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ ((log‘if(𝑆 =
0, 𝑚, 𝑘)) / 𝑘) ∈ ℂ) |
| 25 | 16, 24 | mulcld 11281 |
. . 3
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ) |
| 26 | 9, 25 | fsumcl 15769 |
. 2
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ) |
| 27 | | fveq2 6906 |
. . . 4
⊢ (𝑚 = (𝑥 / 𝑑) → (⌊‘𝑚) = (⌊‘(𝑥 / 𝑑))) |
| 28 | 27 | oveq2d 7447 |
. . 3
⊢ (𝑚 = (𝑥 / 𝑑) → (1...(⌊‘𝑚)) = (1...(⌊‘(𝑥 / 𝑑)))) |
| 29 | | ifeq1 4529 |
. . . . . . 7
⊢ (𝑚 = (𝑥 / 𝑑) → if(𝑆 = 0, 𝑚, 𝑘) = if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) |
| 30 | 29 | fveq2d 6910 |
. . . . . 6
⊢ (𝑚 = (𝑥 / 𝑑) → (log‘if(𝑆 = 0, 𝑚, 𝑘)) = (log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘))) |
| 31 | 30 | oveq1d 7446 |
. . . . 5
⊢ (𝑚 = (𝑥 / 𝑑) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) = ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘)) |
| 32 | 31 | oveq2d 7447 |
. . . 4
⊢ (𝑚 = (𝑥 / 𝑑) → ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘))) |
| 33 | 32 | adantr 480 |
. . 3
⊢ ((𝑚 = (𝑥 / 𝑑) ∧ 𝑘 ∈ (1...(⌊‘(𝑥 / 𝑑)))) → ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘))) |
| 34 | 28, 33 | sumeq12rdv 15743 |
. 2
⊢ (𝑚 = (𝑥 / 𝑑) → Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑑)))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘))) |
| 35 | | dchrvmasumif.c |
. . 3
⊢ (𝜑 → 𝐶 ∈ (0[,)+∞)) |
| 36 | | dchrvmasumif.e |
. . 3
⊢ (𝜑 → 𝐸 ∈ (0[,)+∞)) |
| 37 | 35, 36 | ifcld 4572 |
. 2
⊢ (𝜑 → if(𝑆 = 0, 𝐶, 𝐸) ∈ (0[,)+∞)) |
| 38 | | 0cn 11253 |
. . 3
⊢ 0 ∈
ℂ |
| 39 | | dchrvmasumif.t |
. . . 4
⊢ (𝜑 → seq1( + , 𝐾) ⇝ 𝑇) |
| 40 | | climcl 15535 |
. . . 4
⊢ (seq1( +
, 𝐾) ⇝ 𝑇 → 𝑇 ∈ ℂ) |
| 41 | 39, 40 | syl 17 |
. . 3
⊢ (𝜑 → 𝑇 ∈ ℂ) |
| 42 | | ifcl 4571 |
. . 3
⊢ ((0
∈ ℂ ∧ 𝑇
∈ ℂ) → if(𝑆
= 0, 0, 𝑇) ∈
ℂ) |
| 43 | 38, 41, 42 | sylancr 587 |
. 2
⊢ (𝜑 → if(𝑆 = 0, 0, 𝑇) ∈ ℂ) |
| 44 | | nnuz 12921 |
. . . . . . . . 9
⊢ ℕ =
(ℤ≥‘1) |
| 45 | | 1zzd 12648 |
. . . . . . . . 9
⊢ (𝜑 → 1 ∈
ℤ) |
| 46 | | nncn 12274 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℂ) |
| 47 | 46 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℂ) |
| 48 | | nnne0 12300 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → 𝑘 ≠ 0) |
| 49 | 48 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ≠ 0) |
| 50 | 15, 47, 49 | divcld 12043 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑋‘(𝐿‘𝑘)) / 𝑘) ∈ ℂ) |
| 51 | | dchrvmasumif.f |
. . . . . . . . . . . 12
⊢ 𝐹 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) |
| 52 | | 2fveq3 6911 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑘 → (𝑋‘(𝐿‘𝑎)) = (𝑋‘(𝐿‘𝑘))) |
| 53 | | id 22 |
. . . . . . . . . . . . . 14
⊢ (𝑎 = 𝑘 → 𝑎 = 𝑘) |
| 54 | 52, 53 | oveq12d 7449 |
. . . . . . . . . . . . 13
⊢ (𝑎 = 𝑘 → ((𝑋‘(𝐿‘𝑎)) / 𝑎) = ((𝑋‘(𝐿‘𝑘)) / 𝑘)) |
| 55 | 54 | cbvmptv 5255 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) / 𝑎)) = (𝑘 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑘)) / 𝑘)) |
| 56 | 51, 55 | eqtri 2765 |
. . . . . . . . . . 11
⊢ 𝐹 = (𝑘 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑘)) / 𝑘)) |
| 57 | 50, 56 | fmptd 7134 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐹:ℕ⟶ℂ) |
| 58 | | ffvelcdm 7101 |
. . . . . . . . . 10
⊢ ((𝐹:ℕ⟶ℂ ∧
𝑘 ∈ ℕ) →
(𝐹‘𝑘) ∈ ℂ) |
| 59 | 57, 58 | sylan 580 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) |
| 60 | 44, 45, 59 | serf 14071 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐹):ℕ⟶ℂ) |
| 61 | 60 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → seq1( + , 𝐹):ℕ⟶ℂ) |
| 62 | | 3re 12346 |
. . . . . . . . . . 11
⊢ 3 ∈
ℝ |
| 63 | | elicopnf 13485 |
. . . . . . . . . . 11
⊢ (3 ∈
ℝ → (𝑚 ∈
(3[,)+∞) ↔ (𝑚
∈ ℝ ∧ 3 ≤ 𝑚))) |
| 64 | 62, 63 | mp1i 13 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑚 ∈ (3[,)+∞) ↔ (𝑚 ∈ ℝ ∧ 3 ≤
𝑚))) |
| 65 | 64 | simprbda 498 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 𝑚 ∈
ℝ) |
| 66 | | 1red 11262 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 1 ∈
ℝ) |
| 67 | 62 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 3 ∈
ℝ) |
| 68 | | 1le3 12478 |
. . . . . . . . . . 11
⊢ 1 ≤
3 |
| 69 | 68 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 1 ≤
3) |
| 70 | 64 | simplbda 499 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 3 ≤ 𝑚) |
| 71 | 66, 67, 65, 69, 70 | letrd 11418 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 1 ≤ 𝑚) |
| 72 | | flge1nn 13861 |
. . . . . . . . 9
⊢ ((𝑚 ∈ ℝ ∧ 1 ≤
𝑚) →
(⌊‘𝑚) ∈
ℕ) |
| 73 | 65, 71, 72 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
(⌊‘𝑚) ∈
ℕ) |
| 74 | 73 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) →
(⌊‘𝑚) ∈
ℕ) |
| 75 | 61, 74 | ffvelcdmd 7105 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (seq1( + , 𝐹)‘(⌊‘𝑚)) ∈
ℂ) |
| 76 | 75 | abscld 15475 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘(seq1( +
, 𝐹)‘(⌊‘𝑚))) ∈ ℝ) |
| 77 | | simpl 482 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 𝜑) |
| 78 | | 0red 11264 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 0 ∈
ℝ) |
| 79 | | 3pos 12371 |
. . . . . . . . . . 11
⊢ 0 <
3 |
| 80 | 79 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 0 <
3) |
| 81 | 78, 67, 65, 80, 70 | ltletrd 11421 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 0 < 𝑚) |
| 82 | 65, 81 | elrpd 13074 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 𝑚 ∈
ℝ+) |
| 83 | 77, 82 | jca 511 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (𝜑 ∧ 𝑚 ∈
ℝ+)) |
| 84 | | elrege0 13494 |
. . . . . . . . . 10
⊢ (𝐶 ∈ (0[,)+∞) ↔
(𝐶 ∈ ℝ ∧ 0
≤ 𝐶)) |
| 85 | 84 | simplbi 497 |
. . . . . . . . 9
⊢ (𝐶 ∈ (0[,)+∞) →
𝐶 ∈
ℝ) |
| 86 | 35, 85 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℝ) |
| 87 | | rerpdivcl 13065 |
. . . . . . . 8
⊢ ((𝐶 ∈ ℝ ∧ 𝑚 ∈ ℝ+)
→ (𝐶 / 𝑚) ∈
ℝ) |
| 88 | 86, 87 | sylan 580 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → (𝐶 / 𝑚) ∈ ℝ) |
| 89 | 83, 88 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (𝐶 / 𝑚) ∈ ℝ) |
| 90 | 89 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (𝐶 / 𝑚) ∈ ℝ) |
| 91 | 82 | relogcld 26665 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
(log‘𝑚) ∈
ℝ) |
| 92 | 65, 71 | logge0d 26672 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 0 ≤
(log‘𝑚)) |
| 93 | 91, 92 | jca 511 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
((log‘𝑚) ∈
ℝ ∧ 0 ≤ (log‘𝑚))) |
| 94 | 93 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((log‘𝑚) ∈ ℝ ∧ 0 ≤
(log‘𝑚))) |
| 95 | | oveq2 7439 |
. . . . . . . 8
⊢ (𝑆 = 0 → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆) = ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 0)) |
| 96 | 60 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → seq1( + ,
𝐹):ℕ⟶ℂ) |
| 97 | 96, 73 | ffvelcdmd 7105 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → (seq1( + ,
𝐹)‘(⌊‘𝑚)) ∈ ℂ) |
| 98 | 97 | subid1d 11609 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → ((seq1( + ,
𝐹)‘(⌊‘𝑚)) − 0) = (seq1( + , 𝐹)‘(⌊‘𝑚))) |
| 99 | 95, 98 | sylan9eqr 2799 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆) = (seq1( + , 𝐹)‘(⌊‘𝑚))) |
| 100 | 99 | fveq2d 6910 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘((seq1(
+ , 𝐹)‘(⌊‘𝑚)) − 𝑆)) = (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))) |
| 101 | | 2fveq3 6911 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑚 → (seq1( + , 𝐹)‘(⌊‘𝑦)) = (seq1( + , 𝐹)‘(⌊‘𝑚))) |
| 102 | 101 | fvoveq1d 7453 |
. . . . . . . . 9
⊢ (𝑦 = 𝑚 → (abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) = (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆))) |
| 103 | | oveq2 7439 |
. . . . . . . . 9
⊢ (𝑦 = 𝑚 → (𝐶 / 𝑦) = (𝐶 / 𝑚)) |
| 104 | 102, 103 | breq12d 5156 |
. . . . . . . 8
⊢ (𝑦 = 𝑚 → ((abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦) ↔ (abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆)) ≤ (𝐶 / 𝑚))) |
| 105 | | dchrvmasumif.1 |
. . . . . . . . 9
⊢ (𝜑 → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦)) |
| 106 | 105 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → ∀𝑦 ∈
(1[,)+∞)(abs‘((seq1( + , 𝐹)‘(⌊‘𝑦)) − 𝑆)) ≤ (𝐶 / 𝑦)) |
| 107 | | 1re 11261 |
. . . . . . . . . 10
⊢ 1 ∈
ℝ |
| 108 | | elicopnf 13485 |
. . . . . . . . . 10
⊢ (1 ∈
ℝ → (𝑚 ∈
(1[,)+∞) ↔ (𝑚
∈ ℝ ∧ 1 ≤ 𝑚))) |
| 109 | 107, 108 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑚 ∈ (1[,)+∞) ↔
(𝑚 ∈ ℝ ∧ 1
≤ 𝑚)) |
| 110 | 65, 71, 109 | sylanbrc 583 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → 𝑚 ∈
(1[,)+∞)) |
| 111 | 104, 106,
110 | rspcdva 3623 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
(abs‘((seq1( + , 𝐹)‘(⌊‘𝑚)) − 𝑆)) ≤ (𝐶 / 𝑚)) |
| 112 | 111 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘((seq1(
+ , 𝐹)‘(⌊‘𝑚)) − 𝑆)) ≤ (𝐶 / 𝑚)) |
| 113 | 100, 112 | eqbrtrrd 5167 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (abs‘(seq1( +
, 𝐹)‘(⌊‘𝑚))) ≤ (𝐶 / 𝑚)) |
| 114 | | lemul2a 12122 |
. . . . 5
⊢
((((abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))) ∈ ℝ ∧ (𝐶 / 𝑚) ∈ ℝ ∧ ((log‘𝑚) ∈ ℝ ∧ 0 ≤
(log‘𝑚))) ∧
(abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))) ≤ (𝐶 / 𝑚)) → ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))) ≤ ((log‘𝑚) · (𝐶 / 𝑚))) |
| 115 | 76, 90, 94, 113, 114 | syl31anc 1375 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((log‘𝑚) · (abs‘(seq1( + ,
𝐹)‘(⌊‘𝑚)))) ≤ ((log‘𝑚) · (𝐶 / 𝑚))) |
| 116 | | iftrue 4531 |
. . . . . . . . . . . . . . 15
⊢ (𝑆 = 0 → if(𝑆 = 0, 𝑚, 𝑘) = 𝑚) |
| 117 | 116 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ (𝑆 = 0 → (log‘if(𝑆 = 0, 𝑚, 𝑘)) = (log‘𝑚)) |
| 118 | 117 | oveq1d 7446 |
. . . . . . . . . . . . 13
⊢ (𝑆 = 0 → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) = ((log‘𝑚) / 𝑘)) |
| 119 | 118 | ad2antlr 727 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) = ((log‘𝑚) / 𝑘)) |
| 120 | 119 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑚) / 𝑘))) |
| 121 | 16 | adantlr 715 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (𝑋‘(𝐿‘𝑘)) ∈ ℂ) |
| 122 | | relogcl 26617 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℝ+
→ (log‘𝑚) ∈
ℝ) |
| 123 | 122 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(log‘𝑚) ∈
ℝ) |
| 124 | 123 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(log‘𝑚) ∈
ℂ) |
| 125 | 124 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → (log‘𝑚) ∈
ℂ) |
| 126 | 11 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → 𝑘 ∈ ℕ) |
| 127 | 126 | nncnd 12282 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → 𝑘 ∈ ℂ) |
| 128 | 126 | nnne0d 12316 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → 𝑘 ≠ 0) |
| 129 | 121, 125,
127, 128 | div12d 12079 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑚) / 𝑘)) = ((log‘𝑚) · ((𝑋‘(𝐿‘𝑘)) / 𝑘))) |
| 130 | 120, 129 | eqtrd 2777 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) ∧ 𝑘 ∈ (1...(⌊‘𝑚))) → ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((log‘𝑚) · ((𝑋‘(𝐿‘𝑘)) / 𝑘))) |
| 131 | 130 | sumeq2dv 15738 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = Σ𝑘 ∈ (1...(⌊‘𝑚))((log‘𝑚) · ((𝑋‘(𝐿‘𝑘)) / 𝑘))) |
| 132 | | iftrue 4531 |
. . . . . . . . . . 11
⊢ (𝑆 = 0 → if(𝑆 = 0, 0, 𝑇) = 0) |
| 133 | 132 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑆 = 0 → (Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = (Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − 0)) |
| 134 | 26 | subid1d 11609 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − 0) = Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) |
| 135 | 133, 134 | sylan9eqr 2799 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) |
| 136 | | ovex 7464 |
. . . . . . . . . . . . . 14
⊢ ((𝑋‘(𝐿‘𝑘)) / 𝑘) ∈ V |
| 137 | 54, 51, 136 | fvmpt 7016 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = ((𝑋‘(𝐿‘𝑘)) / 𝑘)) |
| 138 | 22, 137 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ (𝐹‘𝑘) = ((𝑋‘(𝐿‘𝑘)) / 𝑘)) |
| 139 | 57 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝐹:ℕ⟶ℂ) |
| 140 | 139, 11, 58 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ (𝐹‘𝑘) ∈
ℂ) |
| 141 | 138, 140 | eqeltrrd 2842 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ ((𝑋‘(𝐿‘𝑘)) / 𝑘) ∈ ℂ) |
| 142 | 9, 124, 141 | fsummulc2 15820 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
((log‘𝑚) ·
Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) / 𝑘)) = Σ𝑘 ∈ (1...(⌊‘𝑚))((log‘𝑚) · ((𝑋‘(𝐿‘𝑘)) / 𝑘))) |
| 143 | 142 | adantr 480 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → ((log‘𝑚) · Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) / 𝑘)) = Σ𝑘 ∈ (1...(⌊‘𝑚))((log‘𝑚) · ((𝑋‘(𝐿‘𝑘)) / 𝑘))) |
| 144 | 131, 135,
143 | 3eqtr4d 2787 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = ((log‘𝑚) · Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) / 𝑘))) |
| 145 | 83, 144 | sylan 580 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = ((log‘𝑚) · Σ𝑘 ∈ (1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) / 𝑘))) |
| 146 | 83, 138 | sylan 580 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ (𝐹‘𝑘) = ((𝑋‘(𝐿‘𝑘)) / 𝑘)) |
| 147 | 73, 44 | eleqtrdi 2851 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
(⌊‘𝑚) ∈
(ℤ≥‘1)) |
| 148 | 77, 11, 50 | syl2an 596 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ ((𝑋‘(𝐿‘𝑘)) / 𝑘) ∈ ℂ) |
| 149 | 146, 147,
148 | fsumser 15766 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) → Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) / 𝑘) = (seq1( + , 𝐹)‘(⌊‘𝑚))) |
| 150 | 149 | adantr 480 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) / 𝑘) = (seq1( + , 𝐹)‘(⌊‘𝑚))) |
| 151 | 150 | oveq2d 7447 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → ((log‘𝑚) · Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) / 𝑘)) = ((log‘𝑚) · (seq1( + , 𝐹)‘(⌊‘𝑚)))) |
| 152 | 145, 151 | eqtrd 2777 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = ((log‘𝑚) · (seq1( + , 𝐹)‘(⌊‘𝑚)))) |
| 153 | 152 | fveq2d 6910 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) = (abs‘((log‘𝑚) · (seq1( + , 𝐹)‘(⌊‘𝑚))))) |
| 154 | 122 | ad2antlr 727 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (log‘𝑚) ∈
ℝ) |
| 155 | 154 | recnd 11289 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (log‘𝑚) ∈
ℂ) |
| 156 | 83, 155 | sylan 580 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (log‘𝑚) ∈
ℂ) |
| 157 | 156, 75 | absmuld 15493 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) →
(abs‘((log‘𝑚)
· (seq1( + , 𝐹)‘(⌊‘𝑚)))) = ((abs‘(log‘𝑚)) · (abs‘(seq1( +
, 𝐹)‘(⌊‘𝑚))))) |
| 158 | 91, 92 | absidd 15461 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
(abs‘(log‘𝑚)) =
(log‘𝑚)) |
| 159 | 158 | oveq1d 7446 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
((abs‘(log‘𝑚))
· (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))) = ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))))) |
| 160 | 159 | adantr 480 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) →
((abs‘(log‘𝑚))
· (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚)))) = ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))))) |
| 161 | 153, 157,
160 | 3eqtrd 2781 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) = ((log‘𝑚) · (abs‘(seq1( + , 𝐹)‘(⌊‘𝑚))))) |
| 162 | | iftrue 4531 |
. . . . . . . 8
⊢ (𝑆 = 0 → if(𝑆 = 0, 𝐶, 𝐸) = 𝐶) |
| 163 | 162 | adantl 481 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → if(𝑆 = 0, 𝐶, 𝐸) = 𝐶) |
| 164 | 163 | oveq1d 7446 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)) = (𝐶 · ((log‘𝑚) / 𝑚))) |
| 165 | 86 | recnd 11289 |
. . . . . . . 8
⊢ (𝜑 → 𝐶 ∈ ℂ) |
| 166 | 165 | ad2antrr 726 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → 𝐶 ∈ ℂ) |
| 167 | | rpcnne0 13053 |
. . . . . . . 8
⊢ (𝑚 ∈ ℝ+
→ (𝑚 ∈ ℂ
∧ 𝑚 ≠
0)) |
| 168 | 167 | ad2antlr 727 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (𝑚 ∈ ℂ ∧ 𝑚 ≠ 0)) |
| 169 | | div12 11944 |
. . . . . . 7
⊢ ((𝐶 ∈ ℂ ∧
(log‘𝑚) ∈
ℂ ∧ (𝑚 ∈
ℂ ∧ 𝑚 ≠ 0))
→ (𝐶 ·
((log‘𝑚) / 𝑚)) = ((log‘𝑚) · (𝐶 / 𝑚))) |
| 170 | 166, 155,
168, 169 | syl3anc 1373 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (𝐶 · ((log‘𝑚) / 𝑚)) = ((log‘𝑚) · (𝐶 / 𝑚))) |
| 171 | 164, 170 | eqtrd 2777 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑆 = 0) → (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)) = ((log‘𝑚) · (𝐶 / 𝑚))) |
| 172 | 83, 171 | sylan 580 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) → (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)) = ((log‘𝑚) · (𝐶 / 𝑚))) |
| 173 | 115, 161,
172 | 3brtr4d 5175 |
. . 3
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 = 0) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚))) |
| 174 | | dchrvmasumif.2 |
. . . . . 6
⊢ (𝜑 → ∀𝑦 ∈ (3[,)+∞)(abs‘((seq1( + ,
𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦))) |
| 175 | | 2fveq3 6911 |
. . . . . . . . 9
⊢ (𝑦 = 𝑚 → (seq1( + , 𝐾)‘(⌊‘𝑦)) = (seq1( + , 𝐾)‘(⌊‘𝑚))) |
| 176 | 175 | fvoveq1d 7453 |
. . . . . . . 8
⊢ (𝑦 = 𝑚 → (abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) = (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇))) |
| 177 | | fveq2 6906 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑚 → (log‘𝑦) = (log‘𝑚)) |
| 178 | | id 22 |
. . . . . . . . . 10
⊢ (𝑦 = 𝑚 → 𝑦 = 𝑚) |
| 179 | 177, 178 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑦 = 𝑚 → ((log‘𝑦) / 𝑦) = ((log‘𝑚) / 𝑚)) |
| 180 | 179 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑦 = 𝑚 → (𝐸 · ((log‘𝑦) / 𝑦)) = (𝐸 · ((log‘𝑚) / 𝑚))) |
| 181 | 176, 180 | breq12d 5156 |
. . . . . . 7
⊢ (𝑦 = 𝑚 → ((abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦)) ↔ (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) ≤ (𝐸 · ((log‘𝑚) / 𝑚)))) |
| 182 | 181 | rspccva 3621 |
. . . . . 6
⊢
((∀𝑦 ∈
(3[,)+∞)(abs‘((seq1( + , 𝐾)‘(⌊‘𝑦)) − 𝑇)) ≤ (𝐸 · ((log‘𝑦) / 𝑦)) ∧ 𝑚 ∈ (3[,)+∞)) →
(abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) ≤ (𝐸 · ((log‘𝑚) / 𝑚))) |
| 183 | 174, 182 | sylan 580 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
(abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) ≤ (𝐸 · ((log‘𝑚) / 𝑚))) |
| 184 | 183 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) →
(abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) ≤ (𝐸 · ((log‘𝑚) / 𝑚))) |
| 185 | | fveq2 6906 |
. . . . . . . . . . . 12
⊢ (𝑎 = 𝑘 → (log‘𝑎) = (log‘𝑘)) |
| 186 | 185, 53 | oveq12d 7449 |
. . . . . . . . . . 11
⊢ (𝑎 = 𝑘 → ((log‘𝑎) / 𝑎) = ((log‘𝑘) / 𝑘)) |
| 187 | 52, 186 | oveq12d 7449 |
. . . . . . . . . 10
⊢ (𝑎 = 𝑘 → ((𝑋‘(𝐿‘𝑎)) · ((log‘𝑎) / 𝑎)) = ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘))) |
| 188 | | dchrvmasumif.g |
. . . . . . . . . 10
⊢ 𝐾 = (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · ((log‘𝑎) / 𝑎))) |
| 189 | | ovex 7464 |
. . . . . . . . . 10
⊢ ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘)) ∈ V |
| 190 | 187, 188,
189 | fvmpt 7016 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℕ → (𝐾‘𝑘) = ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘))) |
| 191 | 11, 190 | syl 17 |
. . . . . . . 8
⊢ (𝑘 ∈
(1...(⌊‘𝑚))
→ (𝐾‘𝑘) = ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘))) |
| 192 | | ifnefalse 4537 |
. . . . . . . . . . . . 13
⊢ (𝑆 ≠ 0 → if(𝑆 = 0, 𝑚, 𝑘) = 𝑘) |
| 193 | 192 | fveq2d 6910 |
. . . . . . . . . . . 12
⊢ (𝑆 ≠ 0 →
(log‘if(𝑆 = 0, 𝑚, 𝑘)) = (log‘𝑘)) |
| 194 | 193 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑆 ≠ 0 →
((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) = ((log‘𝑘) / 𝑘)) |
| 195 | 194 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑆 ≠ 0 → ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘))) |
| 196 | 195 | adantl 481 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘))) |
| 197 | 196 | eqcomd 2743 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘)) = ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) |
| 198 | 191, 197 | sylan9eqr 2799 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ (𝐾‘𝑘) = ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) |
| 199 | 147 | adantr 480 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) →
(⌊‘𝑚) ∈
(ℤ≥‘1)) |
| 200 | | nnrp 13046 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
| 201 | 200 | adantl 481 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → 𝑘 ∈ ℝ+) |
| 202 | 201 | relogcld 26665 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (log‘𝑘) ∈
ℝ) |
| 203 | 202 | recnd 11289 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (log‘𝑘) ∈
ℂ) |
| 204 | 203, 47, 49 | divcld 12043 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((log‘𝑘) / 𝑘) ∈ ℂ) |
| 205 | 15, 204 | mulcld 11281 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘)) ∈ ℂ) |
| 206 | 187 | cbvmptv 5255 |
. . . . . . . . . . . 12
⊢ (𝑎 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑎)) · ((log‘𝑎) / 𝑎))) = (𝑘 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘))) |
| 207 | 188, 206 | eqtri 2765 |
. . . . . . . . . . 11
⊢ 𝐾 = (𝑘 ∈ ℕ ↦ ((𝑋‘(𝐿‘𝑘)) · ((log‘𝑘) / 𝑘))) |
| 208 | 205, 207 | fmptd 7134 |
. . . . . . . . . 10
⊢ (𝜑 → 𝐾:ℕ⟶ℂ) |
| 209 | 208 | ad2antrr 726 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → 𝐾:ℕ⟶ℂ) |
| 210 | | ffvelcdm 7101 |
. . . . . . . . 9
⊢ ((𝐾:ℕ⟶ℂ ∧
𝑘 ∈ ℕ) →
(𝐾‘𝑘) ∈ ℂ) |
| 211 | 209, 11, 210 | syl2an 596 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ (𝐾‘𝑘) ∈
ℂ) |
| 212 | 198, 211 | eqeltrrd 2842 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ) |
| 213 | 198, 199,
212 | fsumser 15766 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) = (seq1( + , 𝐾)‘(⌊‘𝑚))) |
| 214 | | ifnefalse 4537 |
. . . . . . 7
⊢ (𝑆 ≠ 0 → if(𝑆 = 0, 0, 𝑇) = 𝑇) |
| 215 | 214 | adantl 481 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → if(𝑆 = 0, 0, 𝑇) = 𝑇) |
| 216 | 213, 215 | oveq12d 7449 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → (Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) = ((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇)) |
| 217 | 216 | fveq2d 6910 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) = (abs‘((seq1( + , 𝐾)‘(⌊‘𝑚)) − 𝑇))) |
| 218 | | ifnefalse 4537 |
. . . . . 6
⊢ (𝑆 ≠ 0 → if(𝑆 = 0, 𝐶, 𝐸) = 𝐸) |
| 219 | 218 | adantl 481 |
. . . . 5
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → if(𝑆 = 0, 𝐶, 𝐸) = 𝐸) |
| 220 | 219 | oveq1d 7446 |
. . . 4
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) → (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚)) = (𝐸 · ((log‘𝑚) / 𝑚))) |
| 221 | 184, 217,
220 | 3brtr4d 5175 |
. . 3
⊢ (((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) ∧ 𝑆 ≠ 0) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚))) |
| 222 | 173, 221 | pm2.61dane 3029 |
. 2
⊢ ((𝜑 ∧ 𝑚 ∈ (3[,)+∞)) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (if(𝑆 = 0, 𝐶, 𝐸) · ((log‘𝑚) / 𝑚))) |
| 223 | | fzfid 14014 |
. . . 4
⊢ (𝜑 → (1...2) ∈
Fin) |
| 224 | 7 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → 𝑋 ∈ 𝐷) |
| 225 | | elfzelz 13564 |
. . . . . . . 8
⊢ (𝑘 ∈ (1...2) → 𝑘 ∈
ℤ) |
| 226 | 225 | adantl 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈ ℤ) |
| 227 | 4, 1, 5, 2, 224, 226 | dchrzrhcl 27289 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → (𝑋‘(𝐿‘𝑘)) ∈ ℂ) |
| 228 | 227 | abscld 15475 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → (abs‘(𝑋‘(𝐿‘𝑘))) ∈ ℝ) |
| 229 | | 3rp 13040 |
. . . . . . 7
⊢ 3 ∈
ℝ+ |
| 230 | | relogcl 26617 |
. . . . . . 7
⊢ (3 ∈
ℝ+ → (log‘3) ∈ ℝ) |
| 231 | 229, 230 | ax-mp 5 |
. . . . . 6
⊢
(log‘3) ∈ ℝ |
| 232 | | elfznn 13593 |
. . . . . . 7
⊢ (𝑘 ∈ (1...2) → 𝑘 ∈
ℕ) |
| 233 | 232 | adantl 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈ ℕ) |
| 234 | | nndivre 12307 |
. . . . . 6
⊢
(((log‘3) ∈ ℝ ∧ 𝑘 ∈ ℕ) → ((log‘3) /
𝑘) ∈
ℝ) |
| 235 | 231, 233,
234 | sylancr 587 |
. . . . 5
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → ((log‘3) /
𝑘) ∈
ℝ) |
| 236 | 228, 235 | remulcld 11291 |
. . . 4
⊢ ((𝜑 ∧ 𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) ∈
ℝ) |
| 237 | 223, 236 | fsumrecl 15770 |
. . 3
⊢ (𝜑 → Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) ∈
ℝ) |
| 238 | 43 | abscld 15475 |
. . 3
⊢ (𝜑 → (abs‘if(𝑆 = 0, 0, 𝑇)) ∈ ℝ) |
| 239 | 237, 238 | readdcld 11290 |
. 2
⊢ (𝜑 → (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇))) ∈ ℝ) |
| 240 | | simpl 482 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 𝜑) |
| 241 | 62 | rexri 11319 |
. . . . . . . . . . 11
⊢ 3 ∈
ℝ* |
| 242 | | elico2 13451 |
. . . . . . . . . . 11
⊢ ((1
∈ ℝ ∧ 3 ∈ ℝ*) → (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤ 𝑚 ∧ 𝑚 < 3))) |
| 243 | 107, 241,
242 | mp2an 692 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (1[,)3) ↔ (𝑚 ∈ ℝ ∧ 1 ≤
𝑚 ∧ 𝑚 < 3)) |
| 244 | 243 | simp1bi 1146 |
. . . . . . . . 9
⊢ (𝑚 ∈ (1[,)3) → 𝑚 ∈
ℝ) |
| 245 | 244 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 𝑚 ∈ ℝ) |
| 246 | | 0red 11264 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 ∈
ℝ) |
| 247 | | 1red 11262 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 1 ∈
ℝ) |
| 248 | | 0lt1 11785 |
. . . . . . . . . 10
⊢ 0 <
1 |
| 249 | 248 | a1i 11 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 <
1) |
| 250 | 243 | simp2bi 1147 |
. . . . . . . . . 10
⊢ (𝑚 ∈ (1[,)3) → 1 ≤
𝑚) |
| 251 | 250 | adantl 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 1 ≤ 𝑚) |
| 252 | 246, 247,
245, 249, 251 | ltletrd 11421 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 0 < 𝑚) |
| 253 | 245, 252 | elrpd 13074 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 𝑚 ∈ ℝ+) |
| 254 | 240, 253 | jca 511 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (𝜑 ∧ 𝑚 ∈
ℝ+)) |
| 255 | 43 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → if(𝑆 = 0, 0, 𝑇) ∈ ℂ) |
| 256 | 26, 255 | subcld 11620 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) ∈ ℂ) |
| 257 | 254, 256 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)) ∈ ℂ) |
| 258 | 257 | abscld 15475 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ∈ ℝ) |
| 259 | 254, 26 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ) |
| 260 | 259 | abscld 15475 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
(abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
| 261 | 238 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (abs‘if(𝑆 = 0, 0, 𝑇)) ∈ ℝ) |
| 262 | 260, 261 | readdcld 11290 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
((abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) + (abs‘if(𝑆 = 0, 0, 𝑇))) ∈ ℝ) |
| 263 | 237 | adantr 480 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → Σ𝑘 ∈
(1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) ∈
ℝ) |
| 264 | 263, 261 | readdcld 11290 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (Σ𝑘 ∈
(1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇))) ∈ ℝ) |
| 265 | 26, 255 | abs2dif2d 15497 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ ((abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) + (abs‘if(𝑆 = 0, 0, 𝑇)))) |
| 266 | 254, 265 | syl 17 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ ((abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) + (abs‘if(𝑆 = 0, 0, 𝑇)))) |
| 267 | 25 | abscld 15475 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈
(1...(⌊‘𝑚)))
→ (abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
| 268 | 9, 267 | fsumrecl 15770 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
Σ𝑘 ∈
(1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
| 269 | 254, 268 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → Σ𝑘 ∈
(1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
| 270 | 9, 25 | fsumabs 15837 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))) |
| 271 | 254, 270 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
(abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))) |
| 272 | | fzfid 14014 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → (1...2)
∈ Fin) |
| 273 | 227 | adantlr 715 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (𝑋‘(𝐿‘𝑘)) ∈ ℂ) |
| 274 | 17 | adantr 480 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑚 ∈
ℝ+) |
| 275 | 232 | adantl 481 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈
ℕ) |
| 276 | 275 | nnrpd 13075 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈
ℝ+) |
| 277 | 274, 276 | ifcld 4572 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → if(𝑆 = 0, 𝑚, 𝑘) ∈
ℝ+) |
| 278 | 277 | relogcld 26665 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
(log‘if(𝑆 = 0, 𝑚, 𝑘)) ∈ ℝ) |
| 279 | 278, 275 | nndivred 12320 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ∈ ℝ) |
| 280 | 279 | recnd 11289 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ∈ ℂ) |
| 281 | 273, 280 | mulcld 11281 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ) |
| 282 | 281 | abscld 15475 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
| 283 | 272, 282 | fsumrecl 15770 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
Σ𝑘 ∈
(1...2)(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
| 284 | 254, 283 | syl 17 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → Σ𝑘 ∈
(1...2)(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
| 285 | | fzfid 14014 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (1...2) ∈
Fin) |
| 286 | 254, 281 | sylan 580 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℂ) |
| 287 | 286 | abscld 15475 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
| 288 | 286 | absge0d 15483 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 0 ≤
(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))) |
| 289 | 245 | flcld 13838 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (⌊‘𝑚) ∈
ℤ) |
| 290 | | 2z 12649 |
. . . . . . . . . . 11
⊢ 2 ∈
ℤ |
| 291 | 290 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 2 ∈
ℤ) |
| 292 | 243 | simp3bi 1148 |
. . . . . . . . . . . . . 14
⊢ (𝑚 ∈ (1[,)3) → 𝑚 < 3) |
| 293 | 292 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 𝑚 < 3) |
| 294 | | 3z 12650 |
. . . . . . . . . . . . . 14
⊢ 3 ∈
ℤ |
| 295 | | fllt 13846 |
. . . . . . . . . . . . . 14
⊢ ((𝑚 ∈ ℝ ∧ 3 ∈
ℤ) → (𝑚 < 3
↔ (⌊‘𝑚)
< 3)) |
| 296 | 245, 294,
295 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (𝑚 < 3 ↔ (⌊‘𝑚) < 3)) |
| 297 | 293, 296 | mpbid 232 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (⌊‘𝑚) < 3) |
| 298 | | df-3 12330 |
. . . . . . . . . . . 12
⊢ 3 = (2 +
1) |
| 299 | 297, 298 | breqtrdi 5184 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (⌊‘𝑚) < (2 + 1)) |
| 300 | | rpre 13043 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℝ+
→ 𝑚 ∈
ℝ) |
| 301 | 300 | adantl 481 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) → 𝑚 ∈
ℝ) |
| 302 | 301 | flcld 13838 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(⌊‘𝑚) ∈
ℤ) |
| 303 | | zleltp1 12668 |
. . . . . . . . . . . . 13
⊢
(((⌊‘𝑚)
∈ ℤ ∧ 2 ∈ ℤ) → ((⌊‘𝑚) ≤ 2 ↔
(⌊‘𝑚) < (2 +
1))) |
| 304 | 302, 290,
303 | sylancl 586 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
((⌊‘𝑚) ≤ 2
↔ (⌊‘𝑚)
< (2 + 1))) |
| 305 | 254, 304 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → ((⌊‘𝑚) ≤ 2 ↔
(⌊‘𝑚) < (2 +
1))) |
| 306 | 299, 305 | mpbird 257 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → (⌊‘𝑚) ≤ 2) |
| 307 | | eluz2 12884 |
. . . . . . . . . 10
⊢ (2 ∈
(ℤ≥‘(⌊‘𝑚)) ↔ ((⌊‘𝑚) ∈ ℤ ∧ 2 ∈ ℤ ∧
(⌊‘𝑚) ≤
2)) |
| 308 | 289, 291,
306, 307 | syl3anbrc 1344 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → 2 ∈
(ℤ≥‘(⌊‘𝑚))) |
| 309 | | fzss2 13604 |
. . . . . . . . 9
⊢ (2 ∈
(ℤ≥‘(⌊‘𝑚)) → (1...(⌊‘𝑚)) ⊆
(1...2)) |
| 310 | 308, 309 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
(1...(⌊‘𝑚))
⊆ (1...2)) |
| 311 | 285, 287,
288, 310 | fsumless 15832 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → Σ𝑘 ∈
(1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))) |
| 312 | 236 | adantlr 715 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) ∈
ℝ) |
| 313 | 273, 280 | absmuld 15493 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) = ((abs‘(𝑋‘(𝐿‘𝑘))) · (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))) |
| 314 | 254, 313 | sylan 580 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) = ((abs‘(𝑋‘(𝐿‘𝑘))) · (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)))) |
| 315 | 254, 279 | sylan 580 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ∈ ℝ) |
| 316 | 254, 278 | sylan 580 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (log‘if(𝑆 = 0, 𝑚, 𝑘)) ∈ ℝ) |
| 317 | | log1 26627 |
. . . . . . . . . . . . . 14
⊢
(log‘1) = 0 |
| 318 | | elfzle1 13567 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 ∈ (1...2) → 1 ≤
𝑘) |
| 319 | | breq2 5147 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 = if(𝑆 = 0, 𝑚, 𝑘) → (1 ≤ 𝑚 ↔ 1 ≤ if(𝑆 = 0, 𝑚, 𝑘))) |
| 320 | | breq2 5147 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑘 = if(𝑆 = 0, 𝑚, 𝑘) → (1 ≤ 𝑘 ↔ 1 ≤ if(𝑆 = 0, 𝑚, 𝑘))) |
| 321 | 319, 320 | ifboth 4565 |
. . . . . . . . . . . . . . . 16
⊢ ((1 ≤
𝑚 ∧ 1 ≤ 𝑘) → 1 ≤ if(𝑆 = 0, 𝑚, 𝑘)) |
| 322 | 251, 318,
321 | syl2an 596 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 1 ≤ if(𝑆 = 0, 𝑚, 𝑘)) |
| 323 | | 1rp 13038 |
. . . . . . . . . . . . . . . . 17
⊢ 1 ∈
ℝ+ |
| 324 | | logleb 26645 |
. . . . . . . . . . . . . . . . 17
⊢ ((1
∈ ℝ+ ∧ if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ+) → (1 ≤
if(𝑆 = 0, 𝑚, 𝑘) ↔ (log‘1) ≤
(log‘if(𝑆 = 0, 𝑚, 𝑘)))) |
| 325 | 323, 277,
324 | sylancr 587 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (1 ≤
if(𝑆 = 0, 𝑚, 𝑘) ↔ (log‘1) ≤
(log‘if(𝑆 = 0, 𝑚, 𝑘)))) |
| 326 | 254, 325 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (1 ≤ if(𝑆 = 0, 𝑚, 𝑘) ↔ (log‘1) ≤
(log‘if(𝑆 = 0, 𝑚, 𝑘)))) |
| 327 | 322, 326 | mpbid 232 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (log‘1) ≤
(log‘if(𝑆 = 0, 𝑚, 𝑘))) |
| 328 | 317, 327 | eqbrtrrid 5179 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 0 ≤
(log‘if(𝑆 = 0, 𝑚, 𝑘))) |
| 329 | 276 | rpregt0d 13083 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → (𝑘 ∈ ℝ ∧ 0 <
𝑘)) |
| 330 | 254, 329 | sylan 580 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (𝑘 ∈ ℝ ∧ 0 < 𝑘)) |
| 331 | | divge0 12137 |
. . . . . . . . . . . . 13
⊢
((((log‘if(𝑆 =
0, 𝑚, 𝑘)) ∈ ℝ ∧ 0 ≤
(log‘if(𝑆 = 0, 𝑚, 𝑘))) ∧ (𝑘 ∈ ℝ ∧ 0 < 𝑘)) → 0 ≤
((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) |
| 332 | 316, 328,
330, 331 | syl21anc 838 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 0 ≤
((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) |
| 333 | 315, 332 | absidd 15461 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) →
(abs‘((log‘if(𝑆
= 0, 𝑚, 𝑘)) / 𝑘)) = ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) |
| 334 | 333, 315 | eqeltrd 2841 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) →
(abs‘((log‘if(𝑆
= 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℝ) |
| 335 | 235 | adantlr 715 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((log‘3) /
𝑘) ∈
ℝ) |
| 336 | 228 | adantlr 715 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
(abs‘(𝑋‘(𝐿‘𝑘))) ∈ ℝ) |
| 337 | 273 | absge0d 15483 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 0 ≤
(abs‘(𝑋‘(𝐿‘𝑘)))) |
| 338 | 336, 337 | jca 511 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
((abs‘(𝑋‘(𝐿‘𝑘))) ∈ ℝ ∧ 0 ≤
(abs‘(𝑋‘(𝐿‘𝑘))))) |
| 339 | 254, 338 | sylan 580 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿‘𝑘))) ∈ ℝ ∧ 0 ≤
(abs‘(𝑋‘(𝐿‘𝑘))))) |
| 340 | 292 | ad2antlr 727 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 𝑚 < 3) |
| 341 | 275 | nnred 12281 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 ∈
ℝ) |
| 342 | | 2re 12340 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℝ |
| 343 | 342 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 2 ∈
ℝ) |
| 344 | 62 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 3 ∈
ℝ) |
| 345 | | elfzle2 13568 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 ∈ (1...2) → 𝑘 ≤ 2) |
| 346 | 345 | adantl 481 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 ≤ 2) |
| 347 | | 2lt3 12438 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 <
3 |
| 348 | 347 | a1i 11 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 2 <
3) |
| 349 | 341, 343,
344, 346, 348 | lelttrd 11419 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → 𝑘 < 3) |
| 350 | 254, 349 | sylan 580 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → 𝑘 < 3) |
| 351 | | breq1 5146 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 = if(𝑆 = 0, 𝑚, 𝑘) → (𝑚 < 3 ↔ if(𝑆 = 0, 𝑚, 𝑘) < 3)) |
| 352 | | breq1 5146 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = if(𝑆 = 0, 𝑚, 𝑘) → (𝑘 < 3 ↔ if(𝑆 = 0, 𝑚, 𝑘) < 3)) |
| 353 | 351, 352 | ifboth 4565 |
. . . . . . . . . . . . . . 15
⊢ ((𝑚 < 3 ∧ 𝑘 < 3) → if(𝑆 = 0, 𝑚, 𝑘) < 3) |
| 354 | 340, 350,
353 | syl2anc 584 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → if(𝑆 = 0, 𝑚, 𝑘) < 3) |
| 355 | 277 | rpred 13077 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) → if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ) |
| 356 | | ltle 11349 |
. . . . . . . . . . . . . . . 16
⊢
((if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ ∧ 3 ∈ ℝ)
→ (if(𝑆 = 0, 𝑚, 𝑘) < 3 → if(𝑆 = 0, 𝑚, 𝑘) ≤ 3)) |
| 357 | 355, 62, 356 | sylancl 586 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
(if(𝑆 = 0, 𝑚, 𝑘) < 3 → if(𝑆 = 0, 𝑚, 𝑘) ≤ 3)) |
| 358 | 254, 357 | sylan 580 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (if(𝑆 = 0, 𝑚, 𝑘) < 3 → if(𝑆 = 0, 𝑚, 𝑘) ≤ 3)) |
| 359 | 354, 358 | mpd 15 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → if(𝑆 = 0, 𝑚, 𝑘) ≤ 3) |
| 360 | | logleb 26645 |
. . . . . . . . . . . . . . 15
⊢
((if(𝑆 = 0, 𝑚, 𝑘) ∈ ℝ+ ∧ 3 ∈
ℝ+) → (if(𝑆 = 0, 𝑚, 𝑘) ≤ 3 ↔ (log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3))) |
| 361 | 277, 229,
360 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
(if(𝑆 = 0, 𝑚, 𝑘) ≤ 3 ↔ (log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3))) |
| 362 | 254, 361 | sylan 580 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (if(𝑆 = 0, 𝑚, 𝑘) ≤ 3 ↔ (log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3))) |
| 363 | 359, 362 | mpbid 232 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3)) |
| 364 | 231 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
(log‘3) ∈ ℝ) |
| 365 | 278, 364,
276 | lediv1d 13123 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑚 ∈ ℝ+) ∧ 𝑘 ∈ (1...2)) →
((log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3) ↔
((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ≤ ((log‘3) / 𝑘))) |
| 366 | 254, 365 | sylan 580 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) ≤ (log‘3) ↔
((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ≤ ((log‘3) / 𝑘))) |
| 367 | 363, 366 | mpbid 232 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘) ≤ ((log‘3) / 𝑘)) |
| 368 | 333, 367 | eqbrtrd 5165 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) →
(abs‘((log‘if(𝑆
= 0, 𝑚, 𝑘)) / 𝑘)) ≤ ((log‘3) / 𝑘)) |
| 369 | | lemul2a 12122 |
. . . . . . . . . 10
⊢
((((abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ∈ ℝ ∧ ((log‘3) /
𝑘) ∈ ℝ ∧
((abs‘(𝑋‘(𝐿‘𝑘))) ∈ ℝ ∧ 0 ≤
(abs‘(𝑋‘(𝐿‘𝑘))))) ∧ (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) ≤ ((log‘3) / 𝑘)) → ((abs‘(𝑋‘(𝐿‘𝑘))) · (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ ((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘))) |
| 370 | 334, 335,
339, 368, 369 | syl31anc 1375 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → ((abs‘(𝑋‘(𝐿‘𝑘))) · (abs‘((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ ((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘))) |
| 371 | 314, 370 | eqbrtrd 5165 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑚 ∈ (1[,)3)) ∧ 𝑘 ∈ (1...2)) → (abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ ((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘))) |
| 372 | 285, 287,
312, 371 | fsumle 15835 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → Σ𝑘 ∈
(1...2)(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘))) |
| 373 | 269, 284,
263, 311, 372 | letrd 11418 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) → Σ𝑘 ∈
(1...(⌊‘𝑚))(abs‘((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘))) |
| 374 | 260, 269,
263, 271, 373 | letrd 11418 |
. . . . 5
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
(abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ≤ Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘))) |
| 375 | 26 | abscld 15475 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) ∈ ℝ) |
| 376 | 237 | adantr 480 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
Σ𝑘 ∈
(1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) ∈
ℝ) |
| 377 | 255 | abscld 15475 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑚 ∈ ℝ+) →
(abs‘if(𝑆 = 0, 0,
𝑇)) ∈
ℝ) |
| 378 | 375, 376,
377 | leadd1d 11857 |
. . . . . 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, 𝑇))))) |
| 379 | 254, 378 | 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, 𝑇))))) |
| 380 | 374, 379 | mpbid 232 |
. . . 4
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
((abs‘Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘))) + (abs‘if(𝑆 = 0, 0, 𝑇))) ≤ (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇)))) |
| 381 | 258, 262,
264, 266, 380 | letrd 11418 |
. . 3
⊢ ((𝜑 ∧ 𝑚 ∈ (1[,)3)) →
(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇)))) |
| 382 | 381 | ralrimiva 3146 |
. 2
⊢ (𝜑 → ∀𝑚 ∈ (1[,)3)(abs‘(Σ𝑘 ∈
(1...(⌊‘𝑚))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, 𝑚, 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇))) ≤ (Σ𝑘 ∈ (1...2)((abs‘(𝑋‘(𝐿‘𝑘))) · ((log‘3) / 𝑘)) + (abs‘if(𝑆 = 0, 0, 𝑇)))) |
| 383 | 1, 2, 3, 4, 5, 6, 7, 8, 26, 34, 37, 43, 222, 239, 382 | dchrvmasumlem3 27543 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑑 ∈
(1...(⌊‘𝑥))(((𝑋‘(𝐿‘𝑑)) · ((μ‘𝑑) / 𝑑)) · (Σ𝑘 ∈ (1...(⌊‘(𝑥 / 𝑑)))((𝑋‘(𝐿‘𝑘)) · ((log‘if(𝑆 = 0, (𝑥 / 𝑑), 𝑘)) / 𝑘)) − if(𝑆 = 0, 0, 𝑇)))) ∈ 𝑂(1)) |