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

Theorem rpvmasum2 25653
Description: A partial result along the lines of rpvmasum 25667. 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 474 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → 𝑁 ∈ ℕ)
3 rpvmasum2.g . . . . . . 7 𝐺 = (DChr‘𝑁)
4 rpvmasum2.d . . . . . . 7 𝐷 = (Base‘𝐺)
53, 4dchrfi 25432 . . . . . 6 (𝑁 ∈ ℕ → 𝐷 ∈ Fin)
62, 5syl 17 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → 𝐷 ∈ Fin)
7 fzfid 13091 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → (1...(⌊‘𝑥)) ∈ Fin)
8 rpvmasum.z . . . . . . . . . . . . 13 𝑍 = (ℤ/nℤ‘𝑁)
9 eqid 2778 . . . . . . . . . . . . 13 (Base‘𝑍) = (Base‘𝑍)
10 simpr 479 . . . . . . . . . . . . 13 ((𝜑𝑓𝐷) → 𝑓𝐷)
113, 8, 4, 9, 10dchrf 25419 . . . . . . . . . . . 12 ((𝜑𝑓𝐷) → 𝑓:(Base‘𝑍)⟶ℂ)
12 rpvmasum2.u . . . . . . . . . . . . . . 15 𝑈 = (Unit‘𝑍)
139, 12unitss 19047 . . . . . . . . . . . . . 14 𝑈 ⊆ (Base‘𝑍)
14 rpvmasum2.b . . . . . . . . . . . . . 14 (𝜑𝐴𝑈)
1513, 14sseldi 3819 . . . . . . . . . . . . 13 (𝜑𝐴 ∈ (Base‘𝑍))
1615adantr 474 . . . . . . . . . . . 12 ((𝜑𝑓𝐷) → 𝐴 ∈ (Base‘𝑍))
1711, 16ffvelrnd 6624 . . . . . . . . . . 11 ((𝜑𝑓𝐷) → (𝑓𝐴) ∈ ℂ)
1817cjcld 14343 . . . . . . . . . 10 ((𝜑𝑓𝐷) → (∗‘(𝑓𝐴)) ∈ ℂ)
1918adantlr 705 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → (∗‘(𝑓𝐴)) ∈ ℂ)
2019adantrl 706 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑓𝐷)) → (∗‘(𝑓𝐴)) ∈ ℂ)
2111adantlr 705 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → 𝑓:(Base‘𝑍)⟶ℂ)
2221adantlr 705 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑓𝐷) → 𝑓:(Base‘𝑍)⟶ℂ)
231nnnn0d 11702 . . . . . . . . . . . . . . 15 (𝜑𝑁 ∈ ℕ0)
24 rpvmasum.l . . . . . . . . . . . . . . . 16 𝐿 = (ℤRHom‘𝑍)
258, 9, 24znzrhfo 20291 . . . . . . . . . . . . . . 15 (𝑁 ∈ ℕ0𝐿:ℤ–onto→(Base‘𝑍))
26 fof 6366 . . . . . . . . . . . . . . 15 (𝐿:ℤ–onto→(Base‘𝑍) → 𝐿:ℤ⟶(Base‘𝑍))
2723, 25, 263syl 18 . . . . . . . . . . . . . 14 (𝜑𝐿:ℤ⟶(Base‘𝑍))
2827adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → 𝐿:ℤ⟶(Base‘𝑍))
29 elfzelz 12659 . . . . . . . . . . . . 13 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℤ)
30 ffvelrn 6621 . . . . . . . . . . . . 13 ((𝐿:ℤ⟶(Base‘𝑍) ∧ 𝑛 ∈ ℤ) → (𝐿𝑛) ∈ (Base‘𝑍))
3128, 29, 30syl2an 589 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝐿𝑛) ∈ (Base‘𝑍))
3231adantr 474 . . . . . . . . . . 11 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑓𝐷) → (𝐿𝑛) ∈ (Base‘𝑍))
3322, 32ffvelrnd 6624 . . . . . . . . . 10 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑓𝐷) → (𝑓‘(𝐿𝑛)) ∈ ℂ)
3433anasss 460 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑓𝐷)) → (𝑓‘(𝐿𝑛)) ∈ ℂ)
35 elfznn 12687 . . . . . . . . . . . . . 14 (𝑛 ∈ (1...(⌊‘𝑥)) → 𝑛 ∈ ℕ)
3635adantl 475 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ)
37 vmacl 25296 . . . . . . . . . . . . 13 (𝑛 ∈ ℕ → (Λ‘𝑛) ∈ ℝ)
3836, 37syl 17 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈ ℝ)
3938, 36nndivred 11429 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℝ)
4039recnd 10405 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
4140adantrr 707 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑓𝐷)) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
4234, 41mulcld 10397 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑓𝐷)) → ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
4320, 42mulcld 10397 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑓𝐷)) → ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ ℂ)
4443anass1rs 645 . . . . . 6 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ ℂ)
457, 44fsumcl 14871 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) ∈ ℂ)
46 relogcl 24759 . . . . . . . . 9 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℝ)
4746adantl 475 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℝ)
4847recnd 10405 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
4948adantr 474 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → (log‘𝑥) ∈ ℂ)
50 ax-1cn 10330 . . . . . . 7 1 ∈ ℂ
51 neg1cn 11496 . . . . . . . 8 -1 ∈ ℂ
52 0cn 10368 . . . . . . . 8 0 ∈ ℂ
5351, 52ifcli 4353 . . . . . . 7 if(𝑓𝑊, -1, 0) ∈ ℂ
5450, 53ifcli 4353 . . . . . 6 if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)) ∈ ℂ
55 mulcl 10356 . . . . . 6 (((log‘𝑥) ∈ ℂ ∧ if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)) ∈ ℂ) → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) ∈ ℂ)
5649, 54, 55sylancl 580 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) ∈ ℂ)
576, 45, 56fsumsub 14924 . . . 4 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓𝐷𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (Σ𝑓𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) − Σ𝑓𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))
5842anass1rs 645 . . . . . . . 8 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
597, 58fsumcl 14871 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
6019, 59, 56subdid 10831 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) = (((∗‘(𝑓𝐴)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((∗‘(𝑓𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))))
617, 19, 58fsummulc2 14920 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((∗‘(𝑓𝐴)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
6254a1i 11 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)) ∈ ℂ)
6319, 49, 62mul12d 10585 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((∗‘(𝑓𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = ((log‘𝑥) · ((∗‘(𝑓𝐴)) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))
64 ovif2 7015 . . . . . . . . . 10 ((∗‘(𝑓𝐴)) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = if(𝑓 = 1 , ((∗‘(𝑓𝐴)) · 1), ((∗‘(𝑓𝐴)) · if(𝑓𝑊, -1, 0)))
65 fveq1 6445 . . . . . . . . . . . . . . . . 17 (𝑓 = 1 → (𝑓𝐴) = ( 1𝐴))
66 rpvmasum2.1 . . . . . . . . . . . . . . . . . 18 1 = (0g𝐺)
671ad2antrr 716 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → 𝑁 ∈ ℕ)
6814ad2antrr 716 . . . . . . . . . . . . . . . . . 18 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → 𝐴𝑈)
693, 8, 66, 12, 67, 68dchr1 25434 . . . . . . . . . . . . . . . . 17 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ( 1𝐴) = 1)
7065, 69sylan9eqr 2836 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓 = 1 ) → (𝑓𝐴) = 1)
7170fveq2d 6450 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓 = 1 ) → (∗‘(𝑓𝐴)) = (∗‘1))
72 1re 10376 . . . . . . . . . . . . . . . 16 1 ∈ ℝ
73 cjre 14286 . . . . . . . . . . . . . . . 16 (1 ∈ ℝ → (∗‘1) = 1)
7472, 73ax-mp 5 . . . . . . . . . . . . . . 15 (∗‘1) = 1
7571, 74syl6eq 2830 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓 = 1 ) → (∗‘(𝑓𝐴)) = 1)
7675oveq1d 6937 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓 = 1 ) → ((∗‘(𝑓𝐴)) · 1) = (1 · 1))
77 1t1e1 11544 . . . . . . . . . . . . 13 (1 · 1) = 1
7876, 77syl6eq 2830 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓 = 1 ) → ((∗‘(𝑓𝐴)) · 1) = 1)
7978ifeq1da 4337 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → if(𝑓 = 1 , ((∗‘(𝑓𝐴)) · 1), ((∗‘(𝑓𝐴)) · if(𝑓𝑊, -1, 0))) = if(𝑓 = 1 , 1, ((∗‘(𝑓𝐴)) · if(𝑓𝑊, -1, 0))))
80 df-ne 2970 . . . . . . . . . . . . 13 (𝑓1 ↔ ¬ 𝑓 = 1 )
81 ovif2 7015 . . . . . . . . . . . . . 14 ((∗‘(𝑓𝐴)) · if(𝑓𝑊, -1, 0)) = if(𝑓𝑊, ((∗‘(𝑓𝐴)) · -1), ((∗‘(𝑓𝐴)) · 0))
82 simplll 765 . . . . . . . . . . . . . . . . . . . . . 22 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) → 𝜑)
83 rpvmasum2.z1 . . . . . . . . . . . . . . . . . . . . . . 23 ((𝜑𝑓𝑊) → 𝐴 = (1r𝑍))
8483fveq2d 6450 . . . . . . . . . . . . . . . . . . . . . 22 ((𝜑𝑓𝑊) → (𝑓𝐴) = (𝑓‘(1r𝑍)))
8582, 84sylan 575 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) ∧ 𝑓𝑊) → (𝑓𝐴) = (𝑓‘(1r𝑍)))
863, 8, 4dchrmhm 25418 . . . . . . . . . . . . . . . . . . . . . . . 24 𝐷 ⊆ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld))
87 simpr 479 . . . . . . . . . . . . . . . . . . . . . . . 24 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → 𝑓𝐷)
8886, 87sseldi 3819 . . . . . . . . . . . . . . . . . . . . . . 23 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → 𝑓 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)))
89 eqid 2778 . . . . . . . . . . . . . . . . . . . . . . . . 25 (mulGrp‘𝑍) = (mulGrp‘𝑍)
90 eqid 2778 . . . . . . . . . . . . . . . . . . . . . . . . 25 (1r𝑍) = (1r𝑍)
9189, 90ringidval 18890 . . . . . . . . . . . . . . . . . . . . . . . 24 (1r𝑍) = (0g‘(mulGrp‘𝑍))
92 eqid 2778 . . . . . . . . . . . . . . . . . . . . . . . . 25 (mulGrp‘ℂfld) = (mulGrp‘ℂfld)
93 cnfld1 20167 . . . . . . . . . . . . . . . . . . . . . . . . 25 1 = (1r‘ℂfld)
9492, 93ringidval 18890 . . . . . . . . . . . . . . . . . . . . . . . 24 1 = (0g‘(mulGrp‘ℂfld))
9591, 94mhm0 17729 . . . . . . . . . . . . . . . . . . . . . . 23 (𝑓 ∈ ((mulGrp‘𝑍) MndHom (mulGrp‘ℂfld)) → (𝑓‘(1r𝑍)) = 1)
9688, 95syl 17 . . . . . . . . . . . . . . . . . . . . . 22 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → (𝑓‘(1r𝑍)) = 1)
9796ad2antrr 716 . . . . . . . . . . . . . . . . . . . . 21 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) ∧ 𝑓𝑊) → (𝑓‘(1r𝑍)) = 1)
9885, 97eqtrd 2814 . . . . . . . . . . . . . . . . . . . 20 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) ∧ 𝑓𝑊) → (𝑓𝐴) = 1)
9998fveq2d 6450 . . . . . . . . . . . . . . . . . . 19 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) ∧ 𝑓𝑊) → (∗‘(𝑓𝐴)) = (∗‘1))
10099, 74syl6eq 2830 . . . . . . . . . . . . . . . . . 18 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) ∧ 𝑓𝑊) → (∗‘(𝑓𝐴)) = 1)
101100oveq1d 6937 . . . . . . . . . . . . . . . . 17 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) ∧ 𝑓𝑊) → ((∗‘(𝑓𝐴)) · -1) = (1 · -1))
10251mulid2i 10382 . . . . . . . . . . . . . . . . 17 (1 · -1) = -1
103101, 102syl6eq 2830 . . . . . . . . . . . . . . . 16 (((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) ∧ 𝑓𝑊) → ((∗‘(𝑓𝐴)) · -1) = -1)
104103ifeq1da 4337 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) → if(𝑓𝑊, ((∗‘(𝑓𝐴)) · -1), ((∗‘(𝑓𝐴)) · 0)) = if(𝑓𝑊, -1, ((∗‘(𝑓𝐴)) · 0)))
10519adantr 474 . . . . . . . . . . . . . . . . 17 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) → (∗‘(𝑓𝐴)) ∈ ℂ)
106105mul01d 10575 . . . . . . . . . . . . . . . 16 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) → ((∗‘(𝑓𝐴)) · 0) = 0)
107106ifeq2d 4326 . . . . . . . . . . . . . . 15 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) → if(𝑓𝑊, -1, ((∗‘(𝑓𝐴)) · 0)) = if(𝑓𝑊, -1, 0))
108104, 107eqtrd 2814 . . . . . . . . . . . . . 14 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) → if(𝑓𝑊, ((∗‘(𝑓𝐴)) · -1), ((∗‘(𝑓𝐴)) · 0)) = if(𝑓𝑊, -1, 0))
10981, 108syl5eq 2826 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ 𝑓1 ) → ((∗‘(𝑓𝐴)) · if(𝑓𝑊, -1, 0)) = if(𝑓𝑊, -1, 0))
11080, 109sylan2br 588 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) ∧ ¬ 𝑓 = 1 ) → ((∗‘(𝑓𝐴)) · if(𝑓𝑊, -1, 0)) = if(𝑓𝑊, -1, 0))
111110ifeq2da 4338 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → if(𝑓 = 1 , 1, ((∗‘(𝑓𝐴)) · if(𝑓𝑊, -1, 0))) = if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))
11279, 111eqtrd 2814 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → if(𝑓 = 1 , ((∗‘(𝑓𝐴)) · 1), ((∗‘(𝑓𝐴)) · if(𝑓𝑊, -1, 0))) = if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))
11364, 112syl5eq 2826 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((∗‘(𝑓𝐴)) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))
114113oveq2d 6938 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((log‘𝑥) · ((∗‘(𝑓𝐴)) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))
11563, 114eqtrd 2814 . . . . . . 7 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((∗‘(𝑓𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))
11661, 115oveq12d 6940 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → (((∗‘(𝑓𝐴)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((∗‘(𝑓𝐴)) · ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))
11760, 116eqtrd 2814 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))
118117sumeq2dv 14841 . . . 4 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) = Σ𝑓𝐷𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))
119 fzfid 13091 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → (1...(⌊‘𝑥)) ∈ Fin)
120 inss1 4053 . . . . . . . . 9 ((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥))
121 ssfi 8468 . . . . . . . . 9 (((1...(⌊‘𝑥)) ∈ Fin ∧ ((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥))) → ((1...(⌊‘𝑥)) ∩ 𝑇) ∈ Fin)
122119, 120, 121sylancl 580 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → ((1...(⌊‘𝑥)) ∩ 𝑇) ∈ Fin)
1232phicld 15881 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → (ϕ‘𝑁) ∈ ℕ)
124123nncnd 11392 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → (ϕ‘𝑁) ∈ ℂ)
125120a1i 11 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → ((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥)))
126125sselda 3821 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → 𝑛 ∈ (1...(⌊‘𝑥)))
127126, 40syldan 585 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
128122, 124, 127fsummulc2 14920 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)))
129124adantr 474 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (ϕ‘𝑁) ∈ ℂ)
130129, 40mulcld 10397 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
131126, 130syldan 585 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)) → ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
132131ralrimiva 3148 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → ∀𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
133119olcd 863 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → ((1...(⌊‘𝑥)) ⊆ (ℤ‘1) ∨ (1...(⌊‘𝑥)) ∈ Fin))
134 sumss2 14864 . . . . . . . 8 (((((1...(⌊‘𝑥)) ∩ 𝑇) ⊆ (1...(⌊‘𝑥)) ∧ ∀𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ) ∧ ((1...(⌊‘𝑥)) ⊆ (ℤ‘1) ∨ (1...(⌊‘𝑥)) ∈ Fin)) → Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0))
135125, 132, 133, 134syl21anc 828 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0))
136 elin 4019 . . . . . . . . . . . . 13 (𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇) ↔ (𝑛 ∈ (1...(⌊‘𝑥)) ∧ 𝑛𝑇))
137136baib 531 . . . . . . . . . . . 12 (𝑛 ∈ (1...(⌊‘𝑥)) → (𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇) ↔ 𝑛𝑇))
138137adantl 475 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇) ↔ 𝑛𝑇))
139 rpvmasum2.t . . . . . . . . . . . . 13 𝑇 = (𝐿 “ {𝐴})
140139eleq2i 2851 . . . . . . . . . . . 12 (𝑛𝑇𝑛 ∈ (𝐿 “ {𝐴}))
14128ffnd 6292 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → 𝐿 Fn ℤ)
142 fniniseg 6602 . . . . . . . . . . . . . 14 (𝐿 Fn ℤ → (𝑛 ∈ (𝐿 “ {𝐴}) ↔ (𝑛 ∈ ℤ ∧ (𝐿𝑛) = 𝐴)))
143142baibd 535 . . . . . . . . . . . . 13 ((𝐿 Fn ℤ ∧ 𝑛 ∈ ℤ) → (𝑛 ∈ (𝐿 “ {𝐴}) ↔ (𝐿𝑛) = 𝐴))
144141, 29, 143syl2an 589 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 ∈ (𝐿 “ {𝐴}) ↔ (𝐿𝑛) = 𝐴))
145140, 144syl5bb 275 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛𝑇 ↔ (𝐿𝑛) = 𝐴))
146138, 145bitr2d 272 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝐿𝑛) = 𝐴𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)))
14740mul02d 10574 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (0 · ((Λ‘𝑛) / 𝑛)) = 0)
148146, 147ifbieq2d 4332 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → if((𝐿𝑛) = 𝐴, ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), (0 · ((Λ‘𝑛) / 𝑛))) = if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0))
149 ovif 7014 . . . . . . . . . 10 (if((𝐿𝑛) = 𝐴, (ϕ‘𝑁), 0) · ((Λ‘𝑛) / 𝑛)) = if((𝐿𝑛) = 𝐴, ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), (0 · ((Λ‘𝑛) / 𝑛)))
1501ad2antrr 716 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑁 ∈ ℕ)
151150, 5syl 17 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐷 ∈ Fin)
15219adantlr 705 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑓𝐷) → (∗‘(𝑓𝐴)) ∈ ℂ)
15333, 152mulcld 10397 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑓𝐷) → ((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) ∈ ℂ)
154151, 40, 153fsummulc1 14921 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑓𝐷 ((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑓𝐷 (((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) · ((Λ‘𝑛) / 𝑛)))
15514ad2antrr 716 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝐴𝑈)
1563, 4, 8, 9, 12, 150, 31, 155sum2dchr 25451 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑓𝐷 ((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) = if((𝐿𝑛) = 𝐴, (ϕ‘𝑁), 0))
157156oveq1d 6937 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑓𝐷 ((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) · ((Λ‘𝑛) / 𝑛)) = (if((𝐿𝑛) = 𝐴, (ϕ‘𝑁), 0) · ((Λ‘𝑛) / 𝑛)))
15840adantr 474 . . . . . . . . . . . . 13 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑓𝐷) → ((Λ‘𝑛) / 𝑛) ∈ ℂ)
159 mulass 10360 . . . . . . . . . . . . . 14 (((𝑓‘(𝐿𝑛)) ∈ ℂ ∧ (∗‘(𝑓𝐴)) ∈ ℂ ∧ ((Λ‘𝑛) / 𝑛) ∈ ℂ) → (((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) · ((Λ‘𝑛) / 𝑛)) = ((𝑓‘(𝐿𝑛)) · ((∗‘(𝑓𝐴)) · ((Λ‘𝑛) / 𝑛))))
160 mul12 10541 . . . . . . . . . . . . . 14 (((𝑓‘(𝐿𝑛)) ∈ ℂ ∧ (∗‘(𝑓𝐴)) ∈ ℂ ∧ ((Λ‘𝑛) / 𝑛) ∈ ℂ) → ((𝑓‘(𝐿𝑛)) · ((∗‘(𝑓𝐴)) · ((Λ‘𝑛) / 𝑛))) = ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
161159, 160eqtrd 2814 . . . . . . . . . . . . 13 (((𝑓‘(𝐿𝑛)) ∈ ℂ ∧ (∗‘(𝑓𝐴)) ∈ ℂ ∧ ((Λ‘𝑛) / 𝑛) ∈ ℂ) → (((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) · ((Λ‘𝑛) / 𝑛)) = ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
16233, 152, 158, 161syl3anc 1439 . . . . . . . . . . . 12 ((((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑓𝐷) → (((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) · ((Λ‘𝑛) / 𝑛)) = ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
163162sumeq2dv 14841 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑓𝐷 (((𝑓‘(𝐿𝑛)) · (∗‘(𝑓𝐴))) · ((Λ‘𝑛) / 𝑛)) = Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
164154, 157, 1633eqtr3d 2822 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (if((𝐿𝑛) = 𝐴, (ϕ‘𝑁), 0) · ((Λ‘𝑛) / 𝑛)) = Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
165149, 164syl5eqr 2828 . . . . . . . . 9 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → if((𝐿𝑛) = 𝐴, ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), (0 · ((Λ‘𝑛) / 𝑛))) = Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
166148, 165eqtr3d 2816 . . . . . . . 8 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0) = Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
167166sumeq2dv 14841 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))if(𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇), ((ϕ‘𝑁) · ((Λ‘𝑛) / 𝑛)), 0) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
168128, 135, 1673eqtrd 2818 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
169119, 6, 43fsumcom 14911 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) = Σ𝑓𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
170168, 169eqtrd 2814 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → ((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) = Σ𝑓𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))))
1713dchrabl 25431 . . . . . . . . . 10 (𝑁 ∈ ℕ → 𝐺 ∈ Abel)
172 ablgrp 18584 . . . . . . . . . 10 (𝐺 ∈ Abel → 𝐺 ∈ Grp)
1734, 66grpidcl 17837 . . . . . . . . . 10 (𝐺 ∈ Grp → 1𝐷)
1742, 171, 172, 1734syl 19 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → 1𝐷)
17548mulid1d 10394 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) · 1) = (log‘𝑥))
176175, 48eqeltrd 2859 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) · 1) ∈ ℂ)
177 iftrue 4313 . . . . . . . . . . 11 (𝑓 = 1 → if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)) = 1)
178177oveq2d 6938 . . . . . . . . . 10 (𝑓 = 1 → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = ((log‘𝑥) · 1))
179178sumsn 14882 . . . . . . . . 9 (( 1𝐷 ∧ ((log‘𝑥) · 1) ∈ ℂ) → Σ𝑓 ∈ { 1 } ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = ((log‘𝑥) · 1))
180174, 176, 179syl2anc 579 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓 ∈ { 1 } ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = ((log‘𝑥) · 1))
181 eldifsn 4550 . . . . . . . . . . 11 (𝑓 ∈ (𝐷 ∖ { 1 }) ↔ (𝑓𝐷𝑓1 ))
182 ifnefalse 4319 . . . . . . . . . . . . . . 15 (𝑓1 → if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)) = if(𝑓𝑊, -1, 0))
183182ad2antll 719 . . . . . . . . . . . . . 14 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑓𝐷𝑓1 )) → if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)) = if(𝑓𝑊, -1, 0))
184 negeq 10614 . . . . . . . . . . . . . . 15 (if(𝑓𝑊, 1, 0) = 1 → -if(𝑓𝑊, 1, 0) = -1)
185 negeq 10614 . . . . . . . . . . . . . . . 16 (if(𝑓𝑊, 1, 0) = 0 → -if(𝑓𝑊, 1, 0) = -0)
186 neg0 10669 . . . . . . . . . . . . . . . 16 -0 = 0
187185, 186syl6eq 2830 . . . . . . . . . . . . . . 15 (if(𝑓𝑊, 1, 0) = 0 → -if(𝑓𝑊, 1, 0) = 0)
188184, 187ifsb 4320 . . . . . . . . . . . . . 14 -if(𝑓𝑊, 1, 0) = if(𝑓𝑊, -1, 0)
189183, 188syl6eqr 2832 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑓𝐷𝑓1 )) → if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)) = -if(𝑓𝑊, 1, 0))
190189oveq2d 6938 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑓𝐷𝑓1 )) → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = ((log‘𝑥) · -if(𝑓𝑊, 1, 0)))
19148adantr 474 . . . . . . . . . . . . 13 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑓𝐷𝑓1 )) → (log‘𝑥) ∈ ℂ)
19250, 52ifcli 4353 . . . . . . . . . . . . 13 if(𝑓𝑊, 1, 0) ∈ ℂ
193 mulneg2 10812 . . . . . . . . . . . . 13 (((log‘𝑥) ∈ ℂ ∧ if(𝑓𝑊, 1, 0) ∈ ℂ) → ((log‘𝑥) · -if(𝑓𝑊, 1, 0)) = -((log‘𝑥) · if(𝑓𝑊, 1, 0)))
194191, 192, 193sylancl 580 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑓𝐷𝑓1 )) → ((log‘𝑥) · -if(𝑓𝑊, 1, 0)) = -((log‘𝑥) · if(𝑓𝑊, 1, 0)))
195190, 194eqtrd 2814 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ (𝑓𝐷𝑓1 )) → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = -((log‘𝑥) · if(𝑓𝑊, 1, 0)))
196181, 195sylan2b 587 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = -((log‘𝑥) · if(𝑓𝑊, 1, 0)))
197196sumeq2dv 14841 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = Σ𝑓 ∈ (𝐷 ∖ { 1 })-((log‘𝑥) · if(𝑓𝑊, 1, 0)))
198 diffi 8480 . . . . . . . . . . 11 (𝐷 ∈ Fin → (𝐷 ∖ { 1 }) ∈ Fin)
1996, 198syl 17 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → (𝐷 ∖ { 1 }) ∈ Fin)
20048adantr 474 . . . . . . . . . . 11 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) → (log‘𝑥) ∈ ℂ)
201 mulcl 10356 . . . . . . . . . . 11 (((log‘𝑥) ∈ ℂ ∧ if(𝑓𝑊, 1, 0) ∈ ℂ) → ((log‘𝑥) · if(𝑓𝑊, 1, 0)) ∈ ℂ)
202200, 192, 201sylancl 580 . . . . . . . . . 10 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) → ((log‘𝑥) · if(𝑓𝑊, 1, 0)) ∈ ℂ)
203199, 202fsumneg 14923 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓 ∈ (𝐷 ∖ { 1 })-((log‘𝑥) · if(𝑓𝑊, 1, 0)) = -Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓𝑊, 1, 0)))
204192a1i 11 . . . . . . . . . . . 12 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓 ∈ (𝐷 ∖ { 1 })) → if(𝑓𝑊, 1, 0) ∈ ℂ)
205199, 48, 204fsummulc2 14920 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) · Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓𝑊, 1, 0)) = Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓𝑊, 1, 0)))
206 rpvmasum2.w . . . . . . . . . . . . . . . . 17 𝑊 = {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿𝑚)) / 𝑚) = 0}
207 ssrab2 3908 . . . . . . . . . . . . . . . . 17 {𝑦 ∈ (𝐷 ∖ { 1 }) ∣ Σ𝑚 ∈ ℕ ((𝑦‘(𝐿𝑚)) / 𝑚) = 0} ⊆ (𝐷 ∖ { 1 })
208206, 207eqsstri 3854 . . . . . . . . . . . . . . . 16 𝑊 ⊆ (𝐷 ∖ { 1 })
209 difss 3960 . . . . . . . . . . . . . . . 16 (𝐷 ∖ { 1 }) ⊆ 𝐷
210208, 209sstri 3830 . . . . . . . . . . . . . . 15 𝑊𝐷
211 ssfi 8468 . . . . . . . . . . . . . . 15 ((𝐷 ∈ Fin ∧ 𝑊𝐷) → 𝑊 ∈ Fin)
2126, 210, 211sylancl 580 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → 𝑊 ∈ Fin)
213 fsumconst 14926 . . . . . . . . . . . . . 14 ((𝑊 ∈ Fin ∧ 1 ∈ ℂ) → Σ𝑓𝑊 1 = ((♯‘𝑊) · 1))
214212, 50, 213sylancl 580 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓𝑊 1 = ((♯‘𝑊) · 1))
215208a1i 11 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → 𝑊 ⊆ (𝐷 ∖ { 1 }))
21650a1i 11 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → 1 ∈ ℂ)
217216ralrimivw 3149 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → ∀𝑓𝑊 1 ∈ ℂ)
218199olcd 863 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → ((𝐷 ∖ { 1 }) ⊆ (ℤ‘1) ∨ (𝐷 ∖ { 1 }) ∈ Fin))
219 sumss2 14864 . . . . . . . . . . . . . 14 (((𝑊 ⊆ (𝐷 ∖ { 1 }) ∧ ∀𝑓𝑊 1 ∈ ℂ) ∧ ((𝐷 ∖ { 1 }) ⊆ (ℤ‘1) ∨ (𝐷 ∖ { 1 }) ∈ Fin)) → Σ𝑓𝑊 1 = Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓𝑊, 1, 0))
220215, 217, 218, 219syl21anc 828 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓𝑊 1 = Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓𝑊, 1, 0))
221 hashcl 13462 . . . . . . . . . . . . . . . 16 (𝑊 ∈ Fin → (♯‘𝑊) ∈ ℕ0)
222212, 221syl 17 . . . . . . . . . . . . . . 15 ((𝜑𝑥 ∈ ℝ+) → (♯‘𝑊) ∈ ℕ0)
223222nn0cnd 11704 . . . . . . . . . . . . . 14 ((𝜑𝑥 ∈ ℝ+) → (♯‘𝑊) ∈ ℂ)
224223mulid1d 10394 . . . . . . . . . . . . 13 ((𝜑𝑥 ∈ ℝ+) → ((♯‘𝑊) · 1) = (♯‘𝑊))
225214, 220, 2243eqtr3d 2822 . . . . . . . . . . . 12 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓𝑊, 1, 0) = (♯‘𝑊))
226225oveq2d 6938 . . . . . . . . . . 11 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) · Σ𝑓 ∈ (𝐷 ∖ { 1 })if(𝑓𝑊, 1, 0)) = ((log‘𝑥) · (♯‘𝑊)))
227205, 226eqtr3d 2816 . . . . . . . . . 10 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓𝑊, 1, 0)) = ((log‘𝑥) · (♯‘𝑊)))
228227negeqd 10616 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → -Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓𝑊, 1, 0)) = -((log‘𝑥) · (♯‘𝑊)))
229197, 203, 2283eqtrd 2818 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = -((log‘𝑥) · (♯‘𝑊)))
230180, 229oveq12d 6940 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → (Σ𝑓 ∈ { 1 } ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) + Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (((log‘𝑥) · 1) + -((log‘𝑥) · (♯‘𝑊))))
23148, 223mulcld 10397 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) · (♯‘𝑊)) ∈ ℂ)
232176, 231negsubd 10740 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → (((log‘𝑥) · 1) + -((log‘𝑥) · (♯‘𝑊))) = (((log‘𝑥) · 1) − ((log‘𝑥) · (♯‘𝑊))))
233230, 232eqtrd 2814 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → (Σ𝑓 ∈ { 1 } ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) + Σ𝑓 ∈ (𝐷 ∖ { 1 })((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (((log‘𝑥) · 1) − ((log‘𝑥) · (♯‘𝑊))))
234 disjdif 4264 . . . . . . . 8 ({ 1 } ∩ (𝐷 ∖ { 1 })) = ∅
235234a1i 11 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → ({ 1 } ∩ (𝐷 ∖ { 1 })) = ∅)
236 undif2 4268 . . . . . . . 8 ({ 1 } ∪ (𝐷 ∖ { 1 })) = ({ 1 } ∪ 𝐷)
237174snssd 4571 . . . . . . . . 9 ((𝜑𝑥 ∈ ℝ+) → { 1 } ⊆ 𝐷)
238 ssequn1 4006 . . . . . . . . 9 ({ 1 } ⊆ 𝐷 ↔ ({ 1 } ∪ 𝐷) = 𝐷)
239237, 238sylib 210 . . . . . . . 8 ((𝜑𝑥 ∈ ℝ+) → ({ 1 } ∪ 𝐷) = 𝐷)
240236, 239syl5req 2827 . . . . . . 7 ((𝜑𝑥 ∈ ℝ+) → 𝐷 = ({ 1 } ∪ (𝐷 ∖ { 1 })))
241235, 240, 6, 56fsumsplit 14878 . . . . . 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 10831 . . . . . 6 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) · (1 − (♯‘𝑊))) = (((log‘𝑥) · 1) − ((log‘𝑥) · (♯‘𝑊))))
243233, 241, 2423eqtr4rd 2825 . . . . 5 ((𝜑𝑥 ∈ ℝ+) → ((log‘𝑥) · (1 − (♯‘𝑊))) = Σ𝑓𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))
244170, 243oveq12d 6940 . . . 4 ((𝜑𝑥 ∈ ℝ+) → (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊)))) = (Σ𝑓𝐷 Σ𝑛 ∈ (1...(⌊‘𝑥))((∗‘(𝑓𝐴)) · ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛))) − Σ𝑓𝐷 ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))
24557, 118, 2443eqtr4d 2824 . . 3 ((𝜑𝑥 ∈ ℝ+) → Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) = (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊)))))
246245mpteq2dva 4979 . 2 (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))) = (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))))
247 rpssre 12144 . . . 4 + ⊆ ℝ
248247a1i 11 . . 3 (𝜑 → ℝ+ ⊆ ℝ)
2491, 5syl 17 . . 3 (𝜑𝐷 ∈ Fin)
25017adantlr 705 . . . . . 6 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → (𝑓𝐴) ∈ ℂ)
251250cjcld 14343 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → (∗‘(𝑓𝐴)) ∈ ℂ)
25259, 56subcld 10734 . . . . 5 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) ∈ ℂ)
253251, 252mulcld 10397 . . . 4 (((𝜑𝑥 ∈ ℝ+) ∧ 𝑓𝐷) → ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) ∈ ℂ)
254253anasss 460 . . 3 ((𝜑 ∧ (𝑥 ∈ ℝ+𝑓𝐷)) → ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) ∈ ℂ)
25518adantr 474 . . . 4 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → (∗‘(𝑓𝐴)) ∈ ℂ)
256252an32s 642 . . . 4 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) ∈ ℂ)
257 o1const 14758 . . . . 5 ((ℝ+ ⊆ ℝ ∧ (∗‘(𝑓𝐴)) ∈ ℂ) → (𝑥 ∈ ℝ+ ↦ (∗‘(𝑓𝐴))) ∈ 𝑂(1))
258247, 18, 257sylancr 581 . . . 4 ((𝜑𝑓𝐷) → (𝑥 ∈ ℝ+ ↦ (∗‘(𝑓𝐴))) ∈ 𝑂(1))
259 fveq1 6445 . . . . . . . . . . . 12 (𝑓 = 1 → (𝑓‘(𝐿𝑛)) = ( 1 ‘(𝐿𝑛)))
260259oveq1d 6937 . . . . . . . . . . 11 (𝑓 = 1 → ((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) = (( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)))
261260sumeq2sdv 14842 . . . . . . . . . 10 (𝑓 = 1 → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)))
262261, 178oveq12d 6940 . . . . . . . . 9 (𝑓 = 1 → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · 1)))
263262adantl 475 . . . . . . . 8 (((𝜑𝑓𝐷) ∧ 𝑓 = 1 ) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · 1)))
26446recnd 10405 . . . . . . . . . 10 (𝑥 ∈ ℝ+ → (log‘𝑥) ∈ ℂ)
265264mulid1d 10394 . . . . . . . . 9 (𝑥 ∈ ℝ+ → ((log‘𝑥) · 1) = (log‘𝑥))
266265oveq2d 6938 . . . . . . . 8 (𝑥 ∈ ℝ+ → (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · 1)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))
267263, 266sylan9eq 2834 . . . . . . 7 ((((𝜑𝑓𝐷) ∧ 𝑓 = 1 ) ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥)))
268267mpteq2dva 4979 . . . . . 6 (((𝜑𝑓𝐷) ∧ 𝑓 = 1 ) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))))
2698, 24, 1, 3, 4, 66rpvmasumlem 25628 . . . . . . 7 (𝜑 → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1))
270269ad2antrr 716 . . . . . 6 (((𝜑𝑓𝐷) ∧ 𝑓 = 1 ) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))(( 1 ‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − (log‘𝑥))) ∈ 𝑂(1))
271268, 270eqeltrd 2859 . . . . 5 (((𝜑𝑓𝐷) ∧ 𝑓 = 1 ) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) ∈ 𝑂(1))
272182oveq2d 6938 . . . . . . . . . 10 (𝑓1 → ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))) = ((log‘𝑥) · if(𝑓𝑊, -1, 0)))
273272oveq2d 6938 . . . . . . . . 9 (𝑓1 → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓𝑊, -1, 0))))
27448adantlr 705 . . . . . . . . . . . . . . 15 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → (log‘𝑥) ∈ ℂ)
275 mulcom 10358 . . . . . . . . . . . . . . 15 (((log‘𝑥) ∈ ℂ ∧ -1 ∈ ℂ) → ((log‘𝑥) · -1) = (-1 · (log‘𝑥)))
276274, 51, 275sylancl 580 . . . . . . . . . . . . . 14 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥) · -1) = (-1 · (log‘𝑥)))
277274mulm1d 10827 . . . . . . . . . . . . . 14 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → (-1 · (log‘𝑥)) = -(log‘𝑥))
278276, 277eqtrd 2814 . . . . . . . . . . . . 13 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥) · -1) = -(log‘𝑥))
279274mul01d 10575 . . . . . . . . . . . . 13 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥) · 0) = 0)
280278, 279ifeq12d 4327 . . . . . . . . . . . 12 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → if(𝑓𝑊, ((log‘𝑥) · -1), ((log‘𝑥) · 0)) = if(𝑓𝑊, -(log‘𝑥), 0))
281 ovif2 7015 . . . . . . . . . . . 12 ((log‘𝑥) · if(𝑓𝑊, -1, 0)) = if(𝑓𝑊, ((log‘𝑥) · -1), ((log‘𝑥) · 0))
282 negeq 10614 . . . . . . . . . . . . 13 (if(𝑓𝑊, (log‘𝑥), 0) = (log‘𝑥) → -if(𝑓𝑊, (log‘𝑥), 0) = -(log‘𝑥))
283 negeq 10614 . . . . . . . . . . . . . 14 (if(𝑓𝑊, (log‘𝑥), 0) = 0 → -if(𝑓𝑊, (log‘𝑥), 0) = -0)
284283, 186syl6eq 2830 . . . . . . . . . . . . 13 (if(𝑓𝑊, (log‘𝑥), 0) = 0 → -if(𝑓𝑊, (log‘𝑥), 0) = 0)
285282, 284ifsb 4320 . . . . . . . . . . . 12 -if(𝑓𝑊, (log‘𝑥), 0) = if(𝑓𝑊, -(log‘𝑥), 0)
286280, 281, 2853eqtr4g 2839 . . . . . . . . . . 11 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → ((log‘𝑥) · if(𝑓𝑊, -1, 0)) = -if(𝑓𝑊, (log‘𝑥), 0))
287286oveq2d 6938 . . . . . . . . . 10 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓𝑊, -1, 0))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − -if(𝑓𝑊, (log‘𝑥), 0)))
28859an32s 642 . . . . . . . . . . 11 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) ∈ ℂ)
289 ifcl 4351 . . . . . . . . . . . 12 (((log‘𝑥) ∈ ℂ ∧ 0 ∈ ℂ) → if(𝑓𝑊, (log‘𝑥), 0) ∈ ℂ)
290274, 52, 289sylancl 580 . . . . . . . . . . 11 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → if(𝑓𝑊, (log‘𝑥), 0) ∈ ℂ)
291288, 290subnegd 10741 . . . . . . . . . 10 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − -if(𝑓𝑊, (log‘𝑥), 0)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0)))
292287, 291eqtrd 2814 . . . . . . . . 9 (((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓𝑊, -1, 0))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0)))
293273, 292sylan9eqr 2836 . . . . . . . 8 ((((𝜑𝑓𝐷) ∧ 𝑥 ∈ ℝ+) ∧ 𝑓1 ) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0)))
294293an32s 642 . . . . . . 7 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ 𝑥 ∈ ℝ+) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0)))
295294mpteq2dva 4979 . . . . . 6 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) = (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0))))
2961ad2antrr 716 . . . . . . . 8 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → 𝑁 ∈ ℕ)
297 simplr 759 . . . . . . . 8 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → 𝑓𝐷)
298 simpr 479 . . . . . . . 8 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → 𝑓1 )
299 eqid 2778 . . . . . . . 8 (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)) = (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))
3008, 24, 296, 3, 4, 66, 297, 298, 299dchrmusumlema 25634 . . . . . . 7 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → ∃𝑡𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))
3011adantr 474 . . . . . . . . . . . . 13 ((𝜑𝑓𝐷) → 𝑁 ∈ ℕ)
302301ad2antrr 716 . . . . . . . . . . . 12 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑁 ∈ ℕ)
303297adantr 474 . . . . . . . . . . . 12 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑓𝐷)
304 simplr 759 . . . . . . . . . . . 12 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑓1 )
305 simprl 761 . . . . . . . . . . . 12 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → 𝑐 ∈ (0[,)+∞))
306 simprrl 771 . . . . . . . . . . . 12 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡)
307 simprrr 772 . . . . . . . . . . . 12 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦))
3088, 24, 302, 3, 4, 66, 303, 304, 299, 305, 306, 307, 206dchrvmaeq0 25645 . . . . . . . . . . 11 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑓𝑊𝑡 = 0))
309 ifbi 4328 . . . . . . . . . . . . 13 ((𝑓𝑊𝑡 = 0) → if(𝑓𝑊, (log‘𝑥), 0) = if(𝑡 = 0, (log‘𝑥), 0))
310309oveq2d 6938 . . . . . . . . . . . 12 ((𝑓𝑊𝑡 = 0) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑡 = 0, (log‘𝑥), 0)))
311310mpteq2dv 4980 . . . . . . . . . . 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 25644 . . . . . . . . . 10 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑡 = 0, (log‘𝑥), 0))) ∈ 𝑂(1))
314312, 313eqeltrd 2859 . . . . . . . . 9 ((((𝜑𝑓𝐷) ∧ 𝑓1 ) ∧ (𝑐 ∈ (0[,)+∞) ∧ (seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)))) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0))) ∈ 𝑂(1))
315314rexlimdvaa 3214 . . . . . . . 8 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → (∃𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0))) ∈ 𝑂(1)))
316315exlimdv 1976 . . . . . . 7 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → (∃𝑡𝑐 ∈ (0[,)+∞)(seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎))) ⇝ 𝑡 ∧ ∀𝑦 ∈ (1[,)+∞)(abs‘((seq1( + , (𝑎 ∈ ℕ ↦ ((𝑓‘(𝐿𝑎)) / 𝑎)))‘(⌊‘𝑦)) − 𝑡)) ≤ (𝑐 / 𝑦)) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0))) ∈ 𝑂(1)))
317300, 316mpd 15 . . . . . 6 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) + if(𝑓𝑊, (log‘𝑥), 0))) ∈ 𝑂(1))
318295, 317eqeltrd 2859 . . . . 5 (((𝜑𝑓𝐷) ∧ 𝑓1 ) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) ∈ 𝑂(1))
319271, 318pm2.61dane 3057 . . . 4 ((𝜑𝑓𝐷) → (𝑥 ∈ ℝ+ ↦ (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0))))) ∈ 𝑂(1))
320255, 256, 258, 319o1mul2 14763 . . 3 ((𝜑𝑓𝐷) → (𝑥 ∈ ℝ+ ↦ ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))) ∈ 𝑂(1))
321248, 249, 254, 320fsumo1 14948 . 2 (𝜑 → (𝑥 ∈ ℝ+ ↦ Σ𝑓𝐷 ((∗‘(𝑓𝐴)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑓‘(𝐿𝑛)) · ((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · if(𝑓 = 1 , 1, if(𝑓𝑊, -1, 0)))))) ∈ 𝑂(1))
322246, 321eqeltrrd 2860 1 (𝜑 → (𝑥 ∈ ℝ+ ↦ (((ϕ‘𝑁) · Σ𝑛 ∈ ((1...(⌊‘𝑥)) ∩ 𝑇)((Λ‘𝑛) / 𝑛)) − ((log‘𝑥) · (1 − (♯‘𝑊))))) ∈ 𝑂(1))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 198  wa 386  wo 836  w3a 1071   = wceq 1601  wex 1823  wcel 2107  wne 2969  wral 3090  wrex 3091  {crab 3094  cdif 3789  cun 3790  cin 3791  wss 3792  c0 4141  ifcif 4307  {csn 4398   class class class wbr 4886  cmpt 4965  ccnv 5354  cima 5358   Fn wfn 6130  wf 6131  ontowfo 6133  cfv 6135  (class class class)co 6922  Fincfn 8241  cc 10270  cr 10271  0cc0 10272  1c1 10273   + caddc 10275   · cmul 10277  +∞cpnf 10408  cle 10412  cmin 10606  -cneg 10607   / cdiv 11032  cn 11374  0cn0 11642  cz 11728  cuz 11992  +crp 12137  [,)cico 12489  ...cfz 12643  cfl 12910  seqcseq 13119  chash 13435  ccj 14243  abscabs 14381  cli 14623  𝑂(1)co1 14625  Σcsu 14824  ϕcphi 15873  Basecbs 16255  0gc0g 16486   MndHom cmhm 17719  Grpcgrp 17809  Abelcabl 18580  mulGrpcmgp 18876  1rcur 18888  Unitcui 19026  fldccnfld 20142  ℤRHomczrh 20244  ℤ/nczn 20247  logclog 24738  Λcvma 25270  DChrcdchr 25409
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1839  ax-4 1853  ax-5 1953  ax-6 2021  ax-7 2055  ax-8 2109  ax-9 2116  ax-10 2135  ax-11 2150  ax-12 2163  ax-13 2334  ax-ext 2754  ax-rep 5006  ax-sep 5017  ax-nul 5025  ax-pow 5077  ax-pr 5138  ax-un 7226  ax-inf2 8835  ax-cnex 10328  ax-resscn 10329  ax-1cn 10330  ax-icn 10331  ax-addcl 10332  ax-addrcl 10333  ax-mulcl 10334  ax-mulrcl 10335  ax-mulcom 10336  ax-addass 10337  ax-mulass 10338  ax-distr 10339  ax-i2m1 10340  ax-1ne0 10341  ax-1rid 10342  ax-rnegex 10343  ax-rrecex 10344  ax-cnre 10345  ax-pre-lttri 10346  ax-pre-lttrn 10347  ax-pre-ltadd 10348  ax-pre-mulgt0 10349  ax-pre-sup 10350  ax-addf 10351  ax-mulf 10352
This theorem depends on definitions:  df-bi 199  df-an 387  df-or 837  df-3or 1072  df-3an 1073  df-tru 1605  df-fal 1615  df-ex 1824  df-nf 1828  df-sb 2012  df-mo 2551  df-eu 2587  df-clab 2764  df-cleq 2770  df-clel 2774  df-nfc 2921  df-ne 2970  df-nel 3076  df-ral 3095  df-rex 3096  df-reu 3097  df-rmo 3098  df-rab 3099  df-v 3400  df-sbc 3653  df-csb 3752  df-dif 3795  df-un 3797  df-in 3799  df-ss 3806  df-pss 3808  df-nul 4142  df-if 4308  df-pw 4381  df-sn 4399  df-pr 4401  df-tp 4403  df-op 4405  df-uni 4672  df-int 4711  df-iun 4755  df-iin 4756  df-disj 4855  df-br 4887  df-opab 4949  df-mpt 4966  df-tr 4988  df-id 5261  df-eprel 5266  df-po 5274  df-so 5275  df-fr 5314  df-se 5315  df-we 5316  df-xp 5361  df-rel 5362  df-cnv 5363  df-co 5364  df-dm 5365  df-rn 5366  df-res 5367  df-ima 5368  df-pred 5933  df-ord 5979  df-on 5980  df-lim 5981  df-suc 5982  df-iota 6099  df-fun 6137  df-fn 6138  df-f 6139  df-f1 6140  df-fo 6141  df-f1o 6142  df-fv 6143  df-isom 6144  df-riota 6883  df-ov 6925  df-oprab 6926  df-mpt2 6927  df-of 7174  df-rpss 7214  df-om 7344  df-1st 7445  df-2nd 7446  df-supp 7577  df-tpos 7634  df-wrecs 7689  df-recs 7751  df-rdg 7789  df-1o 7843  df-2o 7844  df-oadd 7847  df-omul 7848  df-er 8026  df-ec 8028  df-qs 8032  df-map 8142  df-pm 8143  df-ixp 8195  df-en 8242  df-dom 8243  df-sdom 8244  df-fin 8245  df-fsupp 8564  df-fi 8605  df-sup 8636  df-inf 8637  df-oi 8704  df-card 9098  df-acn 9101  df-cda 9325  df-pnf 10413  df-mnf 10414  df-xr 10415  df-ltxr 10416  df-le 10417  df-sub 10608  df-neg 10609  df-div 11033  df-nn 11375  df-2 11438  df-3 11439  df-4 11440  df-5 11441  df-6 11442  df-7 11443  df-8 11444  df-9 11445  df-n0 11643  df-xnn0 11715  df-z 11729  df-dec 11846  df-uz 11993  df-q 12096  df-rp 12138  df-xneg 12257  df-xadd 12258  df-xmul 12259  df-ioo 12491  df-ioc 12492  df-ico 12493  df-icc 12494  df-fz 12644  df-fzo 12785  df-fl 12912  df-mod 12988  df-seq 13120  df-exp 13179  df-fac 13379  df-bc 13408  df-hash 13436  df-word 13600  df-concat 13661  df-s1 13686  df-shft 14214  df-cj 14246  df-re 14247  df-im 14248  df-sqrt 14382  df-abs 14383  df-limsup 14610  df-clim 14627  df-rlim 14628  df-o1 14629  df-lo1 14630  df-sum 14825  df-ef 15200  df-e 15201  df-sin 15202  df-cos 15203  df-pi 15205  df-dvds 15388  df-gcd 15623  df-prm 15791  df-phi 15875  df-pc 15946  df-struct 16257  df-ndx 16258  df-slot 16259  df-base 16261  df-sets 16262  df-ress 16263  df-plusg 16351  df-mulr 16352  df-starv 16353  df-sca 16354  df-vsca 16355  df-ip 16356  df-tset 16357  df-ple 16358  df-ds 16360  df-unif 16361  df-hom 16362  df-cco 16363  df-rest 16469  df-topn 16470  df-0g 16488  df-gsum 16489  df-topgen 16490  df-pt 16491  df-prds 16494  df-xrs 16548  df-qtop 16553  df-imas 16554  df-qus 16555  df-xps 16556  df-mre 16632  df-mrc 16633  df-acs 16635  df-mgm 17628  df-sgrp 17670  df-mnd 17681  df-mhm 17721  df-submnd 17722  df-grp 17812  df-minusg 17813  df-sbg 17814  df-mulg 17928  df-subg 17975  df-nsg 17976  df-eqg 17977  df-ghm 18042  df-gim 18085  df-ga 18106  df-cntz 18133  df-oppg 18159  df-od 18332  df-gex 18333  df-pgp 18334  df-lsm 18435  df-pj1 18436  df-cmn 18581  df-abl 18582  df-cyg 18666  df-dprd 18781  df-dpj 18782  df-mgp 18877  df-ur 18889  df-ring 18936  df-cring 18937  df-oppr 19010  df-dvdsr 19028  df-unit 19029  df-invr 19059  df-dvr 19070  df-rnghom 19104  df-drng 19141  df-subrg 19170  df-lmod 19257  df-lss 19325  df-lsp 19367  df-sra 19569  df-rgmod 19570  df-lidl 19571  df-rsp 19572  df-2idl 19629  df-psmet 20134  df-xmet 20135  df-met 20136  df-bl 20137  df-mopn 20138  df-fbas 20139  df-fg 20140  df-cnfld 20143  df-zring 20215  df-zrh 20248  df-zn 20251  df-top 21106  df-topon 21123  df-topsp 21145  df-bases 21158  df-cld 21231  df-ntr 21232  df-cls 21233  df-nei 21310  df-lp 21348  df-perf 21349  df-cn 21439  df-cnp 21440  df-haus 21527  df-cmp 21599  df-tx 21774  df-hmeo 21967  df-fil 22058  df-fm 22150  df-flim 22151  df-flf 22152  df-xms 22533  df-ms 22534  df-tms 22535  df-cncf 23089  df-0p 23874  df-limc 24067  df-dv 24068  df-ply 24381  df-idp 24382  df-coe 24383  df-dgr 24384  df-quot 24483  df-log 24740  df-cxp 24741  df-em 25171  df-cht 25275  df-vma 25276  df-chp 25277  df-ppi 25278  df-mu 25279  df-dchr 25410
This theorem is referenced by:  dchrisum0re  25654  rpvmasum  25667
  Copyright terms: Public domain W3C validator