MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  rpvmasum2 Structured version   Visualization version   GIF version

Theorem rpvmasum2 25411
Description: A partial result along the lines of rpvmasum 25425. The sum of the von Mangoldt function over those integers 𝑛𝐴 (mod 𝑁) is asymptotic to (1 − 𝑀)(log𝑥 / ϕ(𝑥)) + 𝑂(1), where 𝑀 is the number of non-principal Dirichlet characters with Σ𝑛 ∈ ℕ, 𝑋(𝑛) / 𝑛 = 0. Our goal is to show this set is empty. Equation 9.4.3 of [Shapiro], p. 375. (Contributed by Mario Carneiro, 5-May-2016.)
Hypotheses
Ref Expression
rpvmasum.z 𝑍 = (ℤ/nℤ‘𝑁)
rpvmasum.l 𝐿 = (ℤRHom‘𝑍)
rpvmasum.a (𝜑𝑁 ∈ ℕ)
rpvmasum2.g 𝐺 = (DChr‘𝑁)
rpvmasum2.d 𝐷 = (Base‘𝐺)
rpvmasum2.1 1 = (0g𝐺)
rpvmasum2.w 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿𝑚)) / 𝑚) = 0}
rpvmasum2.u 𝑈 = (Unit‘𝑍)
rpvmasum2.b (𝜑𝐴𝑈)
rpvmasum2.t 𝑇 = (𝐿 “ {𝐴})
rpvmasum2.z1 ((𝜑𝑓𝑊) → 𝐴 = (1r𝑍))
Assertion
Ref Expression
rpvmasum2 (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))) ∈ 𝑂(1))
Distinct variable groups:   𝑚,𝑛,𝑥,𝑦,𝑓, 1   𝐴,𝑓,𝑚,𝑥,𝑦   𝑓,𝐺   𝑓,𝑁,𝑚,𝑛,𝑥,𝑦   𝜑,𝑓,𝑚,𝑛,𝑥   𝑇,𝑚,𝑛,𝑥,𝑦   𝑈,𝑚,𝑛,𝑥   𝑓,𝑊,𝑥   𝑓,𝑍,𝑚,𝑛,𝑥,𝑦   𝐷,𝑓,𝑚,𝑛,𝑥,𝑦   𝑓,𝐿,𝑚,𝑛,𝑥,𝑦   𝐴,𝑛
Allowed substitution hints:   𝜑(𝑦)   𝑇(𝑓)   𝑈(𝑦,𝑓)   𝐺(𝑥,𝑦,𝑚,𝑛)   𝑊(𝑦,𝑚,𝑛)

Proof of Theorem rpvmasum2
Dummy variables 𝑐 𝑡 𝑎 are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 rpvmasum.a . . . . . . 7 (𝜑𝑁 ∈ ℕ)
21adantr 468 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ ℕ)
3 rpvmasum2.g . . . . . . 7 𝐺 = (DChr‘𝑁)
4 rpvmasum2.d . . . . . . 7 𝐷 = (Base‘𝐺)
53, 4dchrfi 25190 . . . . . 6 (𝑁 ∈ ℕ → 𝐷 ∈ Fin)
62, 5syl 17 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → 𝐷 ∈ Fin)
7 fzfid 12992 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → (1...(⌊‘𝑥)) ∈ Fin)
8 rpvmasum.z . . . . . . . . . . . . 13 𝑍 = (ℤ/nℤ‘𝑁)
9 eqid 2805 . . . . . . . . . . . . 13 (Base‘𝑍) = (Base‘𝑍)
10 simpr 473 . . . . . . . . . . . . 13 ((𝜑𝑓𝐷) → 𝑓𝐷)
113, 8, 4, 9, 10dchrf 25177 . . . . . . . . . . . 12 ((𝜑𝑓𝐷) → 𝑓:(Base‘𝑍)⟶ℂ)
12 rpvmasum2.u . . . . . . . . . . . . . . 15 𝑈 = (Unit‘𝑍)
139, 12unitss 18858 . . . . . . . . . . . . . 14 𝑈 ⊆ (Base‘𝑍)
14 rpvmasum2.b . . . . . . . . . . . . . 14 (𝜑𝐴𝑈)
1513, 14sseldi 3793 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ (Base‘𝑍))
1615adantr 468 . . . . . . . . . . . 12 ((𝜑𝑓𝐷) → 𝐴 ∈ (Base‘𝑍))
1711, 16ffvelrnd 6579 . . . . . . . . . . 11 ((𝜑𝑓𝐷) → (𝑓𝐴) ∈ ℂ)
1817cjcld 14155 . . . . . . . . . 10 ((𝜑𝑓𝐷) → (∗‘(𝑓𝐴)) ∈ ℂ)
1918adantlr 697 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → (∗‘(𝑓𝐴)) ∈ ℂ)
2019adantrl 698 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑓𝐷)) → (∗‘(𝑓𝐴)) ∈ ℂ)
2111adantlr 697 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → 𝑓:(Base‘𝑍)⟶ℂ)
2221adantlr 697 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑓𝐷) → 𝑓:(Base‘𝑍)⟶ℂ)
231nnnn0d 11613 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℕ0)
24 rpvmasum.l . . . . . . . . . . . . . . . 16 𝐿 = (ℤRHom‘𝑍)
258, 9, 24znzrhfo 20099 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ0𝐿:ℤ–onto→(Base‘𝑍))
26 fof 6328 . . . . . . . . . . . . . . 15 (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍))
2723, 25, 263syl 18 . . . . . . . . . . . . . 14 (𝜑𝐿:ℤ⟶(Base‘𝑍))
2827adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → 𝐿:ℤ⟶(Base‘𝑍))
29 elfzelz 12561 . . . . . . . . . . . . 13 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℤ)
30 ffvelrn 6576 . . . . . . . . . . . . 13 ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑛 ∈ ℤ) → (𝐿𝑛) ∈ (Base‘𝑍))
3128, 29, 30syl2an 585 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐿𝑛) ∈ (Base‘𝑍))
3231adantr 468 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑓𝐷) → (𝐿𝑛) ∈ (Base‘𝑍))
3322, 32ffvelrnd 6579 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑓𝐷) → (𝑓‘(𝐿𝑛)) ∈ ℂ)
3433anasss 454 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑓𝐷)) → (𝑓‘(𝐿𝑛)) ∈ ℂ)
35 elfznn 12589 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
3635adantl 469 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
37 vmacl 25054 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
3836, 37syl 17 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
3938, 36nndivred 11351 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
4039recnd 10350 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
4140adantrr 699 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑓𝐷)) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
4234, 41mulcld 10342 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑓𝐷)) → ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
4320, 42mulcld 10342 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑓𝐷)) → ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ ℂ)
4443anass1rs 637 . . . . . 6 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ ℂ)
457, 44fsumcl 14683 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ ℂ)
46 relogcl 24532 . . . . . . . . 9 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
4746adantl 469 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
4847recnd 10350 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
4948adantr 468 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → (log‘𝑥) ∈ ℂ)
50 ax-1cn 10276 . . . . . . 7 1 ∈ ℂ
51 neg1cn 11402 . . . . . . . 8 -1 ∈ ℂ
52 0cn 10314 . . . . . . . 8 0 ∈ ℂ
5351, 52ifcli 4322 . . . . . . 7 if(𝑓𝑊, -1, 0) ∈ ℂ
5450, 53ifcli 4322 . . . . . 6 if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)) ∈ ℂ
55 mulcl 10302 . . . . . 6 (((log‘𝑥) ∈ ℂ ∧ if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)) ∈ ℂ) → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) ∈ ℂ)
5649, 54, 55sylancl 576 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) ∈ ℂ)
576, 45, 56fsumsub 14738 . . . 4 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓𝐷𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (Σ𝑓𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) − Σ𝑓𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))
5842anass1rs 637 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
597, 58fsumcl 14683 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
6019, 59, 56subdid 10768 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) = (((∗‘(𝑓𝐴)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((∗‘(𝑓𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))))
617, 19, 58fsummulc2 14734 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((∗‘(𝑓𝐴)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
6254a1i 11 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)) ∈ ℂ)
6319, 49, 62mul12d 10527 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((∗‘(𝑓𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = ((log‘𝑥) · ((∗‘(𝑓𝐴)) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))
64 ovif2 6965 . . . . . . . . . 10 ((∗‘(𝑓𝐴)) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = if(𝑓 = 1 , ((∗‘(𝑓𝐴)) · 1), ((∗‘(𝑓𝐴)) · if(𝑓𝑊, -1, 0)))
65 fveq1 6404 . . . . . . . . . . . . . . . . 17 (𝑓 = 1 → (𝑓𝐴) = ( 1𝐴))
66 rpvmasum2.1 . . . . . . . . . . . . . . . . . 18 1 = (0g𝐺)
671ad2antrr 708 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → 𝑁 ∈ ℕ)
6814ad2antrr 708 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → 𝐴𝑈)
693, 8, 66, 12, 67, 68dchr1 25192 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ( 1𝐴) = 1)
7065, 69sylan9eqr 2861 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓 = 1 ) → (𝑓𝐴) = 1)
7170fveq2d 6409 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓 = 1 ) → (∗‘(𝑓𝐴)) = (∗‘1))
72 1re 10322 . . . . . . . . . . . . . . . 16 1 ∈ ℝ
73 cjre 14098 . . . . . . . . . . . . . . . 16 (1 ∈ ℝ → (∗‘1) = 1)
7472, 73ax-mp 5 . . . . . . . . . . . . . . 15 (∗‘1) = 1
7571, 74syl6eq 2855 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓 = 1 ) → (∗‘(𝑓𝐴)) = 1)
7675oveq1d 6886 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓 = 1 ) → ((∗‘(𝑓𝐴)) · 1) = (1 · 1))
77 1t1e1 11449 . . . . . . . . . . . . 13 (1 · 1) = 1
7876, 77syl6eq 2855 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓 = 1 ) → ((∗‘(𝑓𝐴)) · 1) = 1)
7978ifeq1da 4306 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → if(𝑓 = 1 , ((∗‘(𝑓𝐴)) · 1), ((∗‘(𝑓𝐴)) · if(𝑓𝑊, -1, 0))) = if(𝑓 = 1 , 1, ((∗‘(𝑓𝐴)) · if(𝑓𝑊, -1, 0))))
80 df-ne 2978 . . . . . . . . . . . . 13 (𝑓1 ↔ ¬ 𝑓 = 1 )
81 ovif2 6965 . . . . . . . . . . . . . 14 ((∗‘(𝑓𝐴)) · if(𝑓𝑊, -1, 0)) = if(𝑓𝑊, ((∗‘(𝑓𝐴)) · -1), ((∗‘(𝑓𝐴)) · 0))
82 simplll 782 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) → 𝜑)
83 rpvmasum2.z1 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓𝑊) → 𝐴 = (1r𝑍))
8483fveq2d 6409 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓𝑊) → (𝑓𝐴) = (𝑓‘(1r𝑍)))
8582, 84sylan 571 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) ∧ 𝑓𝑊) → (𝑓𝐴) = (𝑓‘(1r𝑍)))
863, 8, 4dchrmhm 25176 . . . . . . . . . . . . . . . . . . . . . . . 24 𝐷 ⊆ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld))
87 simpr 473 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → 𝑓𝐷)
8886, 87sseldi 3793 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → 𝑓 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)))
89 eqid 2805 . . . . . . . . . . . . . . . . . . . . . . . . 25 (mulGrp‘𝑍) = (mulGrp‘𝑍)
90 eqid 2805 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1r𝑍) = (1r𝑍)
9189, 90ringidval 18701 . . . . . . . . . . . . . . . . . . . . . . . 24 (1r𝑍) = (0g‘(mulGrp‘𝑍))
92 eqid 2805 . . . . . . . . . . . . . . . . . . . . . . . . 25 (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
93 cnfld1 19975 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 = (1r‘ℂfld)
9492, 93ringidval 18701 . . . . . . . . . . . . . . . . . . . . . . . 24 1 = (0g‘(mulGrp‘ℂfld))
9591, 94mhm0 17544 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) → (𝑓‘(1r𝑍)) = 1)
9688, 95syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → (𝑓‘(1r𝑍)) = 1)
9796ad2antrr 708 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) ∧ 𝑓𝑊) → (𝑓‘(1r𝑍)) = 1)
9885, 97eqtrd 2839 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) ∧ 𝑓𝑊) → (𝑓𝐴) = 1)
9998fveq2d 6409 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) ∧ 𝑓𝑊) → (∗‘(𝑓𝐴)) = (∗‘1))
10099, 74syl6eq 2855 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) ∧ 𝑓𝑊) → (∗‘(𝑓𝐴)) = 1)
101100oveq1d 6886 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) ∧ 𝑓𝑊) → ((∗‘(𝑓𝐴)) · -1) = (1 · -1))
10251mulid2i 10327 . . . . . . . . . . . . . . . . 17 (1 · -1) = -1
103101, 102syl6eq 2855 . . . . . . . . . . . . . . . 16 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) ∧ 𝑓𝑊) → ((∗‘(𝑓𝐴)) · -1) = -1)
104103ifeq1da 4306 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) → if(𝑓𝑊, ((∗‘(𝑓𝐴)) · -1), ((∗‘(𝑓𝐴)) · 0)) = if(𝑓𝑊, -1, ((∗‘(𝑓𝐴)) · 0)))
10519adantr 468 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) → (∗‘(𝑓𝐴)) ∈ ℂ)
106105mul01d 10517 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) → ((∗‘(𝑓𝐴)) · 0) = 0)
107106ifeq2d 4295 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) → if(𝑓𝑊, -1, ((∗‘(𝑓𝐴)) · 0)) = if(𝑓𝑊, -1, 0))
108104, 107eqtrd 2839 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) → if(𝑓𝑊, ((∗‘(𝑓𝐴)) · -1), ((∗‘(𝑓𝐴)) · 0)) = if(𝑓𝑊, -1, 0))
10981, 108syl5eq 2851 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) → ((∗‘(𝑓𝐴)) · if(𝑓𝑊, -1, 0)) = if(𝑓𝑊, -1, 0))
11080, 109sylan2br 584 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ ¬ 𝑓 = 1 ) → ((∗‘(𝑓𝐴)) · if(𝑓𝑊, -1, 0)) = if(𝑓𝑊, -1, 0))
111110ifeq2da 4307 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → if(𝑓 = 1 , 1, ((∗‘(𝑓𝐴)) · if(𝑓𝑊, -1, 0))) = if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))
11279, 111eqtrd 2839 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → if(𝑓 = 1 , ((∗‘(𝑓𝐴)) · 1), ((∗‘(𝑓𝐴)) · if(𝑓𝑊, -1, 0))) = if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))
11364, 112syl5eq 2851 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((∗‘(𝑓𝐴)) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))
114113oveq2d 6887 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((log‘𝑥) · ((∗‘(𝑓𝐴)) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))
11563, 114eqtrd 2839 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((∗‘(𝑓𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))
11661, 115oveq12d 6889 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → (((∗‘(𝑓𝐴)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((∗‘(𝑓𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))
11760, 116eqtrd 2839 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))
118117sumeq2dv 14652 . . . 4 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) = Σ𝑓𝐷𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))
119 fzfid 12992 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
120 inss1 4026 . . . . . . . . 9 ((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥))
121 ssfi 8416 . . . . . . . . 9 (((1...(⌊‘𝑥)) ∈ Fin ∧ ((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥))) → ((1...(⌊‘𝑥)) ∩ 𝑇) ∈ Fin)
122119, 120, 121sylancl 576 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → ((1...(⌊‘𝑥)) ∩ 𝑇) ∈ Fin)
1232phicld 15690 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → (ϕ‘𝑁) ∈ ℕ)
124123nncnd 11318 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → (ϕ‘𝑁) ∈ ℂ)
125120a1i 11 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → ((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥)))
126125sselda 3795 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → 𝑛 ∈ (1...(⌊‘𝑥)))
127126, 40syldan 581 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
128122, 124, 127fsummulc2 14734 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)))
129124adantr 468 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ϕ‘𝑁) ∈ ℂ)
130129, 40mulcld 10342 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
131126, 130syldan 581 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
132131ralrimiva 3153 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → ∀𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
133119olcd 892 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → ((1...(⌊‘𝑥)) ⊆ (ℤ‘1) ∨ (1...(⌊‘𝑥)) ∈ Fin))
134 sumss2 14676 . . . . . . . 8 (((((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥)) ∧ ∀𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) ∧ ((1...(⌊‘𝑥)) ⊆ (ℤ‘1) ∨ (1...(⌊‘𝑥)) ∈ Fin)) → Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0))
135125, 132, 133, 134syl21anc 857 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0))
136 elin 3992 . . . . . . . . . . . . 13 (𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇) ↔ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑛𝑇))
137136baib 527 . . . . . . . . . . . 12 (𝑛 ∈ (1...(⌊‘𝑥)) → (𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇) ↔ 𝑛𝑇))
138137adantl 469 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇) ↔ 𝑛𝑇))
139 rpvmasum2.t . . . . . . . . . . . . 13 𝑇 = (𝐿 “ {𝐴})
140139eleq2i 2876 . . . . . . . . . . . 12 (𝑛𝑇𝑛 ∈ (𝐿 “ {𝐴}))
14128ffnd 6254 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → 𝐿 Fn ℤ)
142 fniniseg 6557 . . . . . . . . . . . . . 14 (𝐿 Fn ℤ → (𝑛 ∈ (𝐿 “ {𝐴}) ↔ (𝑛 ∈ ℤ ∧ (𝐿𝑛) = 𝐴)))
143142baibd 531 . . . . . . . . . . . . 13 ((𝐿 Fn ℤ ∧ 𝑛 ∈ ℤ) → (𝑛 ∈ (𝐿 “ {𝐴}) ↔ (𝐿𝑛) = 𝐴))
144141, 29, 143syl2an 585 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ (𝐿 “ {𝐴}) ↔ (𝐿𝑛) = 𝐴))
145140, 144syl5bb 274 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛𝑇 ↔ (𝐿𝑛) = 𝐴))
146138, 145bitr2d 271 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝐿𝑛) = 𝐴𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)))
14740mul02d 10516 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (0 · ((Λ‘𝑛) / 𝑛)) = 0)
148146, 147ifbieq2d 4301 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → if((𝐿𝑛) = 𝐴, ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), (0 · ((Λ‘𝑛) / 𝑛))) = if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0))
149 ovif 6964 . . . . . . . . . 10 (if((𝐿𝑛) = 𝐴, (ϕ‘𝑁), 0) · ((Λ‘𝑛) / 𝑛)) = if((𝐿𝑛) = 𝐴, ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), (0 · ((Λ‘𝑛) / 𝑛)))
1501ad2antrr 708 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈ ℕ)
151150, 5syl 17 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐷 ∈ Fin)
15219adantlr 697 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑓𝐷) → (∗‘(𝑓𝐴)) ∈ ℂ)
15333, 152mulcld 10342 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑓𝐷) → ((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) ∈ ℂ)
154151, 40, 153fsummulc1 14735 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑓𝐷 ((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑓𝐷 (((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) · ((Λ‘𝑛) / 𝑛)))
15514ad2antrr 708 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐴𝑈)
1563, 4, 8, 9, 12, 150, 31, 155sum2dchr 25209 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑓𝐷 ((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) = if((𝐿𝑛) = 𝐴, (ϕ‘𝑁), 0))
157156oveq1d 6886 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑓𝐷 ((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) · ((Λ‘𝑛) / 𝑛)) = (if((𝐿𝑛) = 𝐴, (ϕ‘𝑁), 0) · ((Λ‘𝑛) / 𝑛)))
15840adantr 468 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑓𝐷) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
159 mulass 10306 . . . . . . . . . . . . . 14 (((𝑓‘(𝐿𝑛)) ∈ ℂ ∧ (∗‘(𝑓𝐴)) ∈ ℂ ∧ ((Λ‘𝑛) / 𝑛) ∈ ℂ) → (((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) · ((Λ‘𝑛) / 𝑛)) = ((𝑓‘(𝐿𝑛)) · ((∗‘(𝑓𝐴)) · ((Λ‘𝑛) / 𝑛))))
160 mul12 10484 . . . . . . . . . . . . . 14 (((𝑓‘(𝐿𝑛)) ∈ ℂ ∧ (∗‘(𝑓𝐴)) ∈ ℂ ∧ ((Λ‘𝑛) / 𝑛) ∈ ℂ) → ((𝑓‘(𝐿𝑛)) · ((∗‘(𝑓𝐴)) · ((Λ‘𝑛) / 𝑛))) = ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
161159, 160eqtrd 2839 . . . . . . . . . . . . 13 (((𝑓‘(𝐿𝑛)) ∈ ℂ ∧ (∗‘(𝑓𝐴)) ∈ ℂ ∧ ((Λ‘𝑛) / 𝑛) ∈ ℂ) → (((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) · ((Λ‘𝑛) / 𝑛)) = ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
16233, 152, 158, 161syl3anc 1483 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑓𝐷) → (((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) · ((Λ‘𝑛) / 𝑛)) = ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
163162sumeq2dv 14652 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑓𝐷 (((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
164154, 157, 1633eqtr3d 2847 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (if((𝐿𝑛) = 𝐴, (ϕ‘𝑁), 0) · ((Λ‘𝑛) / 𝑛)) = Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
165149, 164syl5eqr 2853 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → if((𝐿𝑛) = 𝐴, ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), (0 · ((Λ‘𝑛) / 𝑛))) = Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
166148, 165eqtr3d 2841 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0) = Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
167166sumeq2dv 14652 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
168128, 135, 1673eqtrd 2843 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
169119, 6, 43fsumcom 14725 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) = Σ𝑓𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
170168, 169eqtrd 2839 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) = Σ𝑓𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
1713dchrabl 25189 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝐺 ∈ Abel)
172 ablgrp 18395 . . . . . . . . . 10 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
1734, 66grpidcl 17651 . . . . . . . . . 10 (𝐺 ∈ Grp → 1𝐷)
1742, 171, 172, 1734syl 19 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → 1𝐷)
17548mulid1d 10339 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) · 1) = (log‘𝑥))
176175, 48eqeltrd 2884 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) · 1) ∈ ℂ)
177 iftrue 4282 . . . . . . . . . . 11 (𝑓 = 1 → if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)) = 1)
178177oveq2d 6887 . . . . . . . . . 10 (𝑓 = 1 → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = ((log‘𝑥) · 1))
179178sumsn 14694 . . . . . . . . 9 (( 1𝐷 ∧ ((log‘𝑥) · 1) ∈ ℂ) → Σ𝑓 ∈ { 1 } ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = ((log‘𝑥) · 1))
180174, 176, 179syl2anc 575 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓 ∈ { 1 } ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = ((log‘𝑥) · 1))
181 eldifsn 4505 . . . . . . . . . . 11 (𝑓 ∈ (𝐷 ∖ { 1 }) ↔ (𝑓𝐷𝑓1 ))
182 ifnefalse 4288 . . . . . . . . . . . . . . 15 (𝑓1 → if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)) = if(𝑓𝑊, -1, 0))
183182ad2antll 711 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑓𝐷𝑓1 )) → if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)) = if(𝑓𝑊, -1, 0))
184 negeq 10555 . . . . . . . . . . . . . . 15 (if(𝑓𝑊, 1, 0) = 1 → -if(𝑓𝑊, 1, 0) = -1)
185 negeq 10555 . . . . . . . . . . . . . . . 16 (if(𝑓𝑊, 1, 0) = 0 → -if(𝑓𝑊, 1, 0) = -0)
186 neg0 10609 . . . . . . . . . . . . . . . 16 -0 = 0
187185, 186syl6eq 2855 . . . . . . . . . . . . . . 15 (if(𝑓𝑊, 1, 0) = 0 → -if(𝑓𝑊, 1, 0) = 0)
188184, 187ifsb 4289 . . . . . . . . . . . . . 14 -if(𝑓𝑊, 1, 0) = if(𝑓𝑊, -1, 0)
189183, 188syl6eqr 2857 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑓𝐷𝑓1 )) → if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)) = -if(𝑓𝑊, 1, 0))
190189oveq2d 6887 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑓𝐷𝑓1 )) → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = ((log‘𝑥) · -if(𝑓𝑊, 1, 0)))
19148adantr 468 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑓𝐷𝑓1 )) → (log‘𝑥) ∈ ℂ)
19250, 52ifcli 4322 . . . . . . . . . . . . 13 if(𝑓𝑊, 1, 0) ∈ ℂ
193 mulneg2 10749 . . . . . . . . . . . . 13 (((log‘𝑥) ∈ ℂ ∧ if(𝑓𝑊, 1, 0) ∈ ℂ) → ((log‘𝑥) · -if(𝑓𝑊, 1, 0)) = -((log‘𝑥) · if(𝑓𝑊, 1, 0)))
194191, 192, 193sylancl 576 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑓𝐷𝑓1 )) → ((log‘𝑥) · -if(𝑓𝑊, 1, 0)) = -((log‘𝑥) · if(𝑓𝑊, 1, 0)))
195190, 194eqtrd 2839 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑓𝐷𝑓1 )) → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = -((log‘𝑥) · if(𝑓𝑊, 1, 0)))
196181, 195sylan2b 583 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = -((log‘𝑥) · if(𝑓𝑊, 1, 0)))
197196sumeq2dv 14652 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = Σ𝑓 ∈ (𝐷 ∖ { 1 })-((log‘𝑥) · if(𝑓𝑊, 1, 0)))
198 diffi 8428 . . . . . . . . . . 11 (𝐷 ∈ Fin → (𝐷 ∖ { 1 }) ∈ Fin)
1996, 198syl 17 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → (𝐷 ∖ { 1 }) ∈ Fin)
20048adantr 468 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) → (log‘𝑥) ∈ ℂ)
201 mulcl 10302 . . . . . . . . . . 11 (((log‘𝑥) ∈ ℂ ∧ if(𝑓𝑊, 1, 0) ∈ ℂ) → ((log‘𝑥) · if(𝑓𝑊, 1, 0)) ∈ ℂ)
202200, 192, 201sylancl 576 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) → ((log‘𝑥) · if(𝑓𝑊, 1, 0)) ∈ ℂ)
203199, 202fsumneg 14737 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓 ∈ (𝐷 ∖ { 1 })-((log‘𝑥) · if(𝑓𝑊, 1, 0)) = -Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓𝑊, 1, 0)))
204192a1i 11 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) → if(𝑓𝑊, 1, 0) ∈ ℂ)
205199, 48, 204fsummulc2 14734 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) · Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓𝑊, 1, 0)) = Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓𝑊, 1, 0)))
206 rpvmasum2.w . . . . . . . . . . . . . . . . 17 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿𝑚)) / 𝑚) = 0}
207 ssrab2 3881 . . . . . . . . . . . . . . . . 17 {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿𝑚)) / 𝑚) = 0} ⊆ (𝐷 ∖ { 1 })
208206, 207eqsstri 3829 . . . . . . . . . . . . . . . 16 𝑊 ⊆ (𝐷 ∖ { 1 })
209 difss 3933 . . . . . . . . . . . . . . . 16 (𝐷 ∖ { 1 }) ⊆ 𝐷
210208, 209sstri 3804 . . . . . . . . . . . . . . 15 𝑊𝐷
211 ssfi 8416 . . . . . . . . . . . . . . 15 ((𝐷 ∈ Fin ∧ 𝑊𝐷) → 𝑊 ∈ Fin)
2126, 210, 211sylancl 576 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → 𝑊 ∈ Fin)
213 fsumconst 14740 . . . . . . . . . . . . . 14 ((𝑊 ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑓𝑊 1 = ((♯‘𝑊) · 1))
214212, 50, 213sylancl 576 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓𝑊 1 = ((♯‘𝑊) · 1))
215208a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → 𝑊 ⊆ (𝐷 ∖ { 1 }))
21650a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → 1 ∈ ℂ)
217216ralrimivw 3154 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → ∀𝑓𝑊 1 ∈ ℂ)
218199olcd 892 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → ((𝐷 ∖ { 1 }) ⊆ (ℤ‘1) ∨ (𝐷 ∖ { 1 }) ∈ Fin))
219 sumss2 14676 . . . . . . . . . . . . . 14 (((𝑊 ⊆ (𝐷 ∖ { 1 }) ∧ ∀𝑓𝑊 1 ∈ ℂ) ∧ ((𝐷 ∖ { 1 }) ⊆ (ℤ‘1) ∨ (𝐷 ∖ { 1 }) ∈ Fin)) → Σ𝑓𝑊 1 = Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓𝑊, 1, 0))
220215, 217, 218, 219syl21anc 857 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓𝑊 1 = Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓𝑊, 1, 0))
221 hashcl 13361 . . . . . . . . . . . . . . . 16 (𝑊 ∈ Fin → (♯‘𝑊) ∈ ℕ0)
222212, 221syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → (♯‘𝑊) ∈ ℕ0)
223222nn0cnd 11615 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → (♯‘𝑊) ∈ ℂ)
224223mulid1d 10339 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → ((♯‘𝑊) · 1) = (♯‘𝑊))
225214, 220, 2243eqtr3d 2847 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓𝑊, 1, 0) = (♯‘𝑊))
226225oveq2d 6887 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) · Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓𝑊, 1, 0)) = ((log‘𝑥) · (♯‘𝑊)))
227205, 226eqtr3d 2841 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓𝑊, 1, 0)) = ((log‘𝑥) · (♯‘𝑊)))
228227negeqd 10557 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → -Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓𝑊, 1, 0)) = -((log‘𝑥) · (♯‘𝑊)))
229197, 203, 2283eqtrd 2843 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = -((log‘𝑥) · (♯‘𝑊)))
230180, 229oveq12d 6889 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → (Σ𝑓 ∈ { 1 } ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) + Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (((log‘𝑥) · 1) + -((log‘𝑥) · (♯‘𝑊))))
23148, 223mulcld 10342 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) · (♯‘𝑊)) ∈ ℂ)
232176, 231negsubd 10680 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → (((log‘𝑥) · 1) + -((log‘𝑥) · (♯‘𝑊))) = (((log‘𝑥) · 1) − ((log‘𝑥) · (♯‘𝑊))))
233230, 232eqtrd 2839 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → (Σ𝑓 ∈ { 1 } ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) + Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (((log‘𝑥) · 1) − ((log‘𝑥) · (♯‘𝑊))))
234 disjdif 4233 . . . . . . . 8 ({ 1 } ∩ (𝐷 ∖ { 1 })) = ∅
235234a1i 11 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → ({ 1 } ∩ (𝐷 ∖ { 1 })) = ∅)
236 undif2 4237 . . . . . . . 8 ({ 1 } ∪ (𝐷 ∖ { 1 })) = ({ 1 } ∪ 𝐷)
237174snssd 4527 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → { 1 } ⊆ 𝐷)
238 ssequn1 3979 . . . . . . . . 9 ({ 1 } ⊆ 𝐷 ↔ ({ 1 } ∪ 𝐷) = 𝐷)
239237, 238sylib 209 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → ({ 1 } ∪ 𝐷) = 𝐷)
240236, 239syl5req 2852 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → 𝐷 = ({ 1 } ∪ (𝐷 ∖ { 1 })))
241235, 240, 6, 56fsumsplit 14690 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = (Σ𝑓 ∈ { 1 } ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) + Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))
24248, 216, 223subdid 10768 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) · (1 − (♯‘𝑊))) = (((log‘𝑥) · 1) − ((log‘𝑥) · (♯‘𝑊))))
243233, 241, 2423eqtr4rd 2850 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) · (1 − (♯‘𝑊))) = Σ𝑓𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))
244170, 243oveq12d 6889 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊)))) = (Σ𝑓𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) − Σ𝑓𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))
24557, 118, 2443eqtr4d 2849 . . 3 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) = (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊)))))
246245mpteq2dva 4934 . 2 (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))) = (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))))
247 rpssre 12053 . . . 4 + ⊆ ℝ
248247a1i 11 . . 3 (𝜑 → ℝ+ ⊆ ℝ)
2491, 5syl 17 . . 3 (𝜑𝐷 ∈ Fin)
25017adantlr 697 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → (𝑓𝐴) ∈ ℂ)
251250cjcld 14155 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → (∗‘(𝑓𝐴)) ∈ ℂ)
25259, 56subcld 10674 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) ∈ ℂ)
253251, 252mulcld 10342 . . . 4 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) ∈ ℂ)
254253anasss 454 . . 3 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑓𝐷)) → ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) ∈ ℂ)
25518adantr 468 . . . 4 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → (∗‘(𝑓𝐴)) ∈ ℂ)
256252an32s 634 . . . 4 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) ∈ ℂ)
257 o1const 14569 . . . . 5 ((ℝ+ ⊆ ℝ ∧ (∗‘(𝑓𝐴)) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (∗‘(𝑓𝐴))) ∈ 𝑂(1))
258247, 18, 257sylancr 577 . . . 4 ((𝜑𝑓𝐷) → (𝑥 ∈ ℝ+ ↦ (∗‘(𝑓𝐴))) ∈ 𝑂(1))
259 fveq1 6404 . . . . . . . . . . . 12 (𝑓 = 1 → (𝑓‘(𝐿𝑛)) = ( 1 ‘(𝐿𝑛)))
260259oveq1d 6886 . . . . . . . . . . 11 (𝑓 = 1 → ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) = (( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)))
261260sumeq2sdv 14654 . . . . . . . . . 10 (𝑓 = 1 → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)))
262261, 178oveq12d 6889 . . . . . . . . 9 (𝑓 = 1 → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · 1)))
263262adantl 469 . . . . . . . 8 (((𝜑𝑓𝐷) ∧ 𝑓 = 1 ) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · 1)))
26446recnd 10350 . . . . . . . . . 10 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℂ)
265264mulid1d 10339 . . . . . . . . 9 (𝑥 ∈ ℝ+ → ((log‘𝑥) · 1) = (log‘𝑥))
266265oveq2d 6887 . . . . . . . 8 (𝑥 ∈ ℝ+ → (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · 1)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))
267263, 266sylan9eq 2859 . . . . . . 7 ((((𝜑𝑓𝐷) ∧ 𝑓 = 1 ) ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))
268267mpteq2dva 4934 . . . . . 6 (((𝜑𝑓𝐷) ∧ 𝑓 = 1 ) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))))
2698, 24, 1, 3, 4, 66rpvmasumlem 25386 . . . . . . 7 (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1))
270269ad2antrr 708 . . . . . 6 (((𝜑𝑓𝐷) ∧ 𝑓 = 1 ) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1))
271268, 270eqeltrd 2884 . . . . 5 (((𝜑𝑓𝐷) ∧ 𝑓 = 1 ) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) ∈ 𝑂(1))
272182oveq2d 6887 . . . . . . . . . 10 (𝑓1 → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = ((log‘𝑥) · if(𝑓𝑊, -1, 0)))
273272oveq2d 6887 . . . . . . . . 9 (𝑓1 → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓𝑊, -1, 0))))
27448adantlr 697 . . . . . . . . . . . . . . 15 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
275 mulcom 10304 . . . . . . . . . . . . . . 15 (((log‘𝑥) ∈ ℂ ∧ -1 ∈ ℂ) → ((log‘𝑥) · -1) = (-1 · (log‘𝑥)))
276274, 51, 275sylancl 576 . . . . . . . . . . . . . 14 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥) · -1) = (-1 · (log‘𝑥)))
277274mulm1d 10764 . . . . . . . . . . . . . 14 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → (-1 · (log‘𝑥)) = -(log‘𝑥))
278276, 277eqtrd 2839 . . . . . . . . . . . . 13 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥) · -1) = -(log‘𝑥))
279274mul01d 10517 . . . . . . . . . . . . 13 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥) · 0) = 0)
280278, 279ifeq12d 4296 . . . . . . . . . . . 12 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → if(𝑓𝑊, ((log‘𝑥) · -1), ((log‘𝑥) · 0)) = if(𝑓𝑊, -(log‘𝑥), 0))
281 ovif2 6965 . . . . . . . . . . . 12 ((log‘𝑥) · if(𝑓𝑊, -1, 0)) = if(𝑓𝑊, ((log‘𝑥) · -1), ((log‘𝑥) · 0))
282 negeq 10555 . . . . . . . . . . . . 13 (if(𝑓𝑊, (log‘𝑥), 0) = (log‘𝑥) → -if(𝑓𝑊, (log‘𝑥), 0) = -(log‘𝑥))
283 negeq 10555 . . . . . . . . . . . . . 14 (if(𝑓𝑊, (log‘𝑥), 0) = 0 → -if(𝑓𝑊, (log‘𝑥), 0) = -0)
284283, 186syl6eq 2855 . . . . . . . . . . . . 13 (if(𝑓𝑊, (log‘𝑥), 0) = 0 → -if(𝑓𝑊, (log‘𝑥), 0) = 0)
285282, 284ifsb 4289 . . . . . . . . . . . 12 -if(𝑓𝑊, (log‘𝑥), 0) = if(𝑓𝑊, -(log‘𝑥), 0)
286280, 281, 2853eqtr4g 2864 . . . . . . . . . . 11 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥) · if(𝑓𝑊, -1, 0)) = -if(𝑓𝑊, (log‘𝑥), 0))
287286oveq2d 6887 . . . . . . . . . 10 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓𝑊, -1, 0))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − -if(𝑓𝑊, (log‘𝑥), 0)))
28859an32s 634 . . . . . . . . . . 11 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
289 ifcl 4320 . . . . . . . . . . . 12 (((log‘𝑥) ∈ ℂ ∧ 0 ∈ ℂ) → if(𝑓𝑊, (log‘𝑥), 0) ∈ ℂ)
290274, 52, 289sylancl 576 . . . . . . . . . . 11 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → if(𝑓𝑊, (log‘𝑥), 0) ∈ ℂ)
291288, 290subnegd 10681 . . . . . . . . . 10 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − -if(𝑓𝑊, (log‘𝑥), 0)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0)))
292287, 291eqtrd 2839 . . . . . . . . 9 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓𝑊, -1, 0))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0)))
293273, 292sylan9eqr 2861 . . . . . . . 8 ((((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) ∧ 𝑓1 ) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0)))
294293an32s 634 . . . . . . 7 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0)))
295294mpteq2dva 4934 . . . . . 6 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0))))
2961ad2antrr 708 . . . . . . . 8 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → 𝑁 ∈ ℕ)
297 simplr 776 . . . . . . . 8 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → 𝑓𝐷)
298 simpr 473 . . . . . . . 8 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → 𝑓1 )
299 eqid 2805 . . . . . . . 8 (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)) = (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))
3008, 24, 296, 3, 4, 66, 297, 298, 299dchrmusumlema 25392 . . . . . . 7 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → ∃𝑡𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))
3011adantr 468 . . . . . . . . . . . . 13 ((𝜑𝑓𝐷) → 𝑁 ∈ ℕ)
302301ad2antrr 708 . . . . . . . . . . . 12 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑁 ∈ ℕ)
303297adantr 468 . . . . . . . . . . . 12 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑓𝐷)
304 simplr 776 . . . . . . . . . . . 12 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑓1 )
305 simprl 778 . . . . . . . . . . . 12 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑐 ∈ (0[,)+∞))
306 simprrl 790 . . . . . . . . . . . 12 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡)
307 simprrr 791 . . . . . . . . . . . 12 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦))
3088, 24, 302, 3, 4, 66, 303, 304, 299, 305, 306, 307, 206dchrvmaeq0 25403 . . . . . . . . . . 11 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑓𝑊𝑡 = 0))
309 ifbi 4297 . . . . . . . . . . . . 13 ((𝑓𝑊𝑡 = 0) → if(𝑓𝑊, (log‘𝑥), 0) = if(𝑡 = 0, (log‘𝑥), 0))
310309oveq2d 6887 . . . . . . . . . . . 12 ((𝑓𝑊𝑡 = 0) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑡 = 0, (log‘𝑥), 0)))
311310mpteq2dv 4935 . . . . . . . . . . 11 ((𝑓𝑊𝑡 = 0) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑡 = 0, (log‘𝑥), 0))))
312308, 311syl 17 . . . . . . . . . 10 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑡 = 0, (log‘𝑥), 0))))
3138, 24, 302, 3, 4, 66, 303, 304, 299, 305, 306, 307dchrvmasumif 25402 . . . . . . . . . 10 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑡 = 0, (log‘𝑥), 0))) ∈ 𝑂(1))
314312, 313eqeltrd 2884 . . . . . . . . 9 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0))) ∈ 𝑂(1))
315314rexlimdvaa 3219 . . . . . . . 8 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → (∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0))) ∈ 𝑂(1)))
316315exlimdv 2026 . . . . . . 7 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → (∃𝑡𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0))) ∈ 𝑂(1)))
317300, 316mpd 15 . . . . . 6 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0))) ∈ 𝑂(1))
318295, 317eqeltrd 2884 . . . . 5 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) ∈ 𝑂(1))
319271, 318pm2.61dane 3064 . . . 4 ((𝜑𝑓𝐷) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) ∈ 𝑂(1))
320255, 256, 258, 319o1mul2 14574 . . 3 ((𝜑𝑓𝐷) → (𝑥 ∈ ℝ+ ↦ ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))) ∈ 𝑂(1))
321248, 249, 254, 320fsumo1 14762 . 2 (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))) ∈ 𝑂(1))
322246, 321eqeltrrd 2885 1 (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))) ∈ 𝑂(1))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 197  wa 384  wo 865  w3a 1100   = wceq 1637  wex 1859  wcel 2158  wne 2977  wral 3095  wrex 3096  {crab 3099  cdif 3763  cun 3764  cin 3765  wss 3766  c0 4113  ifcif 4276  {csn 4367   class class class wbr 4840  cmpt 4919  ccnv 5307  cima 5311   Fn wfn 6093  wf 6094  ontowfo 6096  cfv 6098  (class class class)co 6871  Fincfn 8189  cc 10216  cr 10217  0cc0 10218  1c1 10219   + caddc 10221   · cmul 10223  +∞cpnf 10353  cle 10357  cmin 10548  -cneg 10549   / cdiv 10966  cn 11302  0cn0 11555  cz 11639  cuz 11900  +crp 12042  [,)cico 12391  ...cfz 12545  cfl 12811  seqcseq 13020  chash 13333  ccj 14055  abscabs 14193  cli 14434  𝑂(1)co1 14436  Σcsu 14635  ϕcphi 15682  Basecbs 16064  0gc0g 16301   MndHom cmhm 17534  Grpcgrp 17623  Abelcabl 18391  mulGrpcmgp 18687  1rcur 18699  Unitcui 18837  fldccnfld 19950  ℤRHomczrh 20052  ℤ/nczn 20055  logclog 24511  Λcvma 25028  DChrcdchr 25167
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1880  ax-4 1897  ax-5 2004  ax-6 2070  ax-7 2106  ax-8 2160  ax-9 2167  ax-10 2187  ax-11 2203  ax-12 2216  ax-13 2422  ax-ext 2784  ax-rep 4960  ax-sep 4971  ax-nul 4980  ax-pow 5032  ax-pr 5093  ax-un 7176  ax-inf2 8782  ax-cnex 10274  ax-resscn 10275  ax-1cn 10276  ax-icn 10277  ax-addcl 10278  ax-addrcl 10279  ax-mulcl 10280  ax-mulrcl 10281  ax-mulcom 10282  ax-addass 10283  ax-mulass 10284  ax-distr 10285  ax-i2m1 10286  ax-1ne0 10287  ax-1rid 10288  ax-rnegex 10289  ax-rrecex 10290  ax-cnre 10291  ax-pre-lttri 10292  ax-pre-lttrn 10293  ax-pre-ltadd 10294  ax-pre-mulgt0 10295  ax-pre-sup 10296  ax-addf 10297  ax-mulf 10298
This theorem depends on definitions:  df-bi 198  df-an 385  df-or 866  df-3or 1101  df-3an 1102  df-tru 1641  df-fal 1651  df-ex 1860  df-nf 1865  df-sb 2063  df-eu 2636  df-mo 2637  df-clab 2792  df-cleq 2798  df-clel 2801  df-nfc 2936  df-ne 2978  df-nel 3081  df-ral 3100  df-rex 3101  df-reu 3102  df-rmo 3103  df-rab 3104  df-v 3392  df-sbc 3631  df-csb 3726  df-dif 3769  df-un 3771  df-in 3773  df-ss 3780  df-pss 3782  df-nul 4114  df-if 4277  df-pw 4350  df-sn 4368  df-pr 4370  df-tp 4372  df-op 4374  df-uni 4627  df-int 4666  df-iun 4710  df-iin 4711  df-disj 4809  df-br 4841  df-opab 4903  df-mpt 4920  df-tr 4943  df-id 5216  df-eprel 5221  df-po 5229  df-so 5230  df-fr 5267  df-se 5268  df-we 5269  df-xp 5314  df-rel 5315  df-cnv 5316  df-co 5317  df-dm 5318  df-rn 5319  df-res 5320  df-ima 5321  df-pred 5890  df-ord 5936  df-on 5937  df-lim 5938  df-suc 5939  df-iota 6061  df-fun 6100  df-fn 6101  df-f 6102  df-f1 6103  df-fo 6104  df-f1o 6105  df-fv 6106  df-isom 6107  df-riota 6832  df-ov 6874  df-oprab 6875  df-mpt2 6876  df-of 7124  df-rpss 7164  df-om 7293  df-1st 7395  df-2nd 7396  df-supp 7527  df-tpos 7584  df-wrecs 7639  df-recs 7701  df-rdg 7739  df-1o 7793  df-2o 7794  df-oadd 7797  df-omul 7798  df-er 7976  df-ec 7978  df-qs 7982  df-map 8091  df-pm 8092  df-ixp 8143  df-en 8190  df-dom 8191  df-sdom 8192  df-fin 8193  df-fsupp 8512  df-fi 8553  df-sup 8584  df-inf 8585  df-oi 8651  df-card 9045  df-acn 9048  df-cda 9272  df-pnf 10358  df-mnf 10359  df-xr 10360  df-ltxr 10361  df-le 10362  df-sub 10550  df-neg 10551  df-div 10967  df-nn 11303  df-2 11360  df-3 11361  df-4 11362  df-5 11363  df-6 11364  df-7 11365  df-8 11366  df-9 11367  df-n0 11556  df-xnn0 11626  df-z 11640  df-dec 11756  df-uz 11901  df-q 12004  df-rp 12043  df-xneg 12158  df-xadd 12159  df-xmul 12160  df-ioo 12393  df-ioc 12394  df-ico 12395  df-icc 12396  df-fz 12546  df-fzo 12686  df-fl 12813  df-mod 12889  df-seq 13021  df-exp 13080  df-fac 13277  df-bc 13306  df-hash 13334  df-word 13506  df-concat 13508  df-s1 13509  df-shft 14026  df-cj 14058  df-re 14059  df-im 14060  df-sqrt 14194  df-abs 14195  df-limsup 14421  df-clim 14438  df-rlim 14439  df-o1 14440  df-lo1 14441  df-sum 14636  df-ef 15014  df-e 15015  df-sin 15016  df-cos 15017  df-pi 15019  df-dvds 15200  df-gcd 15432  df-prm 15600  df-phi 15684  df-pc 15755  df-struct 16066  df-ndx 16067  df-slot 16068  df-base 16070  df-sets 16071  df-ress 16072  df-plusg 16162  df-mulr 16163  df-starv 16164  df-sca 16165  df-vsca 16166  df-ip 16167  df-tset 16168  df-ple 16169  df-ds 16171  df-unif 16172  df-hom 16173  df-cco 16174  df-rest 16284  df-topn 16285  df-0g 16303  df-gsum 16304  df-topgen 16305  df-pt 16306  df-prds 16309  df-xrs 16363  df-qtop 16368  df-imas 16369  df-qus 16370  df-xps 16371  df-mre 16447  df-mrc 16448  df-acs 16450  df-mgm 17443  df-sgrp 17485  df-mnd 17496  df-mhm 17536  df-submnd 17537  df-grp 17626  df-minusg 17627  df-sbg 17628  df-mulg 17742  df-subg 17789  df-nsg 17790  df-eqg 17791  df-ghm 17856  df-gim 17899  df-ga 17920  df-cntz 17947  df-oppg 17973  df-od 18145  df-gex 18146  df-pgp 18147  df-lsm 18248  df-pj1 18249  df-cmn 18392  df-abl 18393  df-cyg 18477  df-dprd 18592  df-dpj 18593  df-mgp 18688  df-ur 18700  df-ring 18747  df-cring 18748  df-oppr 18821  df-dvdsr 18839  df-unit 18840  df-invr 18870  df-dvr 18881  df-rnghom 18915  df-drng 18949  df-subrg 18978  df-lmod 19065  df-lss 19133  df-lsp 19175  df-sra 19377  df-rgmod 19378  df-lidl 19379  df-rsp 19380  df-2idl 19437  df-psmet 19942  df-xmet 19943  df-met 19944  df-bl 19945  df-mopn 19946  df-fbas 19947  df-fg 19948  df-cnfld 19951  df-zring 20023  df-zrh 20056  df-zn 20059  df-top 20908  df-topon 20925  df-topsp 20947  df-bases 20960  df-cld 21033  df-ntr 21034  df-cls 21035  df-nei 21112  df-lp 21150  df-perf 21151  df-cn 21241  df-cnp 21242  df-haus 21329  df-cmp 21400  df-tx 21575  df-hmeo 21768  df-fil 21859  df-fm 21951  df-flim 21952  df-flf 21953  df-xms 22334  df-ms 22335  df-tms 22336  df-cncf 22890  df-0p 23647  df-limc 23840  df-dv 23841  df-ply 24154  df-idp 24155  df-coe 24156  df-dgr 24157  df-quot 24256  df-log 24513  df-cxp 24514  df-em 24929  df-cht 25033  df-vma 25034  df-chp 25035  df-ppi 25036  df-mu 25037  df-dchr 25168
This theorem is referenced by:  dchrisum0re  25412  rpvmasum  25425
  Copyright terms: Public domain W3C validator