Step | Hyp | Ref
| Expression |
1 | | rpvmasum.a |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | adantr 484 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑁 ∈
ℕ) |
3 | | rpvmasum2.g |
. . . . . . 7
⊢ 𝐺 = (DChr‘𝑁) |
4 | | rpvmasum2.d |
. . . . . . 7
⊢ 𝐷 = (Base‘𝐺) |
5 | 3, 4 | dchrfi 25991 |
. . . . . 6
⊢ (𝑁 ∈ ℕ → 𝐷 ∈ Fin) |
6 | 2, 5 | syl 17 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐷 ∈ Fin) |
7 | | fzfid 13433 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (1...(⌊‘𝑥)) ∈ Fin) |
8 | | rpvmasum.z |
. . . . . . . . . . . . 13
⊢ 𝑍 =
(ℤ/nℤ‘𝑁) |
9 | | eqid 2738 |
. . . . . . . . . . . . 13
⊢
(Base‘𝑍) =
(Base‘𝑍) |
10 | | simpr 488 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑓 ∈ 𝐷) |
11 | 3, 8, 4, 9, 10 | dchrf 25978 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑓:(Base‘𝑍)⟶ℂ) |
12 | | rpvmasum2.u |
. . . . . . . . . . . . . . 15
⊢ 𝑈 = (Unit‘𝑍) |
13 | 9, 12 | unitss 19533 |
. . . . . . . . . . . . . 14
⊢ 𝑈 ⊆ (Base‘𝑍) |
14 | | rpvmasum2.b |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐴 ∈ 𝑈) |
15 | 13, 14 | sseldi 3876 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 ∈ (Base‘𝑍)) |
16 | 15 | adantr 484 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝐴 ∈ (Base‘𝑍)) |
17 | 11, 16 | ffvelrnd 6863 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑓‘𝐴) ∈ ℂ) |
18 | 17 | cjcld 14646 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (∗‘(𝑓‘𝐴)) ∈ ℂ) |
19 | 18 | adantlr 715 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (∗‘(𝑓‘𝐴)) ∈ ℂ) |
20 | 19 | adantrl 716 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑓 ∈ 𝐷)) → (∗‘(𝑓‘𝐴)) ∈ ℂ) |
21 | 11 | ad4ant14 752 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → 𝑓:(Base‘𝑍)⟶ℂ) |
22 | 1 | nnnn0d 12037 |
. . . . . . . . . . . . . . 15
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
23 | | rpvmasum.l |
. . . . . . . . . . . . . . . 16
⊢ 𝐿 = (ℤRHom‘𝑍) |
24 | 8, 9, 23 | znzrhfo 20367 |
. . . . . . . . . . . . . . 15
⊢ (𝑁 ∈ ℕ0
→ 𝐿:ℤ–onto→(Base‘𝑍)) |
25 | | fof 6593 |
. . . . . . . . . . . . . . 15
⊢ (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍)) |
26 | 22, 24, 25 | 3syl 18 |
. . . . . . . . . . . . . 14
⊢ (𝜑 → 𝐿:ℤ⟶(Base‘𝑍)) |
27 | 26 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐿:ℤ⟶(Base‘𝑍)) |
28 | | elfzelz 12999 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℤ) |
29 | | ffvelrn 6860 |
. . . . . . . . . . . . 13
⊢ ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑛 ∈ ℤ) → (𝐿‘𝑛) ∈ (Base‘𝑍)) |
30 | 27, 28, 29 | syl2an 599 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝐿‘𝑛) ∈ (Base‘𝑍)) |
31 | 30 | adantr 484 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → (𝐿‘𝑛) ∈ (Base‘𝑍)) |
32 | 21, 31 | ffvelrnd 6863 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → (𝑓‘(𝐿‘𝑛)) ∈ ℂ) |
33 | 32 | anasss 470 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑓 ∈ 𝐷)) → (𝑓‘(𝐿‘𝑛)) ∈ ℂ) |
34 | | elfznn 13028 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
35 | 34 | adantl 485 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
36 | | vmacl 25855 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
37 | 35, 36 | syl 17 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
38 | 37, 35 | nndivred 11771 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℝ) |
39 | 38 | recnd 10748 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℂ) |
40 | 39 | adantrr 717 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑓 ∈ 𝐷)) → ((Λ‘𝑛) / 𝑛) ∈ ℂ) |
41 | 33, 40 | mulcld 10740 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑓 ∈ 𝐷)) → ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
42 | 20, 41 | mulcld 10740 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑓 ∈ 𝐷)) →
((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ ℂ) |
43 | 42 | anass1rs 655 |
. . . . . 6
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ ℂ) |
44 | 7, 43 | fsumcl 15184 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ ℂ) |
45 | | relogcl 25319 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℝ) |
46 | 45 | adantl 485 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℝ) |
47 | 46 | recnd 10748 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℂ) |
48 | 47 | adantr 484 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (log‘𝑥) ∈ ℂ) |
49 | | ax-1cn 10674 |
. . . . . . 7
⊢ 1 ∈
ℂ |
50 | | neg1cn 11831 |
. . . . . . . 8
⊢ -1 ∈
ℂ |
51 | | 0cn 10712 |
. . . . . . . 8
⊢ 0 ∈
ℂ |
52 | 50, 51 | ifcli 4462 |
. . . . . . 7
⊢ if(𝑓 ∈ 𝑊, -1, 0) ∈ ℂ |
53 | 49, 52 | ifcli 4462 |
. . . . . 6
⊢ if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)) ∈ ℂ |
54 | | mulcl 10700 |
. . . . . 6
⊢
(((log‘𝑥)
∈ ℂ ∧ if(𝑓 =
1 , 1,
if(𝑓 ∈ 𝑊, -1, 0)) ∈ ℂ) →
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) ∈ ℂ) |
55 | 48, 53, 54 | sylancl 589 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) ∈ ℂ) |
56 | 6, 44, 55 | fsumsub 15237 |
. . . 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 15184 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
59 | 19, 58, 55 | subdid 11175 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (((∗‘(𝑓‘𝐴)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((∗‘(𝑓‘𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))))) |
60 | 7, 19, 57 | fsummulc2 15233 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
61 | 53 | a1i 11 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)) ∈ ℂ) |
62 | 19, 48, 61 | mul12d 10928 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = ((log‘𝑥) · ((∗‘(𝑓‘𝐴)) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
63 | | ovif2 7267 |
. . . . . . . . . 10
⊢
((∗‘(𝑓‘𝐴)) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = if(𝑓 = 1 , ((∗‘(𝑓‘𝐴)) · 1), ((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0))) |
64 | | fveq1 6674 |
. . . . . . . . . . . . . . . 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 25993 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ( 1 ‘𝐴) = 1) |
69 | 64, 68 | sylan9eqr 2795 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) → (𝑓‘𝐴) = 1) |
70 | 69 | fveq2d 6679 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) →
(∗‘(𝑓‘𝐴)) = (∗‘1)) |
71 | | 1re 10720 |
. . . . . . . . . . . . . . 15
⊢ 1 ∈
ℝ |
72 | | cjre 14589 |
. . . . . . . . . . . . . . 15
⊢ (1 ∈
ℝ → (∗‘1) = 1) |
73 | 71, 72 | ax-mp 5 |
. . . . . . . . . . . . . 14
⊢
(∗‘1) = 1 |
74 | 70, 73 | eqtrdi 2789 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) →
(∗‘(𝑓‘𝐴)) = 1) |
75 | 74 | oveq1d 7186 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) →
((∗‘(𝑓‘𝐴)) · 1) = (1 ·
1)) |
76 | | 1t1e1 11879 |
. . . . . . . . . . . 12
⊢ (1
· 1) = 1 |
77 | 75, 76 | eqtrdi 2789 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) →
((∗‘(𝑓‘𝐴)) · 1) = 1) |
78 | | df-ne 2935 |
. . . . . . . . . . . 12
⊢ (𝑓 ≠ 1 ↔ ¬ 𝑓 = 1 ) |
79 | | ovif2 7267 |
. . . . . . . . . . . . 13
⊢
((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0)) = if(𝑓 ∈ 𝑊, ((∗‘(𝑓‘𝐴)) · -1), ((∗‘(𝑓‘𝐴)) · 0)) |
80 | | rpvmasum2.z1 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑊) → 𝐴 = (1r‘𝑍)) |
81 | 80 | fveq2d 6679 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑓 ∈ 𝑊) → (𝑓‘𝐴) = (𝑓‘(1r‘𝑍))) |
82 | 81 | ad5ant15 759 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → (𝑓‘𝐴) = (𝑓‘(1r‘𝑍))) |
83 | 3, 8, 4 | dchrmhm 25977 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 𝐷 ⊆ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld)) |
84 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → 𝑓 ∈ 𝐷) |
85 | 83, 84 | sseldi 3876 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → 𝑓 ∈ ((mulGrp‘𝑍) MndHom
(mulGrp‘ℂfld))) |
86 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(mulGrp‘𝑍) =
(mulGrp‘𝑍) |
87 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(1r‘𝑍) = (1r‘𝑍) |
88 | 86, 87 | ringidval 19373 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(1r‘𝑍) = (0g‘(mulGrp‘𝑍)) |
89 | | eqid 2738 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(mulGrp‘ℂfld) =
(mulGrp‘ℂfld) |
90 | | cnfld1 20243 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ 1 =
(1r‘ℂfld) |
91 | 89, 90 | ringidval 19373 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 =
(0g‘(mulGrp‘ℂfld)) |
92 | 88, 91 | mhm0 18081 |
. . . . . . . . . . . . . . . . . . . . . 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 2773 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → (𝑓‘𝐴) = 1) |
96 | 95 | fveq2d 6679 |
. . . . . . . . . . . . . . . . . 18
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → (∗‘(𝑓‘𝐴)) = (∗‘1)) |
97 | 96, 73 | eqtrdi 2789 |
. . . . . . . . . . . . . . . . 17
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → (∗‘(𝑓‘𝐴)) = 1) |
98 | 97 | oveq1d 7186 |
. . . . . . . . . . . . . . . 16
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → ((∗‘(𝑓‘𝐴)) · -1) = (1 ·
-1)) |
99 | 50 | mulid2i 10725 |
. . . . . . . . . . . . . . . 16
⊢ (1
· -1) = -1 |
100 | 98, 99 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
⊢
(((((𝜑 ∧ 𝑥 ∈ ℝ+)
∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ 𝑓 ∈ 𝑊) → ((∗‘(𝑓‘𝐴)) · -1) = -1) |
101 | 100 | ifeq1da 4446 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → if(𝑓 ∈ 𝑊, ((∗‘(𝑓‘𝐴)) · -1), ((∗‘(𝑓‘𝐴)) · 0)) = if(𝑓 ∈ 𝑊, -1, ((∗‘(𝑓‘𝐴)) · 0))) |
102 | 19 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) →
(∗‘(𝑓‘𝐴)) ∈ ℂ) |
103 | 102 | mul01d 10918 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) →
((∗‘(𝑓‘𝐴)) · 0) = 0) |
104 | 103 | ifeq2d 4435 |
. . . . . . . . . . . . . 14
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → if(𝑓 ∈ 𝑊, -1, ((∗‘(𝑓‘𝐴)) · 0)) = if(𝑓 ∈ 𝑊, -1, 0)) |
105 | 101, 104 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → if(𝑓 ∈ 𝑊, ((∗‘(𝑓‘𝐴)) · -1), ((∗‘(𝑓‘𝐴)) · 0)) = if(𝑓 ∈ 𝑊, -1, 0)) |
106 | 79, 105 | syl5eq 2785 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) →
((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0)) = if(𝑓 ∈ 𝑊, -1, 0)) |
107 | 78, 106 | sylan2br 598 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) ∧ ¬ 𝑓 = 1 ) →
((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0)) = if(𝑓 ∈ 𝑊, -1, 0)) |
108 | 77, 107 | ifeq12da 4448 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → if(𝑓 = 1 , ((∗‘(𝑓‘𝐴)) · 1), ((∗‘(𝑓‘𝐴)) · if(𝑓 ∈ 𝑊, -1, 0))) = if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) |
109 | 63, 108 | syl5eq 2785 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) |
110 | 109 | oveq2d 7187 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((log‘𝑥) · ((∗‘(𝑓‘𝐴)) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) |
111 | 62, 110 | eqtrd 2773 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) |
112 | 60, 111 | oveq12d 7189 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (((∗‘(𝑓‘𝐴)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((∗‘(𝑓‘𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
113 | 59, 112 | eqtrd 2773 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
114 | 113 | sumeq2dv 15154 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = Σ𝑓 ∈ 𝐷 (Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
115 | | fzfid 13433 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(1...(⌊‘𝑥))
∈ Fin) |
116 | | inss1 4120 |
. . . . . . . . 9
⊢
((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥)) |
117 | | ssfi 8773 |
. . . . . . . . 9
⊢
(((1...(⌊‘𝑥)) ∈ Fin ∧
((1...(⌊‘𝑥))
∩ 𝑇) ⊆
(1...(⌊‘𝑥)))
→ ((1...(⌊‘𝑥)) ∩ 𝑇) ∈ Fin) |
118 | 115, 116,
117 | sylancl 589 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((1...(⌊‘𝑥))
∩ 𝑇) ∈
Fin) |
119 | 2 | phicld 16210 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(ϕ‘𝑁) ∈
ℕ) |
120 | 119 | nncnd 11733 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(ϕ‘𝑁) ∈
ℂ) |
121 | 116 | a1i 11 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((1...(⌊‘𝑥))
∩ 𝑇) ⊆
(1...(⌊‘𝑥))) |
122 | 121 | sselda 3878 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)) → 𝑛 ∈
(1...(⌊‘𝑥))) |
123 | 122, 39 | syldan 594 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)) →
((Λ‘𝑛) / 𝑛) ∈
ℂ) |
124 | 118, 120,
123 | fsummulc2 15233 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛))) |
125 | 120 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ϕ‘𝑁)
∈ ℂ) |
126 | 125, 39 | mulcld 10740 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ϕ‘𝑁)
· ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
127 | 122, 126 | syldan 594 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)) →
((ϕ‘𝑁) ·
((Λ‘𝑛) / 𝑛)) ∈
ℂ) |
128 | 127 | ralrimiva 3096 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∀𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
129 | 115 | olcd 873 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((1...(⌊‘𝑥))
⊆ (ℤ≥‘1) ∨ (1...(⌊‘𝑥)) ∈ Fin)) |
130 | | sumss2 15177 |
. . . . . . . 8
⊢
(((((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥)) ∧ ∀𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) ∧
((1...(⌊‘𝑥))
⊆ (ℤ≥‘1) ∨ (1...(⌊‘𝑥)) ∈ Fin)) →
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0)) |
131 | 121, 128,
129, 130 | syl21anc 837 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0)) |
132 | | elin 3860 |
. . . . . . . . . . . . 13
⊢ (𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇) ↔ (𝑛 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈ 𝑇)) |
133 | 132 | baib 539 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ (𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇) ↔ 𝑛 ∈ 𝑇)) |
134 | 133 | adantl 485 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇) ↔ 𝑛 ∈ 𝑇)) |
135 | | rpvmasum2.t |
. . . . . . . . . . . . 13
⊢ 𝑇 = (◡𝐿 “ {𝐴}) |
136 | 135 | eleq2i 2824 |
. . . . . . . . . . . 12
⊢ (𝑛 ∈ 𝑇 ↔ 𝑛 ∈ (◡𝐿 “ {𝐴})) |
137 | 27 | ffnd 6506 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐿 Fn ℤ) |
138 | | fniniseg 6838 |
. . . . . . . . . . . . . 14
⊢ (𝐿 Fn ℤ → (𝑛 ∈ (◡𝐿 “ {𝐴}) ↔ (𝑛 ∈ ℤ ∧ (𝐿‘𝑛) = 𝐴))) |
139 | 138 | baibd 543 |
. . . . . . . . . . . . 13
⊢ ((𝐿 Fn ℤ ∧ 𝑛 ∈ ℤ) → (𝑛 ∈ (◡𝐿 “ {𝐴}) ↔ (𝐿‘𝑛) = 𝐴)) |
140 | 137, 28, 139 | syl2an 599 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ∈ (◡𝐿 “ {𝐴}) ↔ (𝐿‘𝑛) = 𝐴)) |
141 | 136, 140 | syl5bb 286 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑛 ∈ 𝑇 ↔ (𝐿‘𝑛) = 𝐴)) |
142 | 134, 141 | bitr2d 283 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝐿‘𝑛) = 𝐴 ↔ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇))) |
143 | 39 | mul02d 10917 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (0 · ((Λ‘𝑛) / 𝑛)) = 0) |
144 | 142, 143 | ifbieq2d 4441 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ if((𝐿‘𝑛) = 𝐴, ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), (0 · ((Λ‘𝑛) / 𝑛))) = if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0)) |
145 | | ovif 7266 |
. . . . . . . . . 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 10740 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → ((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) ∈ ℂ) |
150 | 147, 39, 149 | fsummulc1 15234 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑓 ∈
𝐷 ((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑓 ∈ 𝐷 (((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛))) |
151 | 14 | ad2antrr 726 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝐴 ∈ 𝑈) |
152 | 3, 4, 8, 9, 12, 146, 30, 151 | sum2dchr 26010 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑓 ∈
𝐷 ((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) = if((𝐿‘𝑛) = 𝐴, (ϕ‘𝑁), 0)) |
153 | 152 | oveq1d 7186 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑓 ∈
𝐷 ((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = (if((𝐿‘𝑛) = 𝐴, (ϕ‘𝑁), 0) · ((Λ‘𝑛) / 𝑛))) |
154 | 39 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → ((Λ‘𝑛) / 𝑛) ∈ ℂ) |
155 | | mulass 10704 |
. . . . . . . . . . . . . 14
⊢ (((𝑓‘(𝐿‘𝑛)) ∈ ℂ ∧
(∗‘(𝑓‘𝐴)) ∈ ℂ ∧
((Λ‘𝑛) / 𝑛) ∈ ℂ) →
(((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = ((𝑓‘(𝐿‘𝑛)) · ((∗‘(𝑓‘𝐴)) · ((Λ‘𝑛) / 𝑛)))) |
156 | | mul12 10884 |
. . . . . . . . . . . . . 14
⊢ (((𝑓‘(𝐿‘𝑛)) ∈ ℂ ∧
(∗‘(𝑓‘𝐴)) ∈ ℂ ∧
((Λ‘𝑛) / 𝑛) ∈ ℂ) → ((𝑓‘(𝐿‘𝑛)) · ((∗‘(𝑓‘𝐴)) · ((Λ‘𝑛) / 𝑛))) = ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
157 | 155, 156 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (((𝑓‘(𝐿‘𝑛)) ∈ ℂ ∧
(∗‘(𝑓‘𝐴)) ∈ ℂ ∧
((Λ‘𝑛) / 𝑛) ∈ ℂ) →
(((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
158 | 32, 148, 154, 157 | syl3anc 1372 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑓 ∈ 𝐷) → (((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
159 | 158 | sumeq2dv 15154 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑓 ∈
𝐷 (((𝑓‘(𝐿‘𝑛)) · (∗‘(𝑓‘𝐴))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
160 | 150, 153,
159 | 3eqtr3d 2781 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (if((𝐿‘𝑛) = 𝐴, (ϕ‘𝑁), 0) · ((Λ‘𝑛) / 𝑛)) = Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
161 | 145, 160 | eqtr3id 2787 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ if((𝐿‘𝑛) = 𝐴, ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), (0 · ((Λ‘𝑛) / 𝑛))) = Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
162 | 144, 161 | eqtr3d 2775 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ if(𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇),
((ϕ‘𝑁) ·
((Λ‘𝑛) / 𝑛)), 0) = Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
163 | 162 | sumeq2dv 15154 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
164 | 124, 131,
163 | 3eqtrd 2777 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
165 | 115, 6, 42 | fsumcom 15224 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) = Σ𝑓 ∈ 𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
166 | 164, 165 | eqtrd 2773 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) = Σ𝑓 ∈ 𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)))) |
167 | 3 | dchrabl 25990 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℕ → 𝐺 ∈ Abel) |
168 | | ablgrp 19030 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Abel → 𝐺 ∈ Grp) |
169 | 4, 65 | grpidcl 18250 |
. . . . . . . . . 10
⊢ (𝐺 ∈ Grp → 1 ∈ 𝐷) |
170 | 2, 167, 168, 169 | 4syl 19 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 1 ∈ 𝐷) |
171 | 47 | mulid1d 10737 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · 1)
= (log‘𝑥)) |
172 | 171, 47 | eqeltrd 2833 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · 1)
∈ ℂ) |
173 | | iftrue 4421 |
. . . . . . . . . . 11
⊢ (𝑓 = 1 → if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)) = 1) |
174 | 173 | oveq2d 7187 |
. . . . . . . . . 10
⊢ (𝑓 = 1 → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = ((log‘𝑥) · 1)) |
175 | 174 | sumsn 15195 |
. . . . . . . . 9
⊢ (( 1 ∈ 𝐷 ∧ ((log‘𝑥) · 1) ∈ ℂ)
→ Σ𝑓 ∈ {
1 }
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = ((log‘𝑥) · 1)) |
176 | 170, 172,
175 | syl2anc 587 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ { 1 }
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = ((log‘𝑥) · 1)) |
177 | | eldifsn 4676 |
. . . . . . . . . . 11
⊢ (𝑓 ∈ (𝐷 ∖ { 1 }) ↔ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) |
178 | | ifnefalse 4427 |
. . . . . . . . . . . . . . 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 10957 |
. . . . . . . . . . . . . . 15
⊢ (if(𝑓 ∈ 𝑊, 1, 0) = 1 → -if(𝑓 ∈ 𝑊, 1, 0) = -1) |
181 | | negeq 10957 |
. . . . . . . . . . . . . . . 16
⊢ (if(𝑓 ∈ 𝑊, 1, 0) = 0 → -if(𝑓 ∈ 𝑊, 1, 0) = -0) |
182 | | neg0 11011 |
. . . . . . . . . . . . . . . 16
⊢ -0 =
0 |
183 | 181, 182 | eqtrdi 2789 |
. . . . . . . . . . . . . . 15
⊢ (if(𝑓 ∈ 𝑊, 1, 0) = 0 → -if(𝑓 ∈ 𝑊, 1, 0) = 0) |
184 | 180, 183 | ifsb 4428 |
. . . . . . . . . . . . . 14
⊢ -if(𝑓 ∈ 𝑊, 1, 0) = if(𝑓 ∈ 𝑊, -1, 0) |
185 | 179, 184 | eqtr4di 2791 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) → if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)) = -if(𝑓 ∈ 𝑊, 1, 0)) |
186 | 185 | oveq2d 7187 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) →
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = ((log‘𝑥) · -if(𝑓 ∈ 𝑊, 1, 0))) |
187 | 47 | adantr 484 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) → (log‘𝑥) ∈
ℂ) |
188 | 49, 51 | ifcli 4462 |
. . . . . . . . . . . . 13
⊢ if(𝑓 ∈ 𝑊, 1, 0) ∈ ℂ |
189 | | mulneg2 11156 |
. . . . . . . . . . . . 13
⊢
(((log‘𝑥)
∈ ℂ ∧ if(𝑓
∈ 𝑊, 1, 0) ∈
ℂ) → ((log‘𝑥) · -if(𝑓 ∈ 𝑊, 1, 0)) = -((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
190 | 187, 188,
189 | sylancl 589 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) →
((log‘𝑥) ·
-if(𝑓 ∈ 𝑊, 1, 0)) = -((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
191 | 186, 190 | eqtrd 2773 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ (𝑓 ∈ 𝐷 ∧ 𝑓 ≠ 1 )) →
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = -((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
192 | 177, 191 | sylan2b 597 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) →
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = -((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
193 | 192 | sumeq2dv 15154 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = Σ𝑓 ∈ (𝐷 ∖ { 1 })-((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
194 | | diffi 8828 |
. . . . . . . . . . 11
⊢ (𝐷 ∈ Fin → (𝐷 ∖ { 1 }) ∈
Fin) |
195 | 6, 194 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → (𝐷 ∖ { 1 }) ∈
Fin) |
196 | 47 | adantr 484 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) →
(log‘𝑥) ∈
ℂ) |
197 | | mulcl 10700 |
. . . . . . . . . . 11
⊢
(((log‘𝑥)
∈ ℂ ∧ if(𝑓
∈ 𝑊, 1, 0) ∈
ℂ) → ((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0)) ∈ ℂ) |
198 | 196, 188,
197 | sylancl 589 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) →
((log‘𝑥) ·
if(𝑓 ∈ 𝑊, 1, 0)) ∈
ℂ) |
199 | 195, 198 | fsumneg 15236 |
. . . . . . . . 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 15233 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) ·
Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓 ∈ 𝑊, 1, 0)) = Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0))) |
202 | | rpvmasum2.w |
. . . . . . . . . . . . . . . . 17
⊢ 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿‘𝑚)) / 𝑚) = 0} |
203 | 202 | ssrab3 3972 |
. . . . . . . . . . . . . . . 16
⊢ 𝑊 ⊆ (𝐷 ∖ { 1 }) |
204 | | difss 4023 |
. . . . . . . . . . . . . . . 16
⊢ (𝐷 ∖ { 1 }) ⊆ 𝐷 |
205 | 203, 204 | sstri 3887 |
. . . . . . . . . . . . . . 15
⊢ 𝑊 ⊆ 𝐷 |
206 | | ssfi 8773 |
. . . . . . . . . . . . . . 15
⊢ ((𝐷 ∈ Fin ∧ 𝑊 ⊆ 𝐷) → 𝑊 ∈ Fin) |
207 | 6, 205, 206 | sylancl 589 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑊 ∈ Fin) |
208 | | fsumconst 15239 |
. . . . . . . . . . . . . 14
⊢ ((𝑊 ∈ Fin ∧ 1 ∈
ℂ) → Σ𝑓
∈ 𝑊 1 =
((♯‘𝑊) ·
1)) |
209 | 207, 49, 208 | sylancl 589 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ 𝑊 1 = ((♯‘𝑊) · 1)) |
210 | 203 | a1i 11 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝑊 ⊆ (𝐷 ∖ { 1 })) |
211 | 49 | a1i 11 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 1 ∈
ℂ) |
212 | 211 | ralrimivw 3097 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
∀𝑓 ∈ 𝑊 1 ∈
ℂ) |
213 | 195 | olcd 873 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ((𝐷 ∖ { 1 }) ⊆
(ℤ≥‘1) ∨ (𝐷 ∖ { 1 }) ∈
Fin)) |
214 | | sumss2 15177 |
. . . . . . . . . . . . . 14
⊢ (((𝑊 ⊆ (𝐷 ∖ { 1 }) ∧ ∀𝑓 ∈ 𝑊 1 ∈ ℂ) ∧ ((𝐷 ∖ { 1 }) ⊆
(ℤ≥‘1) ∨ (𝐷 ∖ { 1 }) ∈ Fin)) →
Σ𝑓 ∈ 𝑊 1 = Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓 ∈ 𝑊, 1, 0)) |
215 | 210, 212,
213, 214 | syl21anc 837 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ 𝑊 1 = Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓 ∈ 𝑊, 1, 0)) |
216 | | hashcl 13810 |
. . . . . . . . . . . . . . . 16
⊢ (𝑊 ∈ Fin →
(♯‘𝑊) ∈
ℕ0) |
217 | 207, 216 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(♯‘𝑊) ∈
ℕ0) |
218 | 217 | nn0cnd 12039 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(♯‘𝑊) ∈
ℂ) |
219 | 218 | mulid1d 10737 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((♯‘𝑊) ·
1) = (♯‘𝑊)) |
220 | 209, 215,
219 | 3eqtr3d 2781 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓 ∈ 𝑊, 1, 0) = (♯‘𝑊)) |
221 | 220 | oveq2d 7187 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) ·
Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓 ∈ 𝑊, 1, 0)) = ((log‘𝑥) · (♯‘𝑊))) |
222 | 201, 221 | eqtr3d 2775 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0)) = ((log‘𝑥) · (♯‘𝑊))) |
223 | 222 | negeqd 10959 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
-Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 ∈ 𝑊, 1, 0)) = -((log‘𝑥) · (♯‘𝑊))) |
224 | 193, 199,
223 | 3eqtrd 2777 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = -((log‘𝑥) · (♯‘𝑊))) |
225 | 176, 224 | oveq12d 7189 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑓 ∈ { 1 }
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) + Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (((log‘𝑥) · 1) +
-((log‘𝑥) ·
(♯‘𝑊)))) |
226 | 47, 218 | mulcld 10740 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) ·
(♯‘𝑊)) ∈
ℂ) |
227 | 172, 226 | negsubd 11082 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(((log‘𝑥) · 1)
+ -((log‘𝑥) ·
(♯‘𝑊))) =
(((log‘𝑥) · 1)
− ((log‘𝑥)
· (♯‘𝑊)))) |
228 | 225, 227 | eqtrd 2773 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(Σ𝑓 ∈ { 1 }
((log‘𝑥) ·
if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) + Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (((log‘𝑥) · 1) −
((log‘𝑥) ·
(♯‘𝑊)))) |
229 | | disjdif 4362 |
. . . . . . . 8
⊢ ({ 1 } ∩
(𝐷 ∖ { 1 })) =
∅ |
230 | 229 | a1i 11 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ({ 1 } ∩
(𝐷 ∖ { 1 })) =
∅) |
231 | | undif2 4367 |
. . . . . . . 8
⊢ ({ 1 } ∪
(𝐷 ∖ { 1 })) = ({
1 } ∪
𝐷) |
232 | 170 | snssd 4698 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → { 1 } ⊆
𝐷) |
233 | | ssequn1 4071 |
. . . . . . . . 9
⊢ ({ 1 } ⊆
𝐷 ↔ ({ 1 } ∪ 𝐷) = 𝐷) |
234 | 232, 233 | sylib 221 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → ({ 1 } ∪ 𝐷) = 𝐷) |
235 | 231, 234 | eqtr2id 2786 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) → 𝐷 = ({ 1 } ∪ (𝐷 ∖ { 1 }))) |
236 | 230, 235,
6, 55 | fsumsplit 15191 |
. . . . . 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 11175 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · (1
− (♯‘𝑊)))
= (((log‘𝑥) ·
1) − ((log‘𝑥)
· (♯‘𝑊)))) |
238 | 228, 236,
237 | 3eqtr4rd 2784 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · (1
− (♯‘𝑊)))
= Σ𝑓 ∈ 𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) |
239 | 166, 238 | oveq12d 7189 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊)))) = (Σ𝑓 ∈ 𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓‘𝐴)) · ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) − Σ𝑓 ∈ 𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) |
240 | 56, 114, 239 | 3eqtr4d 2783 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ ℝ+) →
Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (((ϕ‘𝑁) · Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))) |
241 | 240 | mpteq2dva 5126 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))))) = (𝑥 ∈ ℝ+ ↦
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊)))))) |
242 | | rpssre 12480 |
. . . 4
⊢
ℝ+ ⊆ ℝ |
243 | 242 | a1i 11 |
. . 3
⊢ (𝜑 → ℝ+
⊆ ℝ) |
244 | 1, 5 | syl 17 |
. . 3
⊢ (𝜑 → 𝐷 ∈ Fin) |
245 | 17 | adantlr 715 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (𝑓‘𝐴) ∈ ℂ) |
246 | 245 | cjcld 14646 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (∗‘(𝑓‘𝐴)) ∈ ℂ) |
247 | 58, 55 | subcld 11076 |
. . . . 5
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) ∈ ℂ) |
248 | 246, 247 | mulcld 10740 |
. . . 4
⊢ (((𝜑 ∧ 𝑥 ∈ ℝ+) ∧ 𝑓 ∈ 𝐷) → ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) ∈
ℂ) |
249 | 248 | anasss 470 |
. . 3
⊢ ((𝜑 ∧ (𝑥 ∈ ℝ+ ∧ 𝑓 ∈ 𝐷)) → ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) ∈
ℂ) |
250 | 18 | adantr 484 |
. . . 4
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(∗‘(𝑓‘𝐴)) ∈ ℂ) |
251 | 247 | an32s 652 |
. . . 4
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) ∈ ℂ) |
252 | | o1const 15068 |
. . . . 5
⊢
((ℝ+ ⊆ ℝ ∧ (∗‘(𝑓‘𝐴)) ∈ ℂ) → (𝑥 ∈ ℝ+
↦ (∗‘(𝑓‘𝐴))) ∈ 𝑂(1)) |
253 | 242, 18, 252 | sylancr 590 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑥 ∈ ℝ+ ↦
(∗‘(𝑓‘𝐴))) ∈ 𝑂(1)) |
254 | | fveq1 6674 |
. . . . . . . . . . . 12
⊢ (𝑓 = 1 → (𝑓‘(𝐿‘𝑛)) = ( 1 ‘(𝐿‘𝑛))) |
255 | 254 | oveq1d 7186 |
. . . . . . . . . . 11
⊢ (𝑓 = 1 → ((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) = (( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
256 | 255 | sumeq2sdv 15155 |
. . . . . . . . . 10
⊢ (𝑓 = 1 → Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛))) |
257 | 256, 174 | oveq12d 7189 |
. . . . . . . . 9
⊢ (𝑓 = 1 → (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · 1))) |
258 | 257 | adantl 485 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · 1))) |
259 | 45 | recnd 10748 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (log‘𝑥) ∈
ℂ) |
260 | 259 | mulid1d 10737 |
. . . . . . . . 9
⊢ (𝑥 ∈ ℝ+
→ ((log‘𝑥)
· 1) = (log‘𝑥)) |
261 | 260 | oveq2d 7187 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
→ (Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · 1)) = (Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) |
262 | 258, 261 | sylan9eq 2793 |
. . . . . . 7
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) |
263 | 262 | mpteq2dva 5126 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) → (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) = (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))) |
264 | 8, 23, 1, 3, 4, 65 | rpvmasumlem 26223 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈
𝑂(1)) |
265 | 264 | ad2antrr 726 |
. . . . . 6
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) → (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((
1
‘(𝐿‘𝑛)) ·
((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈
𝑂(1)) |
266 | 263, 265 | eqeltrd 2833 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 = 1 ) → (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) ∈
𝑂(1)) |
267 | 178 | oveq2d 7187 |
. . . . . . . . . 10
⊢ (𝑓 ≠ 1 → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))) = ((log‘𝑥) · if(𝑓 ∈ 𝑊, -1, 0))) |
268 | 267 | oveq2d 7187 |
. . . . . . . . 9
⊢ (𝑓 ≠ 1 → (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 ∈ 𝑊, -1, 0)))) |
269 | 47 | adantlr 715 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(log‘𝑥) ∈
ℂ) |
270 | | mulcom 10702 |
. . . . . . . . . . . . . . 15
⊢
(((log‘𝑥)
∈ ℂ ∧ -1 ∈ ℂ) → ((log‘𝑥) · -1) = (-1 ·
(log‘𝑥))) |
271 | 269, 50, 270 | sylancl 589 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · -1)
= (-1 · (log‘𝑥))) |
272 | 269 | mulm1d 11171 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) → (-1
· (log‘𝑥)) =
-(log‘𝑥)) |
273 | 271, 272 | eqtrd 2773 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · -1)
= -(log‘𝑥)) |
274 | 269 | mul01d 10918 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) · 0)
= 0) |
275 | 273, 274 | ifeq12d 4436 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) → if(𝑓 ∈ 𝑊, ((log‘𝑥) · -1), ((log‘𝑥) · 0)) = if(𝑓 ∈ 𝑊, -(log‘𝑥), 0)) |
276 | | ovif2 7267 |
. . . . . . . . . . . 12
⊢
((log‘𝑥)
· if(𝑓 ∈ 𝑊, -1, 0)) = if(𝑓 ∈ 𝑊, ((log‘𝑥) · -1), ((log‘𝑥) · 0)) |
277 | | negeq 10957 |
. . . . . . . . . . . . 13
⊢ (if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = (log‘𝑥) → -if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = -(log‘𝑥)) |
278 | | negeq 10957 |
. . . . . . . . . . . . . 14
⊢ (if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = 0 → -if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = -0) |
279 | 278, 182 | eqtrdi 2789 |
. . . . . . . . . . . . 13
⊢ (if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = 0 → -if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = 0) |
280 | 277, 279 | ifsb 4428 |
. . . . . . . . . . . 12
⊢ -if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = if(𝑓 ∈ 𝑊, -(log‘𝑥), 0) |
281 | 275, 276,
280 | 3eqtr4g 2798 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
((log‘𝑥) ·
if(𝑓 ∈ 𝑊, -1, 0)) = -if(𝑓 ∈ 𝑊, (log‘𝑥), 0)) |
282 | 281 | oveq2d 7187 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 ∈ 𝑊, -1, 0))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − -if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) |
283 | 58 | an32s 652 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) |
284 | | ifcl 4460 |
. . . . . . . . . . . 12
⊢
(((log‘𝑥)
∈ ℂ ∧ 0 ∈ ℂ) → if(𝑓 ∈ 𝑊, (log‘𝑥), 0) ∈ ℂ) |
285 | 269, 51, 284 | sylancl 589 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) → if(𝑓 ∈ 𝑊, (log‘𝑥), 0) ∈ ℂ) |
286 | 283, 285 | subnegd 11083 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − -if(𝑓 ∈ 𝑊, (log‘𝑥), 0)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) |
287 | 282, 286 | eqtrd 2773 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑥 ∈ ℝ+) →
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 ∈ 𝑊, -1, 0))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) |
288 | 268, 287 | sylan9eqr 2795 |
. . . . . . . 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 5126 |
. . . . . 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 488 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → 𝑓 ≠ 1 ) |
294 | | eqid 2738 |
. . . . . . . 8
⊢ (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎)) = (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎)) |
295 | 8, 23, 291, 3, 4, 65, 292, 293, 294 | dchrmusumlema 26229 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → ∃𝑡∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦))) |
296 | 1 | adantr 484 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → 𝑁 ∈ ℕ) |
297 | 296 | ad2antrr 726 |
. . . . . . . . . . . 12
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑁 ∈ ℕ) |
298 | 292 | adantr 484 |
. . . . . . . . . . . 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 26240 |
. . . . . . . . . . 11
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑓 ∈ 𝑊 ↔ 𝑡 = 0)) |
304 | | ifbi 4437 |
. . . . . . . . . . . . 13
⊢ ((𝑓 ∈ 𝑊 ↔ 𝑡 = 0) → if(𝑓 ∈ 𝑊, (log‘𝑥), 0) = if(𝑡 = 0, (log‘𝑥), 0)) |
305 | 304 | oveq2d 7187 |
. . . . . . . . . . . 12
⊢ ((𝑓 ∈ 𝑊 ↔ 𝑡 = 0) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑡 = 0, (log‘𝑥), 0))) |
306 | 305 | mpteq2dv 5127 |
. . . . . . . . . . 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 26239 |
. . . . . . . . . 10
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑡 = 0, (log‘𝑥), 0))) ∈ 𝑂(1)) |
309 | 307, 308 | eqeltrd 2833 |
. . . . . . . . 9
⊢ ((((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧
(seq1( + , (𝑎 ∈
ℕ ↦ ((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) ∈ 𝑂(1)) |
310 | 309 | rexlimdvaa 3195 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → (∃𝑐 ∈ (0[,)+∞)(seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + ,
(𝑎 ∈ ℕ ↦
((𝑓‘(𝐿‘𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓 ∈ 𝑊, (log‘𝑥), 0))) ∈
𝑂(1))) |
311 | 310 | exlimdv 1939 |
. . . . . . 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 2833 |
. . . . 5
⊢ (((𝜑 ∧ 𝑓 ∈ 𝐷) ∧ 𝑓 ≠ 1 ) → (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) ∈
𝑂(1)) |
314 | 266, 313 | pm2.61dane 3021 |
. . . 4
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0))))) ∈
𝑂(1)) |
315 | 250, 251,
253, 314 | o1mul2 15073 |
. . 3
⊢ ((𝜑 ∧ 𝑓 ∈ 𝐷) → (𝑥 ∈ ℝ+ ↦
((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))))) ∈
𝑂(1)) |
316 | 243, 244,
249, 315 | fsumo1 15261 |
. 2
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
Σ𝑓 ∈ 𝐷 ((∗‘(𝑓‘𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿‘𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓 ∈ 𝑊, -1, 0)))))) ∈
𝑂(1)) |
317 | 241, 316 | eqeltrrd 2834 |
1
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(((ϕ‘𝑁) ·
Σ𝑛 ∈
((1...(⌊‘𝑥))
∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))) ∈
𝑂(1)) |