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 24780 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin) |
6 | 2, 5 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈ Fin) |
7 | | fzfid 12634 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (1...(⌊‘𝑥)) ∈ Fin) |
8 | | rpvmasum.z |
. . . . . . . . . . . . 13
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
9 | | eqid 2610 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑍) =
(Base‘𝑍) |
10 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑓 ∈ 𝐷) |
11 | 3, 8, 4, 9, 10 | dchrf 24767 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑓:(Base‘𝑍)⟶ℂ) |
12 | | rpvmasum2.u |
. . . . . . . . . . . . . . 15
⊢ 𝑈 = (Unit‘𝑍) |
13 | 9, 12 | unitss 18483 |
. . . . . . . . . . . . . 14
⊢ 𝑈 ⊆ (Base‘𝑍) |
14 | | rpvmasum2.b |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
15 | 13, 14 | sseldi 3566 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ (Base‘𝑍)) |
16 | 15 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝐴 ∈ (Base‘𝑍)) |
17 | 11, 16 | ffvelrnd 6268 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓‘𝐴) ∈ ℂ) |
18 | 17 | cjcld 13784 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (∗‘(𝑓‘𝐴)) ∈ ℂ) |
19 | 18 | adantlr 747 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (∗‘(𝑓‘𝐴)) ∈ ℂ) |
20 | 19 | adantrl 748 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑓 ∈ 𝐷)) → (∗‘(𝑓‘𝐴)) ∈ ℂ) |
21 | 11 | adantlr 747 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → 𝑓:(Base‘𝑍)⟶ℂ) |
22 | 21 | adantlr 747 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → 𝑓:(Base‘𝑍)⟶ℂ) |
23 | 1 | nnnn0d 11228 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
24 | | rpvmasum.l |
. . . . . . . . . . . . . . . 16
⊢ 𝐿 = (ℤRHom‘𝑍) |
25 | 8, 9, 24 | znzrhfo 19715 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→(Base‘𝑍)) |
26 | | fof 6028 |
. . . . . . . . . . . . . . 15
⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍)) |
27 | 23, 25, 26 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍)) |
28 | 27 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐿:ℤ⟶(Base‘𝑍)) |
29 | | elfzelz 12213 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℤ) |
30 | | ffvelrn 6265 |
. . . . . . . . . . . . 13
⊢ ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑛 ∈ ℤ) → (𝐿‘𝑛) ∈ (Base‘𝑍)) |
31 | 28, 29, 30 | syl2an 493 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝐿‘𝑛) ∈ (Base‘𝑍)) |
32 | 31 | adantr 480 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → (𝐿‘𝑛) ∈ (Base‘𝑍)) |
33 | 22, 32 | ffvelrnd 6268 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → (𝑓‘(𝐿‘𝑛)) ∈ ℂ) |
34 | 33 | anasss 677 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑓 ∈ 𝐷)) → (𝑓‘(𝐿‘𝑛)) ∈ ℂ) |
35 | | elfznn 12241 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
36 | 35 | adantl 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
37 | | vmacl 24644 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
38 | 36, 37 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
39 | 38, 36 | nndivred 10946 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℝ) |
40 | 39 | recnd 9947 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℂ) |
41 | 40 | adantrr 749 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑓 ∈ 𝐷)) → ((Λ‘𝑛) / 𝑛) ∈ ℂ) |
42 | 34, 41 | mulcld 9939 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑓 ∈ 𝐷)) → ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
43 | 20, 42 | mulcld 9939 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑓 ∈ 𝐷)) →
((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ ℂ) |
44 | 43 | anass1rs 845 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ ℂ) |
45 | 7, 44 | fsumcl 14311 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ ℂ) |
46 | | relogcl 24126 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
47 | 46 | adantl 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℝ) |
48 | 47 | recnd 9947 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℂ) |
49 | 48 | adantr 480 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (log‘𝑥) ∈ ℂ) |
50 | | ax-1cn 9873 |
. . . . . . 7
⊢ 1 ∈
ℂ |
51 | | neg1cn 11001 |
. . . . . . . 8
⊢ -1 ∈
ℂ |
52 | | 0cn 9911 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
53 | 51, 52 | keepel 4105 |
. . . . . . 7
⊢ if(𝑓 ∈ 𝑊, -1, 0) ∈ ℂ |
54 | 50, 53 | keepel 4105 |
. . . . . 6
⊢ if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)) ∈ ℂ |
55 | | mulcl 9899 |
. . . . . 6
⊢
(((log‘𝑥)
∈ ℂ ∧ if(𝑓 =
1 , 1,
if(𝑓 ∈ 𝑊, -1, 0)) ∈ ℂ) →
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) ∈ ℂ) |
56 | 49, 54, 55 | sylancl 693 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) ∈ ℂ) |
57 | 6, 45, 56 | fsumsub 14362 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ 𝐷 (Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑓 ∈ 𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − Σ𝑓 ∈ 𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
58 | 42 | anass1rs 845 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
59 | 7, 58 | fsumcl 14311 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
60 | 19, 59, 56 | subdid 10365 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (((∗‘(𝑓‘𝐴)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((∗‘(𝑓‘𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))))) |
61 | 7, 19, 58 | fsummulc2 14358 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
62 | 54 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)) ∈ ℂ) |
63 | 19, 49, 62 | mul12d 10124 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = ((log‘𝑥) · ((∗‘(𝑓‘𝐴)) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
64 | | ovif2 6636 |
. . . . . . . . . 10
⊢
((∗‘(𝑓‘𝐴)) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = if(𝑓 = 1 , ((∗‘(𝑓‘𝐴)) · 1), ((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0))) |
65 | | fveq1 6102 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑓 = 1 → (𝑓‘𝐴) = ( 1 ‘𝐴)) |
66 | | rpvmasum2.1 |
. . . . . . . . . . . . . . . . . 18
⊢ 1 =
(0g‘𝐺) |
67 | 1 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → 𝑁 ∈ ℕ) |
68 | 14 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → 𝐴 ∈ 𝑈) |
69 | 3, 8, 66, 12, 67, 68 | dchr1 24782 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ( 1 ‘𝐴) = 1) |
70 | 65, 69 | sylan9eqr 2666 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) → (𝑓‘𝐴) = 1) |
71 | 70 | fveq2d 6107 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) →
(∗‘(𝑓‘𝐴)) = (∗‘1)) |
72 | | 1re 9918 |
. . . . . . . . . . . . . . . 16
⊢ 1 ∈
ℝ |
73 | | cjre 13727 |
. . . . . . . . . . . . . . . 16
⊢ (1 ∈
ℝ → (∗‘1) = 1) |
74 | 72, 73 | ax-mp 5 |
. . . . . . . . . . . . . . 15
⊢
(∗‘1) = 1 |
75 | 71, 74 | syl6eq 2660 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) →
(∗‘(𝑓‘𝐴)) = 1) |
76 | 75 | oveq1d 6564 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) →
((∗‘(𝑓‘𝐴)) · 1) = (1 ·
1)) |
77 | | 1t1e1 11052 |
. . . . . . . . . . . . 13
⊢ (1
· 1) = 1 |
78 | 76, 77 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) →
((∗‘(𝑓‘𝐴)) · 1) = 1) |
79 | 78 | ifeq1da 4066 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → if(𝑓 = 1 , ((∗‘(𝑓‘𝐴)) · 1), ((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0))) = if(𝑓 = 1 , 1,
((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0)))) |
80 | | df-ne 2782 |
. . . . . . . . . . . . 13
⊢ (𝑓 ≠ 1 ↔ ¬ 𝑓 = 1 ) |
81 | | ovif2 6636 |
. . . . . . . . . . . . . 14
⊢
((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0)) = if(𝑓 ∈ 𝑊, ((∗‘(𝑓‘𝐴)) · -1), ((∗‘(𝑓‘𝐴)) · 0)) |
82 | | simplll 794 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → 𝜑) |
83 | | rpvmasum2.z1 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑊) → 𝐴 = (1r‘𝑍)) |
84 | 83 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑊) → (𝑓‘𝐴) = (𝑓‘(1r‘𝑍))) |
85 | 82, 84 | sylan 487 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → (𝑓‘𝐴) = (𝑓‘(1r‘𝑍))) |
86 | 3, 8, 4 | dchrmhm 24766 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) |
87 | | simpr 476 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → 𝑓 ∈ 𝐷) |
88 | 86, 87 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → 𝑓 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
89 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
90 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(1r‘𝑍) = (1r‘𝑍) |
91 | 89, 90 | ringidval 18326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1r‘𝑍) = (0g‘(mulGrp‘𝑍)) |
92 | | eqid 2610 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
93 | | cnfld1 19590 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ 1 =
(1r‘ℂfld) |
94 | 92, 93 | ringidval 18326 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) |
95 | 91, 94 | mhm0 17166 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑓 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) → (𝑓‘(1r‘𝑍)) = 1) |
96 | 88, 95 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (𝑓‘(1r‘𝑍)) = 1) |
97 | 96 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → (𝑓‘(1r‘𝑍)) = 1) |
98 | 85, 97 | eqtrd 2644 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → (𝑓‘𝐴) = 1) |
99 | 98 | fveq2d 6107 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → (∗‘(𝑓‘𝐴)) = (∗‘1)) |
100 | 99, 74 | syl6eq 2660 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → (∗‘(𝑓‘𝐴)) = 1) |
101 | 100 | oveq1d 6564 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → ((∗‘(𝑓‘𝐴)) · -1) = (1 ·
-1)) |
102 | 51 | mulid2i 9922 |
. . . . . . . . . . . . . . . . 17
⊢ (1
· -1) = -1 |
103 | 101, 102 | syl6eq 2660 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → ((∗‘(𝑓‘𝐴)) · -1) = -1) |
104 | 103 | ifeq1da 4066 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → if(𝑓 ∈ 𝑊, ((∗‘(𝑓‘𝐴)) · -1), ((∗‘(𝑓‘𝐴)) · 0)) = if(𝑓 ∈ 𝑊, -1, ((∗‘(𝑓‘𝐴)) · 0))) |
105 | 19 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) →
(∗‘(𝑓‘𝐴)) ∈ ℂ) |
106 | 105 | mul01d 10114 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) →
((∗‘(𝑓‘𝐴)) · 0) = 0) |
107 | 106 | ifeq2d 4055 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → if(𝑓 ∈ 𝑊, -1, ((∗‘(𝑓‘𝐴)) · 0)) = if(𝑓 ∈ 𝑊, -1, 0)) |
108 | 104, 107 | eqtrd 2644 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → if(𝑓 ∈ 𝑊, ((∗‘(𝑓‘𝐴)) · -1), ((∗‘(𝑓‘𝐴)) · 0)) = if(𝑓 ∈ 𝑊, -1, 0)) |
109 | 81, 108 | syl5eq 2656 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) →
((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0)) = if(𝑓 ∈ 𝑊, -1, 0)) |
110 | 80, 109 | sylan2br 492 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ ¬ 𝑓 = 1 ) →
((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0)) = if(𝑓 ∈ 𝑊, -1, 0)) |
111 | 110 | ifeq2da 4067 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → if(𝑓 = 1 , 1,
((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0))) = if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) |
112 | 79, 111 | eqtrd 2644 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → if(𝑓 = 1 , ((∗‘(𝑓‘𝐴)) · 1), ((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0))) = if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) |
113 | 64, 112 | syl5eq 2656 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) |
114 | 113 | oveq2d 6565 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((log‘𝑥) · ((∗‘(𝑓‘𝐴)) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) |
115 | 63, 114 | eqtrd 2644 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) |
116 | 61, 115 | oveq12d 6567 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (((∗‘(𝑓‘𝐴)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((∗‘(𝑓‘𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
117 | 60, 116 | eqtrd 2644 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
118 | 117 | sumeq2dv 14281 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = Σ𝑓 ∈ 𝐷 (Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
119 | | fzfid 12634 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘𝑥))
∈ Fin) |
120 | | inss1 3795 |
. . . . . . . . 9
⊢
((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥)) |
121 | | ssfi 8065 |
. . . . . . . . 9
⊢
(((1...(⌊‘𝑥)) ∈ Fin ∧
((1...(⌊‘𝑥))
∩ 𝑇) ⊆
(1...(⌊‘𝑥)))
→ ((1...(⌊‘𝑥)) ∩ 𝑇) ∈ Fin) |
122 | 119, 120,
121 | sylancl 693 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((1...(⌊‘𝑥))
∩ 𝑇) ∈
Fin) |
123 | 2 | phicld 15315 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(ϕ‘𝑁) ∈
ℕ) |
124 | 123 | nncnd 10913 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(ϕ‘𝑁) ∈
ℂ) |
125 | 120 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((1...(⌊‘𝑥))
∩ 𝑇) ⊆
(1...(⌊‘𝑥))) |
126 | 125 | sselda 3568 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)) → 𝑛 ∈
(1...(⌊‘𝑥))) |
127 | 126, 40 | syldan 486 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)) →
((Λ‘𝑛) / 𝑛) ∈
ℂ) |
128 | 122, 124,
127 | fsummulc2 14358 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛))) |
129 | 124 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ϕ‘𝑁)
∈ ℂ) |
130 | 129, 40 | mulcld 9939 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ϕ‘𝑁)
· ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
131 | 126, 130 | syldan 486 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)) →
((ϕ‘𝑁) ·
((Λ‘𝑛) / 𝑛)) ∈
ℂ) |
132 | 131 | ralrimiva 2949 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∀𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
133 | 119 | olcd 407 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((1...(⌊‘𝑥))
⊆ (ℤ≥‘1) ∨ (1...(⌊‘𝑥)) ∈ Fin)) |
134 | | sumss2 14304 |
. . . . . . . 8
⊢
(((((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥)) ∧ ∀𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) ∧
((1...(⌊‘𝑥))
⊆ (ℤ≥‘1) ∨ (1...(⌊‘𝑥)) ∈ Fin)) →
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0)) |
135 | 125, 132,
133, 134 | syl21anc 1317 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0)) |
136 | | elin 3758 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇) ↔ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ 𝑇)) |
137 | 136 | baib 942 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ (𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇) ↔ 𝑛 ∈ 𝑇)) |
138 | 137 | adantl 481 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇) ↔ 𝑛 ∈ 𝑇)) |
139 | | rpvmasum2.t |
. . . . . . . . . . . . 13
⊢ 𝑇 = (◡𝐿 “ {𝐴}) |
140 | 139 | eleq2i 2680 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑇 ↔ 𝑛 ∈ (◡𝐿 “ {𝐴})) |
141 | | ffn 5958 |
. . . . . . . . . . . . . 14
⊢ (𝐿:ℤ⟶(Base‘𝑍) → 𝐿 Fn ℤ) |
142 | 28, 141 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐿 Fn ℤ) |
143 | | fniniseg 6246 |
. . . . . . . . . . . . . 14
⊢ (𝐿 Fn ℤ → (𝑛 ∈ (◡𝐿 “ {𝐴}) ↔ (𝑛 ∈ ℤ ∧ (𝐿‘𝑛) = 𝐴))) |
144 | 143 | baibd 946 |
. . . . . . . . . . . . 13
⊢ ((𝐿 Fn ℤ ∧ 𝑛 ∈ ℤ) → (𝑛 ∈ (◡𝐿 “ {𝐴}) ↔ (𝐿‘𝑛) = 𝐴)) |
145 | 142, 29, 144 | syl2an 493 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ∈ (◡𝐿 “ {𝐴}) ↔ (𝐿‘𝑛) = 𝐴)) |
146 | 140, 145 | syl5bb 271 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ∈ 𝑇 ↔ (𝐿‘𝑛) = 𝐴)) |
147 | 138, 146 | bitr2d 268 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝐿‘𝑛) = 𝐴 ↔ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇))) |
148 | 40 | mul02d 10113 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (0 · ((Λ‘𝑛) / 𝑛)) = 0) |
149 | 147, 148 | ifbieq2d 4061 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ if((𝐿‘𝑛) = 𝐴, ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), (0 · ((Λ‘𝑛) / 𝑛))) = if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0)) |
150 | | ovif 6635 |
. . . . . . . . . 10
⊢
(if((𝐿‘𝑛) = 𝐴, (ϕ‘𝑁), 0) · ((Λ‘𝑛) / 𝑛)) = if((𝐿‘𝑛) = 𝐴, ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), (0 · ((Λ‘𝑛) / 𝑛))) |
151 | 1 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑁 ∈
ℕ) |
152 | 151, 5 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝐷 ∈
Fin) |
153 | 19 | adantlr 747 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → (∗‘(𝑓‘𝐴)) ∈ ℂ) |
154 | 33, 153 | mulcld 9939 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → ((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) ∈ ℂ) |
155 | 152, 40, 154 | fsummulc1 14359 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑓 ∈
𝐷 ((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑓 ∈ 𝐷 (((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛))) |
156 | 14 | ad2antrr 758 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝐴 ∈ 𝑈) |
157 | 3, 4, 8, 9, 12, 151, 31, 156 | sum2dchr 24799 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑓 ∈
𝐷 ((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) = if((𝐿‘𝑛) = 𝐴, (ϕ‘𝑁), 0)) |
158 | 157 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑓 ∈
𝐷 ((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = (if((𝐿‘𝑛) = 𝐴, (ϕ‘𝑁), 0) · ((Λ‘𝑛) / 𝑛))) |
159 | 40 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → ((Λ‘𝑛) / 𝑛) ∈ ℂ) |
160 | | mulass 9903 |
. . . . . . . . . . . . . 14
⊢ (((𝑓‘(𝐿‘𝑛)) ∈ ℂ ∧
(∗‘(𝑓‘𝐴)) ∈ ℂ ∧
((Λ‘𝑛) / 𝑛) ∈ ℂ) →
(((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = ((𝑓‘(𝐿‘𝑛)) · ((∗‘(𝑓‘𝐴)) · ((Λ‘𝑛) / 𝑛)))) |
161 | | mul12 10081 |
. . . . . . . . . . . . . 14
⊢ (((𝑓‘(𝐿‘𝑛)) ∈ ℂ ∧
(∗‘(𝑓‘𝐴)) ∈ ℂ ∧
((Λ‘𝑛) / 𝑛) ∈ ℂ) → ((𝑓‘(𝐿‘𝑛)) · ((∗‘(𝑓‘𝐴)) · ((Λ‘𝑛) / 𝑛))) = ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
162 | 160, 161 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (((𝑓‘(𝐿‘𝑛)) ∈ ℂ ∧
(∗‘(𝑓‘𝐴)) ∈ ℂ ∧
((Λ‘𝑛) / 𝑛) ∈ ℂ) →
(((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
163 | 33, 153, 159, 162 | syl3anc 1318 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → (((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
164 | 163 | sumeq2dv 14281 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑓 ∈
𝐷 (((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
165 | 155, 158,
164 | 3eqtr3d 2652 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (if((𝐿‘𝑛) = 𝐴, (ϕ‘𝑁), 0) · ((Λ‘𝑛) / 𝑛)) = Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
166 | 150, 165 | syl5eqr 2658 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ if((𝐿‘𝑛) = 𝐴, ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), (0 · ((Λ‘𝑛) / 𝑛))) = Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
167 | 149, 166 | eqtr3d 2646 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ if(𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇),
((ϕ‘𝑁) ·
((Λ‘𝑛) / 𝑛)), 0) = Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
168 | 167 | sumeq2dv 14281 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
169 | 128, 135,
168 | 3eqtrd 2648 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
170 | 119, 6, 43 | fsumcom 14349 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) = Σ𝑓 ∈ 𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
171 | 169, 170 | eqtrd 2644 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) = Σ𝑓 ∈ 𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
172 | 3 | dchrabl 24779 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) |
173 | | ablgrp 18021 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
174 | 4, 66 | grpidcl 17273 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp → 1 ∈ 𝐷) |
175 | 2, 172, 173, 174 | 4syl 19 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 1 ∈ 𝐷) |
176 | 48 | mulid1d 9936 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · 1)
= (log‘𝑥)) |
177 | 176, 48 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · 1)
∈ ℂ) |
178 | | iftrue 4042 |
. . . . . . . . . . 11
⊢ (𝑓 = 1 → if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)) = 1) |
179 | 178 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑓 = 1 → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = ((log‘𝑥) · 1)) |
180 | 179 | sumsn 14319 |
. . . . . . . . 9
⊢ (( 1 ∈ 𝐷 ∧ ((log‘𝑥) · 1) ∈ ℂ)
→ Σ𝑓 ∈ {
1 }
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = ((log‘𝑥) · 1)) |
181 | 175, 177,
180 | syl2anc 691 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ { 1 }
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = ((log‘𝑥) · 1)) |
182 | | eldifsn 4260 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (𝐷 ∖ { 1 }) ↔ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) |
183 | | ifnefalse 4048 |
. . . . . . . . . . . . . . 15
⊢ (𝑓 ≠ 1 → if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)) = if(𝑓 ∈ 𝑊, -1, 0)) |
184 | 183 | ad2antll 761 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) → if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)) = if(𝑓 ∈ 𝑊, -1, 0)) |
185 | | negeq 10152 |
. . . . . . . . . . . . . . 15
⊢ (if(𝑓 ∈ 𝑊, 1, 0) = 1 → -if(𝑓 ∈ 𝑊, 1, 0) = -1) |
186 | | negeq 10152 |
. . . . . . . . . . . . . . . 16
⊢ (if(𝑓 ∈ 𝑊, 1, 0) = 0 → -if(𝑓 ∈ 𝑊, 1, 0) = -0) |
187 | | neg0 10206 |
. . . . . . . . . . . . . . . 16
⊢ -0 =
0 |
188 | 186, 187 | syl6eq 2660 |
. . . . . . . . . . . . . . 15
⊢ (if(𝑓 ∈ 𝑊, 1, 0) = 0 → -if(𝑓 ∈ 𝑊, 1, 0) = 0) |
189 | 185, 188 | ifsb 4049 |
. . . . . . . . . . . . . 14
⊢ -if(𝑓 ∈ 𝑊, 1, 0) = if(𝑓 ∈ 𝑊, -1, 0) |
190 | 184, 189 | syl6eqr 2662 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) → if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)) = -if(𝑓 ∈ 𝑊, 1, 0)) |
191 | 190 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) →
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = ((log‘𝑥) · -if(𝑓 ∈ 𝑊, 1, 0))) |
192 | 48 | adantr 480 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) → (log‘𝑥) ∈
ℂ) |
193 | 50, 52 | keepel 4105 |
. . . . . . . . . . . . 13
⊢ if(𝑓 ∈ 𝑊, 1, 0) ∈ ℂ |
194 | | mulneg2 10346 |
. . . . . . . . . . . . 13
⊢
(((log‘𝑥)
∈ ℂ ∧ if(𝑓
∈ 𝑊, 1, 0) ∈
ℂ) → ((log‘𝑥) · -if(𝑓 ∈ 𝑊, 1, 0)) = -((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
195 | 192, 193,
194 | sylancl 693 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) →
((log‘𝑥) ·
-if(𝑓 ∈ 𝑊, 1, 0)) = -((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
196 | 191, 195 | eqtrd 2644 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) →
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = -((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
197 | 182, 196 | sylan2b 491 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) →
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = -((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
198 | 197 | sumeq2dv 14281 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = Σ𝑓 ∈ (𝐷 ∖ { 1 })-((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
199 | | diffi 8077 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ Fin → (𝐷 ∖ { 1 }) ∈
Fin) |
200 | 6, 199 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝐷 ∖ { 1 }) ∈
Fin) |
201 | 48 | adantr 480 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) →
(log‘𝑥) ∈
ℂ) |
202 | | mulcl 9899 |
. . . . . . . . . . 11
⊢
(((log‘𝑥)
∈ ℂ ∧ if(𝑓
∈ 𝑊, 1, 0) ∈
ℂ) → ((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0)) ∈ ℂ) |
203 | 201, 193,
202 | sylancl 693 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) →
((log‘𝑥) ·
if(𝑓 ∈ 𝑊, 1, 0)) ∈
ℂ) |
204 | 200, 203 | fsumneg 14361 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ (𝐷 ∖ { 1 })-((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0)) = -Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
205 | 193 | a1i 11 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) → if(𝑓 ∈ 𝑊, 1, 0) ∈ ℂ) |
206 | 200, 48, 205 | fsummulc2 14358 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) ·
Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓 ∈ 𝑊, 1, 0)) = Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
207 | | rpvmasum2.w |
. . . . . . . . . . . . . . . . 17
⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} |
208 | | ssrab2 3650 |
. . . . . . . . . . . . . . . . 17
⊢ {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} ⊆ (𝐷 ∖ { 1 }) |
209 | 207, 208 | eqsstri 3598 |
. . . . . . . . . . . . . . . 16
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
210 | | difss 3699 |
. . . . . . . . . . . . . . . 16
⊢ (𝐷 ∖ { 1 }) ⊆ 𝐷 |
211 | 209, 210 | sstri 3577 |
. . . . . . . . . . . . . . 15
⊢ 𝑊 ⊆ 𝐷 |
212 | | ssfi 8065 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ Fin ∧ 𝑊 ⊆ 𝐷) → 𝑊 ∈ Fin) |
213 | 6, 211, 212 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑊 ∈ Fin) |
214 | | fsumconst 14364 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Fin ∧ 1 ∈
ℂ) → Σ𝑓
∈ 𝑊 1 =
((#‘𝑊) ·
1)) |
215 | 213, 50, 214 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ 𝑊 1 = ((#‘𝑊) · 1)) |
216 | 209 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑊 ⊆ (𝐷 ∖ { 1 })) |
217 | 50 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℂ) |
218 | 217 | ralrimivw 2950 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∀𝑓 ∈ 𝑊 1 ∈
ℂ) |
219 | 200 | olcd 407 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝐷 ∖ { 1 }) ⊆
(ℤ≥‘1) ∨ (𝐷 ∖ { 1 }) ∈
Fin)) |
220 | | sumss2 14304 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ⊆ (𝐷 ∖ { 1 }) ∧ ∀𝑓 ∈ 𝑊 1 ∈ ℂ) ∧ ((𝐷 ∖ { 1 }) ⊆
(ℤ≥‘1) ∨ (𝐷 ∖ { 1 }) ∈ Fin)) →
Σ𝑓 ∈ 𝑊 1 = Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓 ∈ 𝑊, 1, 0)) |
221 | 216, 218,
219, 220 | syl21anc 1317 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ 𝑊 1 = Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓 ∈ 𝑊, 1, 0)) |
222 | | hashcl 13009 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ Fin →
(#‘𝑊) ∈
ℕ0) |
223 | 213, 222 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(#‘𝑊) ∈
ℕ0) |
224 | 223 | nn0cnd 11230 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(#‘𝑊) ∈
ℂ) |
225 | 224 | mulid1d 9936 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((#‘𝑊) · 1) =
(#‘𝑊)) |
226 | 215, 221,
225 | 3eqtr3d 2652 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓 ∈ 𝑊, 1, 0) = (#‘𝑊)) |
227 | 226 | oveq2d 6565 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) ·
Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓 ∈ 𝑊, 1, 0)) = ((log‘𝑥) · (#‘𝑊))) |
228 | 206, 227 | eqtr3d 2646 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0)) = ((log‘𝑥) · (#‘𝑊))) |
229 | 228 | negeqd 10154 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
-Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0)) = -((log‘𝑥) · (#‘𝑊))) |
230 | 198, 204,
229 | 3eqtrd 2648 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = -((log‘𝑥) · (#‘𝑊))) |
231 | 181, 230 | oveq12d 6567 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑓 ∈ { 1 }
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) + Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (((log‘𝑥) · 1) +
-((log‘𝑥) ·
(#‘𝑊)))) |
232 | 48, 224 | mulcld 9939 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) ·
(#‘𝑊)) ∈
ℂ) |
233 | 177, 232 | negsubd 10277 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(((log‘𝑥) · 1)
+ -((log‘𝑥) ·
(#‘𝑊))) =
(((log‘𝑥) · 1)
− ((log‘𝑥)
· (#‘𝑊)))) |
234 | 231, 233 | eqtrd 2644 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑓 ∈ { 1 }
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) + Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (((log‘𝑥) · 1) −
((log‘𝑥) ·
(#‘𝑊)))) |
235 | | disjdif 3992 |
. . . . . . . 8
⊢ ({ 1 } ∩
(𝐷 ∖ { 1 })) =
∅ |
236 | 235 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ({ 1 } ∩
(𝐷 ∖ { 1 })) =
∅) |
237 | | undif2 3996 |
. . . . . . . 8
⊢ ({ 1 } ∪
(𝐷 ∖ { 1 })) = ({
1 } ∪
𝐷) |
238 | 175 | snssd 4281 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → { 1 } ⊆
𝐷) |
239 | | ssequn1 3745 |
. . . . . . . . 9
⊢ ({ 1 } ⊆
𝐷 ↔ ({ 1 } ∪ 𝐷) = 𝐷) |
240 | 238, 239 | sylib 207 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ({ 1 } ∪ 𝐷) = 𝐷) |
241 | 237, 240 | syl5req 2657 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐷 = ({ 1 } ∪ (𝐷 ∖ { 1 }))) |
242 | 236, 241,
6, 56 | fsumsplit 14318 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ 𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = (Σ𝑓 ∈ { 1 } ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) + Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
243 | 48, 217, 224 | subdid 10365 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · (1
− (#‘𝑊))) =
(((log‘𝑥) · 1)
− ((log‘𝑥)
· (#‘𝑊)))) |
244 | 234, 242,
243 | 3eqtr4rd 2655 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · (1
− (#‘𝑊))) =
Σ𝑓 ∈ 𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) |
245 | 171, 244 | oveq12d 6567 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊)))) = (Σ𝑓 ∈ 𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − Σ𝑓 ∈ 𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
246 | 57, 118, 245 | 3eqtr4d 2654 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (((ϕ‘𝑁) · Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊))))) |
247 | 246 | mpteq2dva 4672 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))))) = (𝑥 ∈ ℝ+ ↦
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊)))))) |
248 | | rpssre 11719 |
. . . 4
⊢
ℝ+ ⊆ ℝ |
249 | 248 | a1i 11 |
. . 3
⊢ (𝜑 → ℝ+
⊆ ℝ) |
250 | 1, 5 | syl 17 |
. . 3
⊢ (𝜑 → 𝐷 ∈ Fin) |
251 | 17 | adantlr 747 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (𝑓‘𝐴) ∈ ℂ) |
252 | 251 | cjcld 13784 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (∗‘(𝑓‘𝐴)) ∈ ℂ) |
253 | 59, 56 | subcld 10271 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) ∈ ℂ) |
254 | 252, 253 | mulcld 9939 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) ∈
ℂ) |
255 | 254 | anasss 677 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑓 ∈ 𝐷)) → ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) ∈
ℂ) |
256 | 18 | adantr 480 |
. . . 4
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(∗‘(𝑓‘𝐴)) ∈ ℂ) |
257 | 253 | an32s 842 |
. . . 4
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) ∈ ℂ) |
258 | | o1const 14198 |
. . . . 5
⊢
((ℝ+ ⊆ ℝ ∧ (∗‘(𝑓‘𝐴)) ∈ ℂ) → (𝑥 ∈ ℝ+
↦ (∗‘(𝑓‘𝐴))) ∈ 𝑂(1)) |
259 | 248, 18, 258 | sylancr 694 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑥 ∈ ℝ+ ↦
(∗‘(𝑓‘𝐴))) ∈ 𝑂(1)) |
260 | | fveq1 6102 |
. . . . . . . . . . . 12
⊢ (𝑓 = 1 → (𝑓‘(𝐿‘𝑛)) = ( 1 ‘(𝐿‘𝑛))) |
261 | 260 | oveq1d 6564 |
. . . . . . . . . . 11
⊢ (𝑓 = 1 → ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) = (( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
262 | 261 | sumeq2sdv 14282 |
. . . . . . . . . 10
⊢ (𝑓 = 1 → Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
263 | 262, 179 | oveq12d 6567 |
. . . . . . . . 9
⊢ (𝑓 = 1 → (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · 1))) |
264 | 263 | adantl 481 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · 1))) |
265 | 46 | recnd 9947 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℂ) |
266 | 265 | mulid1d 9936 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((log‘𝑥)
· 1) = (log‘𝑥)) |
267 | 266 | oveq2d 6565 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · 1)) = (Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) |
268 | 264, 267 | sylan9eq 2664 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) |
269 | 268 | mpteq2dva 4672 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) → (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))) |
270 | 8, 24, 1, 3, 4, 66 | rpvmasumlem 24976 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈
𝑂(1)) |
271 | 270 | ad2antrr 758 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) → (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈
𝑂(1)) |
272 | 269, 271 | eqeltrd 2688 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) → (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) ∈
𝑂(1)) |
273 | 183 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (𝑓 ≠ 1 → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = ((log‘𝑥) · if(𝑓 ∈ 𝑊, -1, 0))) |
274 | 273 | oveq2d 6565 |
. . . . . . . . 9
⊢ (𝑓 ≠ 1 → (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 ∈ 𝑊, -1, 0)))) |
275 | 48 | adantlr 747 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℂ) |
276 | | mulcom 9901 |
. . . . . . . . . . . . . . 15
⊢
(((log‘𝑥)
∈ ℂ ∧ -1 ∈ ℂ) → ((log‘𝑥) · -1) = (-1 ·
(log‘𝑥))) |
277 | 275, 51, 276 | sylancl 693 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · -1)
= (-1 · (log‘𝑥))) |
278 | 275 | mulm1d 10361 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) → (-1
· (log‘𝑥)) =
-(log‘𝑥)) |
279 | 277, 278 | eqtrd 2644 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · -1)
= -(log‘𝑥)) |
280 | 275 | mul01d 10114 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · 0)
= 0) |
281 | 279, 280 | ifeq12d 4056 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) → if(𝑓 ∈ 𝑊, ((log‘𝑥) · -1), ((log‘𝑥) · 0)) = if(𝑓 ∈ 𝑊, -(log‘𝑥), 0)) |
282 | | ovif2 6636 |
. . . . . . . . . . . 12
⊢
((log‘𝑥)
· if(𝑓 ∈ 𝑊, -1, 0)) = if(𝑓 ∈ 𝑊, ((log‘𝑥) · -1), ((log‘𝑥) · 0)) |
283 | | negeq 10152 |
. . . . . . . . . . . . 13
⊢ (if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = (log‘𝑥) → -if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = -(log‘𝑥)) |
284 | | negeq 10152 |
. . . . . . . . . . . . . 14
⊢ (if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = 0 → -if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = -0) |
285 | 284, 187 | syl6eq 2660 |
. . . . . . . . . . . . 13
⊢ (if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = 0 → -if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = 0) |
286 | 283, 285 | ifsb 4049 |
. . . . . . . . . . . 12
⊢ -if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = if(𝑓 ∈ 𝑊, -(log‘𝑥), 0) |
287 | 281, 282,
286 | 3eqtr4g 2669 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) ·
if(𝑓 ∈ 𝑊, -1, 0)) = -if(𝑓 ∈ 𝑊, (log‘𝑥), 0)) |
288 | 287 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 ∈ 𝑊, -1, 0))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − -if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) |
289 | 59 | an32s 842 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
290 | | ifcl 4080 |
. . . . . . . . . . . 12
⊢
(((log‘𝑥)
∈ ℂ ∧ 0 ∈ ℂ) → if(𝑓 ∈ 𝑊, (log‘𝑥), 0) ∈ ℂ) |
291 | 275, 52, 290 | sylancl 693 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) → if(𝑓 ∈ 𝑊, (log‘𝑥), 0) ∈ ℂ) |
292 | 289, 291 | subnegd 10278 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − -if(𝑓 ∈ 𝑊, (log‘𝑥), 0)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) |
293 | 288, 292 | eqtrd 2644 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 ∈ 𝑊, -1, 0))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) |
294 | 274, 293 | sylan9eqr 2666 |
. . . . . . . 8
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ≠ 1 ) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) |
295 | 294 | an32s 842 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) |
296 | 295 | mpteq2dva 4672 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0)))) |
297 | 1 | ad2antrr 758 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → 𝑁 ∈ ℕ) |
298 | | simplr 788 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → 𝑓 ∈ 𝐷) |
299 | | simpr 476 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → 𝑓 ≠ 1 ) |
300 | | eqid 2610 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎)) = (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎)) |
301 | 8, 24, 297, 3, 4, 66, 298, 299, 300 | dchrmusumlema 24982 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦))) |
302 | 1 | adantr 480 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑁 ∈ ℕ) |
303 | 302 | ad2antrr 758 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑁 ∈ ℕ) |
304 | 298 | adantr 480 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑓 ∈ 𝐷) |
305 | | simplr 788 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑓 ≠ 1 ) |
306 | | simprl 790 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑐 ∈ (0[,)+∞)) |
307 | | simprrl 800 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡) |
308 | | simprrr 801 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) |
309 | 8, 24, 303, 3, 4, 66, 304, 305, 300, 306, 307, 308, 207 | dchrvmaeq0 24993 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑓 ∈ 𝑊 ↔ 𝑡 = 0)) |
310 | | ifbi 4057 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ 𝑊 ↔ 𝑡 = 0) → if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = if(𝑡 = 0, (log‘𝑥), 0)) |
311 | 310 | oveq2d 6565 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ 𝑊 ↔ 𝑡 = 0) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑡 = 0, (log‘𝑥), 0))) |
312 | 311 | mpteq2dv 4673 |
. . . . . . . . . . 11
⊢ ((𝑓 ∈ 𝑊 ↔ 𝑡 = 0) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑡 = 0, (log‘𝑥), 0)))) |
313 | 309, 312 | syl 17 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑡 = 0, (log‘𝑥), 0)))) |
314 | 8, 24, 303, 3, 4, 66, 304, 305, 300, 306, 307, 308 | dchrvmasumif 24992 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑡 = 0, (log‘𝑥), 0))) ∈ 𝑂(1)) |
315 | 313, 314 | eqeltrd 2688 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) ∈ 𝑂(1)) |
316 | 315 | rexlimdvaa 3014 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → (∃𝑐 ∈ (0[,)+∞)(seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) ∈
𝑂(1))) |
317 | 316 | exlimdv 1848 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → (∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) ∈
𝑂(1))) |
318 | 301, 317 | mpd 15 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) ∈ 𝑂(1)) |
319 | 296, 318 | eqeltrd 2688 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) ∈
𝑂(1)) |
320 | 272, 319 | pm2.61dane 2869 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) ∈
𝑂(1)) |
321 | 256, 257,
259, 320 | o1mul2 14203 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑥 ∈ ℝ+ ↦
((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))))) ∈
𝑂(1)) |
322 | 249, 250,
255, 321 | fsumo1 14385 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))))) ∈
𝑂(1)) |
323 | 247, 322 | eqeltrrd 2689 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (#‘𝑊))))) ∈
𝑂(1)) |