| Step | Hyp | Ref
| Expression |
| 1 | | rpvmasum.a |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
| 2 | 1 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
ℕ) |
| 3 | | rpvmasum2.g |
. . . . . . 7
⊢ 𝐺 = (DChr‘𝑁) |
| 4 | | rpvmasum2.d |
. . . . . . 7
⊢ 𝐷 = (Base‘𝐺) |
| 5 | 3, 4 | dchrfi 27299 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin) |
| 6 | 2, 5 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈ Fin) |
| 7 | | fzfid 14014 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (1...(⌊‘𝑥)) ∈ Fin) |
| 8 | | rpvmasum.z |
. . . . . . . . . . . . 13
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
| 9 | | eqid 2737 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑍) =
(Base‘𝑍) |
| 10 | | simpr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑓 ∈ 𝐷) |
| 11 | 3, 8, 4, 9, 10 | dchrf 27286 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑓:(Base‘𝑍)⟶ℂ) |
| 12 | | rpvmasum2.u |
. . . . . . . . . . . . . . 15
⊢ 𝑈 = (Unit‘𝑍) |
| 13 | 9, 12 | unitss 20376 |
. . . . . . . . . . . . . 14
⊢ 𝑈 ⊆ (Base‘𝑍) |
| 14 | | rpvmasum2.b |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
| 15 | 13, 14 | sselid 3981 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ (Base‘𝑍)) |
| 16 | 15 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝐴 ∈ (Base‘𝑍)) |
| 17 | 11, 16 | ffvelcdmd 7105 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓‘𝐴) ∈ ℂ) |
| 18 | 17 | cjcld 15235 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (∗‘(𝑓‘𝐴)) ∈ ℂ) |
| 19 | 18 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (∗‘(𝑓‘𝐴)) ∈ ℂ) |
| 20 | 19 | adantrl 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑓 ∈ 𝐷)) → (∗‘(𝑓‘𝐴)) ∈ ℂ) |
| 21 | 11 | ad4ant14 752 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → 𝑓:(Base‘𝑍)⟶ℂ) |
| 22 | 1 | nnnn0d 12587 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
| 23 | | rpvmasum.l |
. . . . . . . . . . . . . . . 16
⊢ 𝐿 = (ℤRHom‘𝑍) |
| 24 | 8, 9, 23 | znzrhfo 21566 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→(Base‘𝑍)) |
| 25 | | fof 6820 |
. . . . . . . . . . . . . . 15
⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍)) |
| 26 | 22, 24, 25 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍)) |
| 27 | 26 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐿:ℤ⟶(Base‘𝑍)) |
| 28 | | elfzelz 13564 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℤ) |
| 29 | | ffvelcdm 7101 |
. . . . . . . . . . . . 13
⊢ ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑛 ∈ ℤ) → (𝐿‘𝑛) ∈ (Base‘𝑍)) |
| 30 | 27, 28, 29 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝐿‘𝑛) ∈ (Base‘𝑍)) |
| 31 | 30 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → (𝐿‘𝑛) ∈ (Base‘𝑍)) |
| 32 | 21, 31 | ffvelcdmd 7105 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → (𝑓‘(𝐿‘𝑛)) ∈ ℂ) |
| 33 | 32 | anasss 466 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑓 ∈ 𝐷)) → (𝑓‘(𝐿‘𝑛)) ∈ ℂ) |
| 34 | | elfznn 13593 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
| 35 | 34 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
| 36 | | vmacl 27161 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
| 37 | 35, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
| 38 | 37, 35 | nndivred 12320 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℝ) |
| 39 | 38 | recnd 11289 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℂ) |
| 40 | 39 | adantrr 717 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑓 ∈ 𝐷)) → ((Λ‘𝑛) / 𝑛) ∈ ℂ) |
| 41 | 33, 40 | mulcld 11281 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑓 ∈ 𝐷)) → ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
| 42 | 20, 41 | mulcld 11281 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑓 ∈ 𝐷)) →
((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ ℂ) |
| 43 | 42 | anass1rs 655 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ ℂ) |
| 44 | 7, 43 | fsumcl 15769 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ ℂ) |
| 45 | | relogcl 26617 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
| 46 | 45 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℝ) |
| 47 | 46 | recnd 11289 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℂ) |
| 48 | 47 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (log‘𝑥) ∈ ℂ) |
| 49 | | ax-1cn 11213 |
. . . . . . 7
⊢ 1 ∈
ℂ |
| 50 | | neg1cn 12380 |
. . . . . . . 8
⊢ -1 ∈
ℂ |
| 51 | | 0cn 11253 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
| 52 | 50, 51 | ifcli 4573 |
. . . . . . 7
⊢ if(𝑓 ∈ 𝑊, -1, 0) ∈ ℂ |
| 53 | 49, 52 | ifcli 4573 |
. . . . . 6
⊢ if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)) ∈ ℂ |
| 54 | | mulcl 11239 |
. . . . . 6
⊢
(((log‘𝑥)
∈ ℂ ∧ if(𝑓 =
1 , 1,
if(𝑓 ∈ 𝑊, -1, 0)) ∈ ℂ) →
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) ∈ ℂ) |
| 55 | 48, 53, 54 | sylancl 586 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) ∈ ℂ) |
| 56 | 6, 44, 55 | fsumsub 15824 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ 𝐷 (Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑓 ∈ 𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − Σ𝑓 ∈ 𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
| 57 | 41 | anass1rs 655 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
| 58 | 7, 57 | fsumcl 15769 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
| 59 | 19, 58, 55 | subdid 11719 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (((∗‘(𝑓‘𝐴)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((∗‘(𝑓‘𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))))) |
| 60 | 7, 19, 57 | fsummulc2 15820 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
| 61 | 53 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)) ∈ ℂ) |
| 62 | 19, 48, 61 | mul12d 11470 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = ((log‘𝑥) · ((∗‘(𝑓‘𝐴)) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
| 63 | | ovif2 7532 |
. . . . . . . . . 10
⊢
((∗‘(𝑓‘𝐴)) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = if(𝑓 = 1 , ((∗‘(𝑓‘𝐴)) · 1), ((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0))) |
| 64 | | fveq1 6905 |
. . . . . . . . . . . . . . . 16
⊢ (𝑓 = 1 → (𝑓‘𝐴) = ( 1 ‘𝐴)) |
| 65 | | rpvmasum2.1 |
. . . . . . . . . . . . . . . . 17
⊢ 1 =
(0g‘𝐺) |
| 66 | 1 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → 𝑁 ∈ ℕ) |
| 67 | 14 | ad2antrr 726 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → 𝐴 ∈ 𝑈) |
| 68 | 3, 8, 65, 12, 66, 67 | dchr1 27301 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ( 1 ‘𝐴) = 1) |
| 69 | 64, 68 | sylan9eqr 2799 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) → (𝑓‘𝐴) = 1) |
| 70 | 69 | fveq2d 6910 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) →
(∗‘(𝑓‘𝐴)) = (∗‘1)) |
| 71 | | 1re 11261 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
| 72 | | cjre 15178 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℝ → (∗‘1) = 1) |
| 73 | 71, 72 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(∗‘1) = 1 |
| 74 | 70, 73 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) →
(∗‘(𝑓‘𝐴)) = 1) |
| 75 | 74 | oveq1d 7446 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) →
((∗‘(𝑓‘𝐴)) · 1) = (1 ·
1)) |
| 76 | | 1t1e1 12428 |
. . . . . . . . . . . 12
⊢ (1
· 1) = 1 |
| 77 | 75, 76 | eqtrdi 2793 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) →
((∗‘(𝑓‘𝐴)) · 1) = 1) |
| 78 | | df-ne 2941 |
. . . . . . . . . . . 12
⊢ (𝑓 ≠ 1 ↔ ¬ 𝑓 = 1 ) |
| 79 | | ovif2 7532 |
. . . . . . . . . . . . 13
⊢
((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0)) = if(𝑓 ∈ 𝑊, ((∗‘(𝑓‘𝐴)) · -1), ((∗‘(𝑓‘𝐴)) · 0)) |
| 80 | | rpvmasum2.z1 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑊) → 𝐴 = (1r‘𝑍)) |
| 81 | 80 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑊) → (𝑓‘𝐴) = (𝑓‘(1r‘𝑍))) |
| 82 | 81 | ad5ant15 759 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → (𝑓‘𝐴) = (𝑓‘(1r‘𝑍))) |
| 83 | 3, 8, 4 | dchrmhm 27285 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) |
| 84 | | simpr 484 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → 𝑓 ∈ 𝐷) |
| 85 | 83, 84 | sselid 3981 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → 𝑓 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
| 86 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
| 87 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1r‘𝑍) = (1r‘𝑍) |
| 88 | 86, 87 | ringidval 20180 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(1r‘𝑍) = (0g‘(mulGrp‘𝑍)) |
| 89 | | eqid 2737 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
| 90 | | cnfld1 21406 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 =
(1r‘ℂfld) |
| 91 | 89, 90 | ringidval 20180 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) |
| 92 | 88, 91 | mhm0 18807 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑓 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) → (𝑓‘(1r‘𝑍)) = 1) |
| 93 | 85, 92 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (𝑓‘(1r‘𝑍)) = 1) |
| 94 | 93 | ad2antrr 726 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → (𝑓‘(1r‘𝑍)) = 1) |
| 95 | 82, 94 | eqtrd 2777 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → (𝑓‘𝐴) = 1) |
| 96 | 95 | fveq2d 6910 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → (∗‘(𝑓‘𝐴)) = (∗‘1)) |
| 97 | 96, 73 | eqtrdi 2793 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → (∗‘(𝑓‘𝐴)) = 1) |
| 98 | 97 | oveq1d 7446 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → ((∗‘(𝑓‘𝐴)) · -1) = (1 ·
-1)) |
| 99 | 50 | mullidi 11266 |
. . . . . . . . . . . . . . . 16
⊢ (1
· -1) = -1 |
| 100 | 98, 99 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → ((∗‘(𝑓‘𝐴)) · -1) = -1) |
| 101 | 100 | ifeq1da 4557 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → if(𝑓 ∈ 𝑊, ((∗‘(𝑓‘𝐴)) · -1), ((∗‘(𝑓‘𝐴)) · 0)) = if(𝑓 ∈ 𝑊, -1, ((∗‘(𝑓‘𝐴)) · 0))) |
| 102 | 19 | adantr 480 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) →
(∗‘(𝑓‘𝐴)) ∈ ℂ) |
| 103 | 102 | mul01d 11460 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) →
((∗‘(𝑓‘𝐴)) · 0) = 0) |
| 104 | 103 | ifeq2d 4546 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → if(𝑓 ∈ 𝑊, -1, ((∗‘(𝑓‘𝐴)) · 0)) = if(𝑓 ∈ 𝑊, -1, 0)) |
| 105 | 101, 104 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → if(𝑓 ∈ 𝑊, ((∗‘(𝑓‘𝐴)) · -1), ((∗‘(𝑓‘𝐴)) · 0)) = if(𝑓 ∈ 𝑊, -1, 0)) |
| 106 | 79, 105 | eqtrid 2789 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) →
((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0)) = if(𝑓 ∈ 𝑊, -1, 0)) |
| 107 | 78, 106 | sylan2br 595 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ ¬ 𝑓 = 1 ) →
((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0)) = if(𝑓 ∈ 𝑊, -1, 0)) |
| 108 | 77, 107 | ifeq12da 4559 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → if(𝑓 = 1 , ((∗‘(𝑓‘𝐴)) · 1), ((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0))) = if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) |
| 109 | 63, 108 | eqtrid 2789 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) |
| 110 | 109 | oveq2d 7447 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((log‘𝑥) · ((∗‘(𝑓‘𝐴)) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) |
| 111 | 62, 110 | eqtrd 2777 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) |
| 112 | 60, 111 | oveq12d 7449 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (((∗‘(𝑓‘𝐴)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((∗‘(𝑓‘𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
| 113 | 59, 112 | eqtrd 2777 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
| 114 | 113 | sumeq2dv 15738 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = Σ𝑓 ∈ 𝐷 (Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
| 115 | | fzfid 14014 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘𝑥))
∈ Fin) |
| 116 | | inss1 4237 |
. . . . . . . . 9
⊢
((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥)) |
| 117 | | ssfi 9213 |
. . . . . . . . 9
⊢
(((1...(⌊‘𝑥)) ∈ Fin ∧
((1...(⌊‘𝑥))
∩ 𝑇) ⊆
(1...(⌊‘𝑥)))
→ ((1...(⌊‘𝑥)) ∩ 𝑇) ∈ Fin) |
| 118 | 115, 116,
117 | sylancl 586 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((1...(⌊‘𝑥))
∩ 𝑇) ∈
Fin) |
| 119 | 2 | phicld 16809 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(ϕ‘𝑁) ∈
ℕ) |
| 120 | 119 | nncnd 12282 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(ϕ‘𝑁) ∈
ℂ) |
| 121 | 116 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((1...(⌊‘𝑥))
∩ 𝑇) ⊆
(1...(⌊‘𝑥))) |
| 122 | 121 | sselda 3983 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)) → 𝑛 ∈
(1...(⌊‘𝑥))) |
| 123 | 122, 39 | syldan 591 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)) →
((Λ‘𝑛) / 𝑛) ∈
ℂ) |
| 124 | 118, 120,
123 | fsummulc2 15820 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛))) |
| 125 | 120 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ϕ‘𝑁)
∈ ℂ) |
| 126 | 125, 39 | mulcld 11281 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ϕ‘𝑁)
· ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
| 127 | 122, 126 | syldan 591 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)) →
((ϕ‘𝑁) ·
((Λ‘𝑛) / 𝑛)) ∈
ℂ) |
| 128 | 127 | ralrimiva 3146 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∀𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
| 129 | 115 | olcd 875 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((1...(⌊‘𝑥))
⊆ (ℤ≥‘1) ∨ (1...(⌊‘𝑥)) ∈ Fin)) |
| 130 | | sumss2 15762 |
. . . . . . . 8
⊢
(((((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥)) ∧ ∀𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) ∧
((1...(⌊‘𝑥))
⊆ (ℤ≥‘1) ∨ (1...(⌊‘𝑥)) ∈ Fin)) →
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0)) |
| 131 | 121, 128,
129, 130 | syl21anc 838 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0)) |
| 132 | | elin 3967 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇) ↔ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ 𝑇)) |
| 133 | 132 | baib 535 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ (𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇) ↔ 𝑛 ∈ 𝑇)) |
| 134 | 133 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇) ↔ 𝑛 ∈ 𝑇)) |
| 135 | | rpvmasum2.t |
. . . . . . . . . . . . 13
⊢ 𝑇 = (◡𝐿 “ {𝐴}) |
| 136 | 135 | eleq2i 2833 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑇 ↔ 𝑛 ∈ (◡𝐿 “ {𝐴})) |
| 137 | 27 | ffnd 6737 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐿 Fn ℤ) |
| 138 | | fniniseg 7080 |
. . . . . . . . . . . . . 14
⊢ (𝐿 Fn ℤ → (𝑛 ∈ (◡𝐿 “ {𝐴}) ↔ (𝑛 ∈ ℤ ∧ (𝐿‘𝑛) = 𝐴))) |
| 139 | 138 | baibd 539 |
. . . . . . . . . . . . 13
⊢ ((𝐿 Fn ℤ ∧ 𝑛 ∈ ℤ) → (𝑛 ∈ (◡𝐿 “ {𝐴}) ↔ (𝐿‘𝑛) = 𝐴)) |
| 140 | 137, 28, 139 | syl2an 596 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ∈ (◡𝐿 “ {𝐴}) ↔ (𝐿‘𝑛) = 𝐴)) |
| 141 | 136, 140 | bitrid 283 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ∈ 𝑇 ↔ (𝐿‘𝑛) = 𝐴)) |
| 142 | 134, 141 | bitr2d 280 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝐿‘𝑛) = 𝐴 ↔ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇))) |
| 143 | 39 | mul02d 11459 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (0 · ((Λ‘𝑛) / 𝑛)) = 0) |
| 144 | 142, 143 | ifbieq2d 4552 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ if((𝐿‘𝑛) = 𝐴, ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), (0 · ((Λ‘𝑛) / 𝑛))) = if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0)) |
| 145 | | ovif 7531 |
. . . . . . . . . 10
⊢
(if((𝐿‘𝑛) = 𝐴, (ϕ‘𝑁), 0) · ((Λ‘𝑛) / 𝑛)) = if((𝐿‘𝑛) = 𝐴, ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), (0 · ((Λ‘𝑛) / 𝑛))) |
| 146 | 1 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑁 ∈
ℕ) |
| 147 | 146, 5 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝐷 ∈
Fin) |
| 148 | 18 | ad4ant14 752 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → (∗‘(𝑓‘𝐴)) ∈ ℂ) |
| 149 | 32, 148 | mulcld 11281 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → ((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) ∈ ℂ) |
| 150 | 147, 39, 149 | fsummulc1 15821 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑓 ∈
𝐷 ((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑓 ∈ 𝐷 (((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛))) |
| 151 | 14 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝐴 ∈ 𝑈) |
| 152 | 3, 4, 8, 9, 12, 146, 30, 151 | sum2dchr 27318 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑓 ∈
𝐷 ((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) = if((𝐿‘𝑛) = 𝐴, (ϕ‘𝑁), 0)) |
| 153 | 152 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑓 ∈
𝐷 ((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = (if((𝐿‘𝑛) = 𝐴, (ϕ‘𝑁), 0) · ((Λ‘𝑛) / 𝑛))) |
| 154 | 39 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → ((Λ‘𝑛) / 𝑛) ∈ ℂ) |
| 155 | | mulass 11243 |
. . . . . . . . . . . . . 14
⊢ (((𝑓‘(𝐿‘𝑛)) ∈ ℂ ∧
(∗‘(𝑓‘𝐴)) ∈ ℂ ∧
((Λ‘𝑛) / 𝑛) ∈ ℂ) →
(((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = ((𝑓‘(𝐿‘𝑛)) · ((∗‘(𝑓‘𝐴)) · ((Λ‘𝑛) / 𝑛)))) |
| 156 | | mul12 11426 |
. . . . . . . . . . . . . 14
⊢ (((𝑓‘(𝐿‘𝑛)) ∈ ℂ ∧
(∗‘(𝑓‘𝐴)) ∈ ℂ ∧
((Λ‘𝑛) / 𝑛) ∈ ℂ) → ((𝑓‘(𝐿‘𝑛)) · ((∗‘(𝑓‘𝐴)) · ((Λ‘𝑛) / 𝑛))) = ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
| 157 | 155, 156 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (((𝑓‘(𝐿‘𝑛)) ∈ ℂ ∧
(∗‘(𝑓‘𝐴)) ∈ ℂ ∧
((Λ‘𝑛) / 𝑛) ∈ ℂ) →
(((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
| 158 | 32, 148, 154, 157 | syl3anc 1373 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → (((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
| 159 | 158 | sumeq2dv 15738 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑓 ∈
𝐷 (((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
| 160 | 150, 153,
159 | 3eqtr3d 2785 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (if((𝐿‘𝑛) = 𝐴, (ϕ‘𝑁), 0) · ((Λ‘𝑛) / 𝑛)) = Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
| 161 | 145, 160 | eqtr3id 2791 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ if((𝐿‘𝑛) = 𝐴, ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), (0 · ((Λ‘𝑛) / 𝑛))) = Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
| 162 | 144, 161 | eqtr3d 2779 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ if(𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇),
((ϕ‘𝑁) ·
((Λ‘𝑛) / 𝑛)), 0) = Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
| 163 | 162 | sumeq2dv 15738 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
| 164 | 124, 131,
163 | 3eqtrd 2781 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
| 165 | 115, 6, 42 | fsumcom 15811 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) = Σ𝑓 ∈ 𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
| 166 | 164, 165 | eqtrd 2777 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) = Σ𝑓 ∈ 𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
| 167 | 3 | dchrabl 27298 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) |
| 168 | | ablgrp 19803 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
| 169 | 4, 65 | grpidcl 18983 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp → 1 ∈ 𝐷) |
| 170 | 2, 167, 168, 169 | 4syl 19 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 1 ∈ 𝐷) |
| 171 | 47 | mulridd 11278 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · 1)
= (log‘𝑥)) |
| 172 | 171, 47 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · 1)
∈ ℂ) |
| 173 | | iftrue 4531 |
. . . . . . . . . . 11
⊢ (𝑓 = 1 → if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)) = 1) |
| 174 | 173 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑓 = 1 → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = ((log‘𝑥) · 1)) |
| 175 | 174 | sumsn 15782 |
. . . . . . . . 9
⊢ (( 1 ∈ 𝐷 ∧ ((log‘𝑥) · 1) ∈ ℂ)
→ Σ𝑓 ∈ {
1 }
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = ((log‘𝑥) · 1)) |
| 176 | 170, 172,
175 | syl2anc 584 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ { 1 }
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = ((log‘𝑥) · 1)) |
| 177 | | eldifsn 4786 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (𝐷 ∖ { 1 }) ↔ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) |
| 178 | | ifnefalse 4537 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ≠ 1 → if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)) = if(𝑓 ∈ 𝑊, -1, 0)) |
| 179 | 178 | ad2antll 729 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) → if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)) = if(𝑓 ∈ 𝑊, -1, 0)) |
| 180 | | negeq 11500 |
. . . . . . . . . . . . . . 15
⊢ (if(𝑓 ∈ 𝑊, 1, 0) = 1 → -if(𝑓 ∈ 𝑊, 1, 0) = -1) |
| 181 | | negeq 11500 |
. . . . . . . . . . . . . . . 16
⊢ (if(𝑓 ∈ 𝑊, 1, 0) = 0 → -if(𝑓 ∈ 𝑊, 1, 0) = -0) |
| 182 | | neg0 11555 |
. . . . . . . . . . . . . . . 16
⊢ -0 =
0 |
| 183 | 181, 182 | eqtrdi 2793 |
. . . . . . . . . . . . . . 15
⊢ (if(𝑓 ∈ 𝑊, 1, 0) = 0 → -if(𝑓 ∈ 𝑊, 1, 0) = 0) |
| 184 | 180, 183 | ifsb 4539 |
. . . . . . . . . . . . . 14
⊢ -if(𝑓 ∈ 𝑊, 1, 0) = if(𝑓 ∈ 𝑊, -1, 0) |
| 185 | 179, 184 | eqtr4di 2795 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) → if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)) = -if(𝑓 ∈ 𝑊, 1, 0)) |
| 186 | 185 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) →
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = ((log‘𝑥) · -if(𝑓 ∈ 𝑊, 1, 0))) |
| 187 | 47 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) → (log‘𝑥) ∈
ℂ) |
| 188 | 49, 51 | ifcli 4573 |
. . . . . . . . . . . . 13
⊢ if(𝑓 ∈ 𝑊, 1, 0) ∈ ℂ |
| 189 | | mulneg2 11700 |
. . . . . . . . . . . . 13
⊢
(((log‘𝑥)
∈ ℂ ∧ if(𝑓
∈ 𝑊, 1, 0) ∈
ℂ) → ((log‘𝑥) · -if(𝑓 ∈ 𝑊, 1, 0)) = -((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
| 190 | 187, 188,
189 | sylancl 586 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) →
((log‘𝑥) ·
-if(𝑓 ∈ 𝑊, 1, 0)) = -((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
| 191 | 186, 190 | eqtrd 2777 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) →
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = -((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
| 192 | 177, 191 | sylan2b 594 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) →
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = -((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
| 193 | 192 | sumeq2dv 15738 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = Σ𝑓 ∈ (𝐷 ∖ { 1 })-((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
| 194 | | diffi 9215 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ Fin → (𝐷 ∖ { 1 }) ∈
Fin) |
| 195 | 6, 194 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝐷 ∖ { 1 }) ∈
Fin) |
| 196 | 47 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) →
(log‘𝑥) ∈
ℂ) |
| 197 | | mulcl 11239 |
. . . . . . . . . . 11
⊢
(((log‘𝑥)
∈ ℂ ∧ if(𝑓
∈ 𝑊, 1, 0) ∈
ℂ) → ((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0)) ∈ ℂ) |
| 198 | 196, 188,
197 | sylancl 586 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) →
((log‘𝑥) ·
if(𝑓 ∈ 𝑊, 1, 0)) ∈
ℂ) |
| 199 | 195, 198 | fsumneg 15823 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ (𝐷 ∖ { 1 })-((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0)) = -Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
| 200 | 188 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) → if(𝑓 ∈ 𝑊, 1, 0) ∈ ℂ) |
| 201 | 195, 47, 200 | fsummulc2 15820 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) ·
Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓 ∈ 𝑊, 1, 0)) = Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
| 202 | | rpvmasum2.w |
. . . . . . . . . . . . . . . . 17
⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} |
| 203 | 202 | ssrab3 4082 |
. . . . . . . . . . . . . . . 16
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
| 204 | | difss 4136 |
. . . . . . . . . . . . . . . 16
⊢ (𝐷 ∖ { 1 }) ⊆ 𝐷 |
| 205 | 203, 204 | sstri 3993 |
. . . . . . . . . . . . . . 15
⊢ 𝑊 ⊆ 𝐷 |
| 206 | | ssfi 9213 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ Fin ∧ 𝑊 ⊆ 𝐷) → 𝑊 ∈ Fin) |
| 207 | 6, 205, 206 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑊 ∈ Fin) |
| 208 | | fsumconst 15826 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Fin ∧ 1 ∈
ℂ) → Σ𝑓
∈ 𝑊 1 =
((♯‘𝑊) ·
1)) |
| 209 | 207, 49, 208 | sylancl 586 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ 𝑊 1 = ((♯‘𝑊) · 1)) |
| 210 | 203 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑊 ⊆ (𝐷 ∖ { 1 })) |
| 211 | 49 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℂ) |
| 212 | 211 | ralrimivw 3150 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∀𝑓 ∈ 𝑊 1 ∈
ℂ) |
| 213 | 195 | olcd 875 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝐷 ∖ { 1 }) ⊆
(ℤ≥‘1) ∨ (𝐷 ∖ { 1 }) ∈
Fin)) |
| 214 | | sumss2 15762 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ⊆ (𝐷 ∖ { 1 }) ∧ ∀𝑓 ∈ 𝑊 1 ∈ ℂ) ∧ ((𝐷 ∖ { 1 }) ⊆
(ℤ≥‘1) ∨ (𝐷 ∖ { 1 }) ∈ Fin)) →
Σ𝑓 ∈ 𝑊 1 = Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓 ∈ 𝑊, 1, 0)) |
| 215 | 210, 212,
213, 214 | syl21anc 838 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ 𝑊 1 = Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓 ∈ 𝑊, 1, 0)) |
| 216 | | hashcl 14395 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ Fin →
(♯‘𝑊) ∈
ℕ0) |
| 217 | 207, 216 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(♯‘𝑊) ∈
ℕ0) |
| 218 | 217 | nn0cnd 12589 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(♯‘𝑊) ∈
ℂ) |
| 219 | 218 | mulridd 11278 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((♯‘𝑊) ·
1) = (♯‘𝑊)) |
| 220 | 209, 215,
219 | 3eqtr3d 2785 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓 ∈ 𝑊, 1, 0) = (♯‘𝑊)) |
| 221 | 220 | oveq2d 7447 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) ·
Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓 ∈ 𝑊, 1, 0)) = ((log‘𝑥) · (♯‘𝑊))) |
| 222 | 201, 221 | eqtr3d 2779 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0)) = ((log‘𝑥) · (♯‘𝑊))) |
| 223 | 222 | negeqd 11502 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
-Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0)) = -((log‘𝑥) · (♯‘𝑊))) |
| 224 | 193, 199,
223 | 3eqtrd 2781 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = -((log‘𝑥) · (♯‘𝑊))) |
| 225 | 176, 224 | oveq12d 7449 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑓 ∈ { 1 }
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) + Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (((log‘𝑥) · 1) +
-((log‘𝑥) ·
(♯‘𝑊)))) |
| 226 | 47, 218 | mulcld 11281 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) ·
(♯‘𝑊)) ∈
ℂ) |
| 227 | 172, 226 | negsubd 11626 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(((log‘𝑥) · 1)
+ -((log‘𝑥) ·
(♯‘𝑊))) =
(((log‘𝑥) · 1)
− ((log‘𝑥)
· (♯‘𝑊)))) |
| 228 | 225, 227 | eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑓 ∈ { 1 }
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) + Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (((log‘𝑥) · 1) −
((log‘𝑥) ·
(♯‘𝑊)))) |
| 229 | | disjdif 4472 |
. . . . . . . 8
⊢ ({ 1 } ∩
(𝐷 ∖ { 1 })) =
∅ |
| 230 | 229 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ({ 1 } ∩
(𝐷 ∖ { 1 })) =
∅) |
| 231 | | undif2 4477 |
. . . . . . . 8
⊢ ({ 1 } ∪
(𝐷 ∖ { 1 })) = ({
1 } ∪
𝐷) |
| 232 | 170 | snssd 4809 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → { 1 } ⊆
𝐷) |
| 233 | | ssequn1 4186 |
. . . . . . . . 9
⊢ ({ 1 } ⊆
𝐷 ↔ ({ 1 } ∪ 𝐷) = 𝐷) |
| 234 | 232, 233 | sylib 218 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ({ 1 } ∪ 𝐷) = 𝐷) |
| 235 | 231, 234 | eqtr2id 2790 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐷 = ({ 1 } ∪ (𝐷 ∖ { 1 }))) |
| 236 | 230, 235,
6, 55 | fsumsplit 15777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ 𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = (Σ𝑓 ∈ { 1 } ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) + Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
| 237 | 47, 211, 218 | subdid 11719 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · (1
− (♯‘𝑊)))
= (((log‘𝑥) ·
1) − ((log‘𝑥)
· (♯‘𝑊)))) |
| 238 | 228, 236,
237 | 3eqtr4rd 2788 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · (1
− (♯‘𝑊)))
= Σ𝑓 ∈ 𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) |
| 239 | 166, 238 | oveq12d 7449 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊)))) = (Σ𝑓 ∈ 𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − Σ𝑓 ∈ 𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
| 240 | 56, 114, 239 | 3eqtr4d 2787 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (((ϕ‘𝑁) · Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))) |
| 241 | 240 | mpteq2dva 5242 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))))) = (𝑥 ∈ ℝ+ ↦
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊)))))) |
| 242 | | rpssre 13042 |
. . . 4
⊢
ℝ+ ⊆ ℝ |
| 243 | 242 | a1i 11 |
. . 3
⊢ (𝜑 → ℝ+
⊆ ℝ) |
| 244 | 1, 5 | syl 17 |
. . 3
⊢ (𝜑 → 𝐷 ∈ Fin) |
| 245 | 17 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (𝑓‘𝐴) ∈ ℂ) |
| 246 | 245 | cjcld 15235 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (∗‘(𝑓‘𝐴)) ∈ ℂ) |
| 247 | 58, 55 | subcld 11620 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) ∈ ℂ) |
| 248 | 246, 247 | mulcld 11281 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) ∈
ℂ) |
| 249 | 248 | anasss 466 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑓 ∈ 𝐷)) → ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) ∈
ℂ) |
| 250 | 18 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(∗‘(𝑓‘𝐴)) ∈ ℂ) |
| 251 | 247 | an32s 652 |
. . . 4
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) ∈ ℂ) |
| 252 | | o1const 15656 |
. . . . 5
⊢
((ℝ+ ⊆ ℝ ∧ (∗‘(𝑓‘𝐴)) ∈ ℂ) → (𝑥 ∈ ℝ+
↦ (∗‘(𝑓‘𝐴))) ∈ 𝑂(1)) |
| 253 | 242, 18, 252 | sylancr 587 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑥 ∈ ℝ+ ↦
(∗‘(𝑓‘𝐴))) ∈ 𝑂(1)) |
| 254 | | fveq1 6905 |
. . . . . . . . . . . 12
⊢ (𝑓 = 1 → (𝑓‘(𝐿‘𝑛)) = ( 1 ‘(𝐿‘𝑛))) |
| 255 | 254 | oveq1d 7446 |
. . . . . . . . . . 11
⊢ (𝑓 = 1 → ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) = (( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
| 256 | 255 | sumeq2sdv 15739 |
. . . . . . . . . 10
⊢ (𝑓 = 1 → Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
| 257 | 256, 174 | oveq12d 7449 |
. . . . . . . . 9
⊢ (𝑓 = 1 → (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · 1))) |
| 258 | 257 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · 1))) |
| 259 | 45 | recnd 11289 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℂ) |
| 260 | 259 | mulridd 11278 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((log‘𝑥)
· 1) = (log‘𝑥)) |
| 261 | 260 | oveq2d 7447 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · 1)) = (Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) |
| 262 | 258, 261 | sylan9eq 2797 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) |
| 263 | 262 | mpteq2dva 5242 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) → (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))) |
| 264 | 8, 23, 1, 3, 4, 65 | rpvmasumlem 27531 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈
𝑂(1)) |
| 265 | 264 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) → (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈
𝑂(1)) |
| 266 | 263, 265 | eqeltrd 2841 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) → (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) ∈
𝑂(1)) |
| 267 | 178 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (𝑓 ≠ 1 → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = ((log‘𝑥) · if(𝑓 ∈ 𝑊, -1, 0))) |
| 268 | 267 | oveq2d 7447 |
. . . . . . . . 9
⊢ (𝑓 ≠ 1 → (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 ∈ 𝑊, -1, 0)))) |
| 269 | 47 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℂ) |
| 270 | | mulcom 11241 |
. . . . . . . . . . . . . . 15
⊢
(((log‘𝑥)
∈ ℂ ∧ -1 ∈ ℂ) → ((log‘𝑥) · -1) = (-1 ·
(log‘𝑥))) |
| 271 | 269, 50, 270 | sylancl 586 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · -1)
= (-1 · (log‘𝑥))) |
| 272 | 269 | mulm1d 11715 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) → (-1
· (log‘𝑥)) =
-(log‘𝑥)) |
| 273 | 271, 272 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · -1)
= -(log‘𝑥)) |
| 274 | 269 | mul01d 11460 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · 0)
= 0) |
| 275 | 273, 274 | ifeq12d 4547 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) → if(𝑓 ∈ 𝑊, ((log‘𝑥) · -1), ((log‘𝑥) · 0)) = if(𝑓 ∈ 𝑊, -(log‘𝑥), 0)) |
| 276 | | ovif2 7532 |
. . . . . . . . . . . 12
⊢
((log‘𝑥)
· if(𝑓 ∈ 𝑊, -1, 0)) = if(𝑓 ∈ 𝑊, ((log‘𝑥) · -1), ((log‘𝑥) · 0)) |
| 277 | | negeq 11500 |
. . . . . . . . . . . . 13
⊢ (if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = (log‘𝑥) → -if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = -(log‘𝑥)) |
| 278 | | negeq 11500 |
. . . . . . . . . . . . . 14
⊢ (if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = 0 → -if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = -0) |
| 279 | 278, 182 | eqtrdi 2793 |
. . . . . . . . . . . . 13
⊢ (if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = 0 → -if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = 0) |
| 280 | 277, 279 | ifsb 4539 |
. . . . . . . . . . . 12
⊢ -if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = if(𝑓 ∈ 𝑊, -(log‘𝑥), 0) |
| 281 | 275, 276,
280 | 3eqtr4g 2802 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) ·
if(𝑓 ∈ 𝑊, -1, 0)) = -if(𝑓 ∈ 𝑊, (log‘𝑥), 0)) |
| 282 | 281 | oveq2d 7447 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 ∈ 𝑊, -1, 0))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − -if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) |
| 283 | 58 | an32s 652 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
| 284 | | ifcl 4571 |
. . . . . . . . . . . 12
⊢
(((log‘𝑥)
∈ ℂ ∧ 0 ∈ ℂ) → if(𝑓 ∈ 𝑊, (log‘𝑥), 0) ∈ ℂ) |
| 285 | 269, 51, 284 | sylancl 586 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) → if(𝑓 ∈ 𝑊, (log‘𝑥), 0) ∈ ℂ) |
| 286 | 283, 285 | subnegd 11627 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − -if(𝑓 ∈ 𝑊, (log‘𝑥), 0)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) |
| 287 | 282, 286 | eqtrd 2777 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 ∈ 𝑊, -1, 0))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) |
| 288 | 268, 287 | sylan9eqr 2799 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ≠ 1 ) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) |
| 289 | 288 | an32s 652 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) |
| 290 | 289 | mpteq2dva 5242 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0)))) |
| 291 | 1 | ad2antrr 726 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → 𝑁 ∈ ℕ) |
| 292 | | simplr 769 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → 𝑓 ∈ 𝐷) |
| 293 | | simpr 484 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → 𝑓 ≠ 1 ) |
| 294 | | eqid 2737 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎)) = (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎)) |
| 295 | 8, 23, 291, 3, 4, 65, 292, 293, 294 | dchrmusumlema 27537 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦))) |
| 296 | 1 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑁 ∈ ℕ) |
| 297 | 296 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑁 ∈ ℕ) |
| 298 | 292 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑓 ∈ 𝐷) |
| 299 | | simplr 769 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑓 ≠ 1 ) |
| 300 | | simprl 771 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑐 ∈ (0[,)+∞)) |
| 301 | | simprrl 781 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡) |
| 302 | | simprrr 782 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) |
| 303 | 8, 23, 297, 3, 4, 65, 298, 299, 294, 300, 301, 302, 202 | dchrvmaeq0 27548 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑓 ∈ 𝑊 ↔ 𝑡 = 0)) |
| 304 | | ifbi 4548 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ 𝑊 ↔ 𝑡 = 0) → if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = if(𝑡 = 0, (log‘𝑥), 0)) |
| 305 | 304 | oveq2d 7447 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ 𝑊 ↔ 𝑡 = 0) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑡 = 0, (log‘𝑥), 0))) |
| 306 | 305 | mpteq2dv 5244 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ 𝑊 ↔ 𝑡 = 0) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑡 = 0, (log‘𝑥), 0)))) |
| 307 | 303, 306 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑡 = 0, (log‘𝑥), 0)))) |
| 308 | 8, 23, 297, 3, 4, 65, 298, 299, 294, 300, 301, 302 | dchrvmasumif 27547 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑡 = 0, (log‘𝑥), 0))) ∈ 𝑂(1)) |
| 309 | 307, 308 | eqeltrd 2841 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) ∈ 𝑂(1)) |
| 310 | 309 | rexlimdvaa 3156 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → (∃𝑐 ∈ (0[,)+∞)(seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) ∈
𝑂(1))) |
| 311 | 310 | exlimdv 1933 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → (∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) ∈
𝑂(1))) |
| 312 | 295, 311 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) ∈ 𝑂(1)) |
| 313 | 290, 312 | eqeltrd 2841 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) ∈
𝑂(1)) |
| 314 | 266, 313 | pm2.61dane 3029 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) ∈
𝑂(1)) |
| 315 | 250, 251,
253, 314 | o1mul2 15661 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑥 ∈ ℝ+ ↦
((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))))) ∈
𝑂(1)) |
| 316 | 243, 244,
249, 315 | fsumo1 15848 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))))) ∈
𝑂(1)) |
| 317 | 241, 316 | eqeltrrd 2842 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))) ∈
𝑂(1)) |