Metamath Proof Explorer


Theorem rpvmasum2

Description: A partial result along the lines of rpvmasum . The sum of the von Mangoldt function over those integers n == A (mod N ) is asymptotic to ( 1 - M ) ( log x / phi ( x ) ) + O(1) , where M is the number of non-principal Dirichlet characters with sum_ n e. NN , X ( n ) / n = 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)

Ref Expression
Hypotheses 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 rpvmasum2 ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) ∈ 𝑂(1) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ( 𝜑𝑁 ∈ ℕ )
4 rpvmasum2.g 𝐺 = ( DChr ‘ 𝑁 )
5 rpvmasum2.d 𝐷 = ( Base ‘ 𝐺 )
6 rpvmasum2.1 1 = ( 0g𝐺 )
7 rpvmasum2.w 𝑊 = { 𝑦 ∈ ( 𝐷 ∖ { 1 } ) ∣ Σ 𝑚 ∈ ℕ ( ( 𝑦 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) = 0 }
8 rpvmasum2.u 𝑈 = ( Unit ‘ 𝑍 )
9 rpvmasum2.b ( 𝜑𝐴𝑈 )
10 rpvmasum2.t 𝑇 = ( 𝐿 “ { 𝐴 } )
11 rpvmasum2.z1 ( ( 𝜑𝑓𝑊 ) → 𝐴 = ( 1r𝑍 ) )
12 3 adantr ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝑁 ∈ ℕ )
13 4 5 dchrfi ( 𝑁 ∈ ℕ → 𝐷 ∈ Fin )
14 12 13 syl ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝐷 ∈ Fin )
15 fzfid ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
16 eqid ( Base ‘ 𝑍 ) = ( Base ‘ 𝑍 )
17 simpr ( ( 𝜑𝑓𝐷 ) → 𝑓𝐷 )
18 4 1 5 16 17 dchrf ( ( 𝜑𝑓𝐷 ) → 𝑓 : ( Base ‘ 𝑍 ) ⟶ ℂ )
19 16 8 unitss 𝑈 ⊆ ( Base ‘ 𝑍 )
20 19 9 sselid ( 𝜑𝐴 ∈ ( Base ‘ 𝑍 ) )
21 20 adantr ( ( 𝜑𝑓𝐷 ) → 𝐴 ∈ ( Base ‘ 𝑍 ) )
22 18 21 ffvelrnd ( ( 𝜑𝑓𝐷 ) → ( 𝑓𝐴 ) ∈ ℂ )
23 22 cjcld ( ( 𝜑𝑓𝐷 ) → ( ∗ ‘ ( 𝑓𝐴 ) ) ∈ ℂ )
24 23 adantlr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( ∗ ‘ ( 𝑓𝐴 ) ) ∈ ℂ )
25 24 adantrl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑓𝐷 ) ) → ( ∗ ‘ ( 𝑓𝐴 ) ) ∈ ℂ )
26 18 ad4ant14 ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑓𝐷 ) → 𝑓 : ( Base ‘ 𝑍 ) ⟶ ℂ )
27 3 nnnn0d ( 𝜑𝑁 ∈ ℕ0 )
28 1 16 2 znzrhfo ( 𝑁 ∈ ℕ0𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) )
29 fof ( 𝐿 : ℤ –onto→ ( Base ‘ 𝑍 ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
30 27 28 29 3syl ( 𝜑𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
31 30 adantr ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) )
32 elfzelz ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℤ )
33 ffvelrn ( ( 𝐿 : ℤ ⟶ ( Base ‘ 𝑍 ) ∧ 𝑛 ∈ ℤ ) → ( 𝐿𝑛 ) ∈ ( Base ‘ 𝑍 ) )
34 31 32 33 syl2an ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐿𝑛 ) ∈ ( Base ‘ 𝑍 ) )
35 34 adantr ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑓𝐷 ) → ( 𝐿𝑛 ) ∈ ( Base ‘ 𝑍 ) )
36 26 35 ffvelrnd ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑓𝐷 ) → ( 𝑓 ‘ ( 𝐿𝑛 ) ) ∈ ℂ )
37 36 anasss ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑓𝐷 ) ) → ( 𝑓 ‘ ( 𝐿𝑛 ) ) ∈ ℂ )
38 elfznn ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
39 38 adantl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
40 vmacl ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
41 39 40 syl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
42 41 39 nndivred ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
43 42 recnd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
44 43 adantrr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑓𝐷 ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
45 37 44 mulcld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑓𝐷 ) ) → ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
46 25 45 mulcld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑓𝐷 ) ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ ℂ )
47 46 anass1rs ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ ℂ )
48 15 47 fsumcl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) ∈ ℂ )
49 relogcl ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
50 49 adantl ( ( 𝜑𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
51 50 recnd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
52 51 adantr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( log ‘ 𝑥 ) ∈ ℂ )
53 ax-1cn 1 ∈ ℂ
54 neg1cn - 1 ∈ ℂ
55 0cn 0 ∈ ℂ
56 54 55 ifcli if ( 𝑓𝑊 , - 1 , 0 ) ∈ ℂ
57 53 56 ifcli if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ∈ ℂ
58 mulcl ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ∈ ℂ ) → ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ∈ ℂ )
59 52 57 58 sylancl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ∈ ℂ )
60 14 48 59 fsumsub ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑓𝐷 ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) = ( Σ 𝑓𝐷 Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − Σ 𝑓𝐷 ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) )
61 45 anass1rs ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
62 15 61 fsumcl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
63 24 62 59 subdid ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ) = ( ( ( ∗ ‘ ( 𝑓𝐴 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ) )
64 15 24 61 fsummulc2 ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
65 57 a1i ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ∈ ℂ )
66 24 52 65 mul12d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) = ( ( log ‘ 𝑥 ) · ( ( ∗ ‘ ( 𝑓𝐴 ) ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) )
67 ovif2 ( ( ∗ ‘ ( 𝑓𝐴 ) ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) = if ( 𝑓 = 1 , ( ( ∗ ‘ ( 𝑓𝐴 ) ) · 1 ) , ( ( ∗ ‘ ( 𝑓𝐴 ) ) · if ( 𝑓𝑊 , - 1 , 0 ) ) )
68 fveq1 ( 𝑓 = 1 → ( 𝑓𝐴 ) = ( 1𝐴 ) )
69 3 ad2antrr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → 𝑁 ∈ ℕ )
70 9 ad2antrr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → 𝐴𝑈 )
71 4 1 6 8 69 70 dchr1 ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( 1𝐴 ) = 1 )
72 68 71 sylan9eqr ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓 = 1 ) → ( 𝑓𝐴 ) = 1 )
73 72 fveq2d ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓 = 1 ) → ( ∗ ‘ ( 𝑓𝐴 ) ) = ( ∗ ‘ 1 ) )
74 1re 1 ∈ ℝ
75 cjre ( 1 ∈ ℝ → ( ∗ ‘ 1 ) = 1 )
76 74 75 ax-mp ( ∗ ‘ 1 ) = 1
77 73 76 eqtrdi ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓 = 1 ) → ( ∗ ‘ ( 𝑓𝐴 ) ) = 1 )
78 77 oveq1d ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓 = 1 ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · 1 ) = ( 1 · 1 ) )
79 1t1e1 ( 1 · 1 ) = 1
80 78 79 eqtrdi ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓 = 1 ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · 1 ) = 1 )
81 df-ne ( 𝑓1 ↔ ¬ 𝑓 = 1 )
82 ovif2 ( ( ∗ ‘ ( 𝑓𝐴 ) ) · if ( 𝑓𝑊 , - 1 , 0 ) ) = if ( 𝑓𝑊 , ( ( ∗ ‘ ( 𝑓𝐴 ) ) · - 1 ) , ( ( ∗ ‘ ( 𝑓𝐴 ) ) · 0 ) )
83 11 fveq2d ( ( 𝜑𝑓𝑊 ) → ( 𝑓𝐴 ) = ( 𝑓 ‘ ( 1r𝑍 ) ) )
84 83 ad5ant15 ( ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓1 ) ∧ 𝑓𝑊 ) → ( 𝑓𝐴 ) = ( 𝑓 ‘ ( 1r𝑍 ) ) )
85 4 1 5 dchrmhm 𝐷 ⊆ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) )
86 simpr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → 𝑓𝐷 )
87 85 86 sselid ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → 𝑓 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) )
88 eqid ( mulGrp ‘ 𝑍 ) = ( mulGrp ‘ 𝑍 )
89 eqid ( 1r𝑍 ) = ( 1r𝑍 )
90 88 89 ringidval ( 1r𝑍 ) = ( 0g ‘ ( mulGrp ‘ 𝑍 ) )
91 eqid ( mulGrp ‘ ℂfld ) = ( mulGrp ‘ ℂfld )
92 cnfld1 1 = ( 1r ‘ ℂfld )
93 91 92 ringidval 1 = ( 0g ‘ ( mulGrp ‘ ℂfld ) )
94 90 93 mhm0 ( 𝑓 ∈ ( ( mulGrp ‘ 𝑍 ) MndHom ( mulGrp ‘ ℂfld ) ) → ( 𝑓 ‘ ( 1r𝑍 ) ) = 1 )
95 87 94 syl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( 𝑓 ‘ ( 1r𝑍 ) ) = 1 )
96 95 ad2antrr ( ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓1 ) ∧ 𝑓𝑊 ) → ( 𝑓 ‘ ( 1r𝑍 ) ) = 1 )
97 84 96 eqtrd ( ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓1 ) ∧ 𝑓𝑊 ) → ( 𝑓𝐴 ) = 1 )
98 97 fveq2d ( ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓1 ) ∧ 𝑓𝑊 ) → ( ∗ ‘ ( 𝑓𝐴 ) ) = ( ∗ ‘ 1 ) )
99 98 76 eqtrdi ( ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓1 ) ∧ 𝑓𝑊 ) → ( ∗ ‘ ( 𝑓𝐴 ) ) = 1 )
100 99 oveq1d ( ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓1 ) ∧ 𝑓𝑊 ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · - 1 ) = ( 1 · - 1 ) )
101 54 mulid2i ( 1 · - 1 ) = - 1
102 100 101 eqtrdi ( ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓1 ) ∧ 𝑓𝑊 ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · - 1 ) = - 1 )
103 102 ifeq1da ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓1 ) → if ( 𝑓𝑊 , ( ( ∗ ‘ ( 𝑓𝐴 ) ) · - 1 ) , ( ( ∗ ‘ ( 𝑓𝐴 ) ) · 0 ) ) = if ( 𝑓𝑊 , - 1 , ( ( ∗ ‘ ( 𝑓𝐴 ) ) · 0 ) ) )
104 24 adantr ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓1 ) → ( ∗ ‘ ( 𝑓𝐴 ) ) ∈ ℂ )
105 104 mul01d ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓1 ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · 0 ) = 0 )
106 105 ifeq2d ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓1 ) → if ( 𝑓𝑊 , - 1 , ( ( ∗ ‘ ( 𝑓𝐴 ) ) · 0 ) ) = if ( 𝑓𝑊 , - 1 , 0 ) )
107 103 106 eqtrd ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓1 ) → if ( 𝑓𝑊 , ( ( ∗ ‘ ( 𝑓𝐴 ) ) · - 1 ) , ( ( ∗ ‘ ( 𝑓𝐴 ) ) · 0 ) ) = if ( 𝑓𝑊 , - 1 , 0 ) )
108 82 107 syl5eq ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ 𝑓1 ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · if ( 𝑓𝑊 , - 1 , 0 ) ) = if ( 𝑓𝑊 , - 1 , 0 ) )
109 81 108 sylan2br ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) ∧ ¬ 𝑓 = 1 ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · if ( 𝑓𝑊 , - 1 , 0 ) ) = if ( 𝑓𝑊 , - 1 , 0 ) )
110 80 109 ifeq12da ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → if ( 𝑓 = 1 , ( ( ∗ ‘ ( 𝑓𝐴 ) ) · 1 ) , ( ( ∗ ‘ ( 𝑓𝐴 ) ) · if ( 𝑓𝑊 , - 1 , 0 ) ) ) = if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) )
111 67 110 syl5eq ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) = if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) )
112 111 oveq2d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( ( log ‘ 𝑥 ) · ( ( ∗ ‘ ( 𝑓𝐴 ) ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) = ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) )
113 66 112 eqtrd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) = ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) )
114 64 113 oveq12d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( ( ( ∗ ‘ ( 𝑓𝐴 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) )
115 63 114 eqtrd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) )
116 115 sumeq2dv ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑓𝐷 ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ) = Σ 𝑓𝐷 ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) )
117 fzfid ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
118 inss1 ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) )
119 ssfi ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ∧ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∈ Fin )
120 117 118 119 sylancl ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ∈ Fin )
121 12 phicld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ϕ ‘ 𝑁 ) ∈ ℕ )
122 121 nncnd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ϕ ‘ 𝑁 ) ∈ ℂ )
123 118 a1i ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
124 123 sselda ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
125 124 43 syldan ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
126 120 122 125 fsummulc2 ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
127 122 adantr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ϕ ‘ 𝑁 ) ∈ ℂ )
128 127 43 mulcld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
129 124 128 syldan ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) → ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
130 129 ralrimiva ( ( 𝜑𝑥 ∈ ℝ+ ) → ∀ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
131 117 olcd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( ℤ ‘ 1 ) ∨ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ) )
132 sumss2 ( ( ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ ∀ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ ) ∧ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( ℤ ‘ 1 ) ∨ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ) ) → Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) if ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) , ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) , 0 ) )
133 123 130 131 132 syl21anc ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) if ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) , ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) , 0 ) )
134 elin ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ↔ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛𝑇 ) )
135 134 baib ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ↔ 𝑛𝑇 ) )
136 135 adantl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ↔ 𝑛𝑇 ) )
137 10 eleq2i ( 𝑛𝑇𝑛 ∈ ( 𝐿 “ { 𝐴 } ) )
138 31 ffnd ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝐿 Fn ℤ )
139 fniniseg ( 𝐿 Fn ℤ → ( 𝑛 ∈ ( 𝐿 “ { 𝐴 } ) ↔ ( 𝑛 ∈ ℤ ∧ ( 𝐿𝑛 ) = 𝐴 ) ) )
140 139 baibd ( ( 𝐿 Fn ℤ ∧ 𝑛 ∈ ℤ ) → ( 𝑛 ∈ ( 𝐿 “ { 𝐴 } ) ↔ ( 𝐿𝑛 ) = 𝐴 ) )
141 138 32 140 syl2an ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 ∈ ( 𝐿 “ { 𝐴 } ) ↔ ( 𝐿𝑛 ) = 𝐴 ) )
142 137 141 syl5bb ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛𝑇 ↔ ( 𝐿𝑛 ) = 𝐴 ) )
143 136 142 bitr2d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐿𝑛 ) = 𝐴𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ) )
144 43 mul02d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 0 · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = 0 )
145 143 144 ifbieq2d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → if ( ( 𝐿𝑛 ) = 𝐴 , ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) , ( 0 · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = if ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) , ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) , 0 ) )
146 ovif ( if ( ( 𝐿𝑛 ) = 𝐴 , ( ϕ ‘ 𝑁 ) , 0 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = if ( ( 𝐿𝑛 ) = 𝐴 , ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) , ( 0 · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
147 3 ad2antrr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑁 ∈ ℕ )
148 147 13 syl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐷 ∈ Fin )
149 23 ad4ant14 ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑓𝐷 ) → ( ∗ ‘ ( 𝑓𝐴 ) ) ∈ ℂ )
150 36 149 mulcld ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑓𝐷 ) → ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ∗ ‘ ( 𝑓𝐴 ) ) ) ∈ ℂ )
151 148 43 150 fsummulc1 ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑓𝐷 ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ∗ ‘ ( 𝑓𝐴 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑓𝐷 ( ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ∗ ‘ ( 𝑓𝐴 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
152 9 ad2antrr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐴𝑈 )
153 4 5 1 16 8 147 34 152 sum2dchr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑓𝐷 ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ∗ ‘ ( 𝑓𝐴 ) ) ) = if ( ( 𝐿𝑛 ) = 𝐴 , ( ϕ ‘ 𝑁 ) , 0 ) )
154 153 oveq1d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑓𝐷 ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ∗ ‘ ( 𝑓𝐴 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( if ( ( 𝐿𝑛 ) = 𝐴 , ( ϕ ‘ 𝑁 ) , 0 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
155 43 adantr ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑓𝐷 ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
156 mulass ( ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) ∈ ℂ ∧ ( ∗ ‘ ( 𝑓𝐴 ) ) ∈ ℂ ∧ ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) → ( ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ∗ ‘ ( 𝑓𝐴 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
157 mul12 ( ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) ∈ ℂ ∧ ( ∗ ‘ ( 𝑓𝐴 ) ) ∈ ℂ ∧ ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) → ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
158 156 157 eqtrd ( ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) ∈ ℂ ∧ ( ∗ ‘ ( 𝑓𝐴 ) ) ∈ ℂ ∧ ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) → ( ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ∗ ‘ ( 𝑓𝐴 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
159 36 149 155 158 syl3anc ( ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑓𝐷 ) → ( ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ∗ ‘ ( 𝑓𝐴 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
160 159 sumeq2dv ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑓𝐷 ( ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ∗ ‘ ( 𝑓𝐴 ) ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑓𝐷 ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
161 151 154 160 3eqtr3d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( if ( ( 𝐿𝑛 ) = 𝐴 , ( ϕ ‘ 𝑁 ) , 0 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑓𝐷 ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
162 146 161 eqtr3id ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → if ( ( 𝐿𝑛 ) = 𝐴 , ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) , ( 0 · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = Σ 𝑓𝐷 ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
163 145 162 eqtr3d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → if ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) , ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) , 0 ) = Σ 𝑓𝐷 ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
164 163 sumeq2dv ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) if ( 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) , ( ( ϕ ‘ 𝑁 ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) , 0 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑓𝐷 ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
165 126 133 164 3eqtrd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑓𝐷 ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
166 117 14 46 fsumcom ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑓𝐷 ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) = Σ 𝑓𝐷 Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
167 165 166 eqtrd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑓𝐷 Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) )
168 4 dchrabl ( 𝑁 ∈ ℕ → 𝐺 ∈ Abel )
169 ablgrp ( 𝐺 ∈ Abel → 𝐺 ∈ Grp )
170 5 6 grpidcl ( 𝐺 ∈ Grp → 1𝐷 )
171 12 168 169 170 4syl ( ( 𝜑𝑥 ∈ ℝ+ ) → 1𝐷 )
172 51 mulid1d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · 1 ) = ( log ‘ 𝑥 ) )
173 172 51 eqeltrd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · 1 ) ∈ ℂ )
174 iftrue ( 𝑓 = 1 → if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) = 1 )
175 174 oveq2d ( 𝑓 = 1 → ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) = ( ( log ‘ 𝑥 ) · 1 ) )
176 175 sumsn ( ( 1𝐷 ∧ ( ( log ‘ 𝑥 ) · 1 ) ∈ ℂ ) → Σ 𝑓 ∈ { 1 } ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) = ( ( log ‘ 𝑥 ) · 1 ) )
177 171 173 176 syl2anc ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ { 1 } ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) = ( ( log ‘ 𝑥 ) · 1 ) )
178 eldifsn ( 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ↔ ( 𝑓𝐷𝑓1 ) )
179 ifnefalse ( 𝑓1 → if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) = if ( 𝑓𝑊 , - 1 , 0 ) )
180 179 ad2antll ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑓𝐷𝑓1 ) ) → if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) = if ( 𝑓𝑊 , - 1 , 0 ) )
181 negeq ( if ( 𝑓𝑊 , 1 , 0 ) = 1 → - if ( 𝑓𝑊 , 1 , 0 ) = - 1 )
182 negeq ( if ( 𝑓𝑊 , 1 , 0 ) = 0 → - if ( 𝑓𝑊 , 1 , 0 ) = - 0 )
183 neg0 - 0 = 0
184 182 183 eqtrdi ( if ( 𝑓𝑊 , 1 , 0 ) = 0 → - if ( 𝑓𝑊 , 1 , 0 ) = 0 )
185 181 184 ifsb - if ( 𝑓𝑊 , 1 , 0 ) = if ( 𝑓𝑊 , - 1 , 0 )
186 180 185 eqtr4di ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑓𝐷𝑓1 ) ) → if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) = - if ( 𝑓𝑊 , 1 , 0 ) )
187 186 oveq2d ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑓𝐷𝑓1 ) ) → ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) = ( ( log ‘ 𝑥 ) · - if ( 𝑓𝑊 , 1 , 0 ) ) )
188 51 adantr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑓𝐷𝑓1 ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
189 53 55 ifcli if ( 𝑓𝑊 , 1 , 0 ) ∈ ℂ
190 mulneg2 ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ if ( 𝑓𝑊 , 1 , 0 ) ∈ ℂ ) → ( ( log ‘ 𝑥 ) · - if ( 𝑓𝑊 , 1 , 0 ) ) = - ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , 1 , 0 ) ) )
191 188 189 190 sylancl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑓𝐷𝑓1 ) ) → ( ( log ‘ 𝑥 ) · - if ( 𝑓𝑊 , 1 , 0 ) ) = - ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , 1 , 0 ) ) )
192 187 191 eqtrd ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ ( 𝑓𝐷𝑓1 ) ) → ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) = - ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , 1 , 0 ) ) )
193 178 192 sylan2b ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ) → ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) = - ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , 1 , 0 ) ) )
194 193 sumeq2dv ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) = Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) - ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , 1 , 0 ) ) )
195 diffi ( 𝐷 ∈ Fin → ( 𝐷 ∖ { 1 } ) ∈ Fin )
196 14 195 syl ( ( 𝜑𝑥 ∈ ℝ+ ) → ( 𝐷 ∖ { 1 } ) ∈ Fin )
197 51 adantr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
198 mulcl ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ if ( 𝑓𝑊 , 1 , 0 ) ∈ ℂ ) → ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , 1 , 0 ) ) ∈ ℂ )
199 197 189 198 sylancl ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ) → ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , 1 , 0 ) ) ∈ ℂ )
200 196 199 fsumneg ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) - ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , 1 , 0 ) ) = - Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , 1 , 0 ) ) )
201 189 a1i ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ) → if ( 𝑓𝑊 , 1 , 0 ) ∈ ℂ )
202 196 51 201 fsummulc2 ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) if ( 𝑓𝑊 , 1 , 0 ) ) = Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , 1 , 0 ) ) )
203 7 ssrab3 𝑊 ⊆ ( 𝐷 ∖ { 1 } )
204 difss ( 𝐷 ∖ { 1 } ) ⊆ 𝐷
205 203 204 sstri 𝑊𝐷
206 ssfi ( ( 𝐷 ∈ Fin ∧ 𝑊𝐷 ) → 𝑊 ∈ Fin )
207 14 205 206 sylancl ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝑊 ∈ Fin )
208 fsumconst ( ( 𝑊 ∈ Fin ∧ 1 ∈ ℂ ) → Σ 𝑓𝑊 1 = ( ( ♯ ‘ 𝑊 ) · 1 ) )
209 207 53 208 sylancl ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑓𝑊 1 = ( ( ♯ ‘ 𝑊 ) · 1 ) )
210 203 a1i ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝑊 ⊆ ( 𝐷 ∖ { 1 } ) )
211 53 a1i ( ( 𝜑𝑥 ∈ ℝ+ ) → 1 ∈ ℂ )
212 211 ralrimivw ( ( 𝜑𝑥 ∈ ℝ+ ) → ∀ 𝑓𝑊 1 ∈ ℂ )
213 196 olcd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( 𝐷 ∖ { 1 } ) ⊆ ( ℤ ‘ 1 ) ∨ ( 𝐷 ∖ { 1 } ) ∈ Fin ) )
214 sumss2 ( ( ( 𝑊 ⊆ ( 𝐷 ∖ { 1 } ) ∧ ∀ 𝑓𝑊 1 ∈ ℂ ) ∧ ( ( 𝐷 ∖ { 1 } ) ⊆ ( ℤ ‘ 1 ) ∨ ( 𝐷 ∖ { 1 } ) ∈ Fin ) ) → Σ 𝑓𝑊 1 = Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) if ( 𝑓𝑊 , 1 , 0 ) )
215 210 212 213 214 syl21anc ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑓𝑊 1 = Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) if ( 𝑓𝑊 , 1 , 0 ) )
216 hashcl ( 𝑊 ∈ Fin → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
217 207 216 syl ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ♯ ‘ 𝑊 ) ∈ ℕ0 )
218 217 nn0cnd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ♯ ‘ 𝑊 ) ∈ ℂ )
219 218 mulid1d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( ♯ ‘ 𝑊 ) · 1 ) = ( ♯ ‘ 𝑊 ) )
220 209 215 219 3eqtr3d ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) if ( 𝑓𝑊 , 1 , 0 ) = ( ♯ ‘ 𝑊 ) )
221 220 oveq2d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) if ( 𝑓𝑊 , 1 , 0 ) ) = ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) )
222 202 221 eqtr3d ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , 1 , 0 ) ) = ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) )
223 222 negeqd ( ( 𝜑𝑥 ∈ ℝ+ ) → - Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , 1 , 0 ) ) = - ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) )
224 194 200 223 3eqtrd ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) = - ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) )
225 177 224 oveq12d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( Σ 𝑓 ∈ { 1 } ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) + Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) = ( ( ( log ‘ 𝑥 ) · 1 ) + - ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) ) )
226 51 218 mulcld ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) ∈ ℂ )
227 173 226 negsubd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( ( log ‘ 𝑥 ) · 1 ) + - ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) ) = ( ( ( log ‘ 𝑥 ) · 1 ) − ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) ) )
228 225 227 eqtrd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( Σ 𝑓 ∈ { 1 } ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) + Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) = ( ( ( log ‘ 𝑥 ) · 1 ) − ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) ) )
229 disjdif ( { 1 } ∩ ( 𝐷 ∖ { 1 } ) ) = ∅
230 229 a1i ( ( 𝜑𝑥 ∈ ℝ+ ) → ( { 1 } ∩ ( 𝐷 ∖ { 1 } ) ) = ∅ )
231 undif2 ( { 1 } ∪ ( 𝐷 ∖ { 1 } ) ) = ( { 1 } ∪ 𝐷 )
232 171 snssd ( ( 𝜑𝑥 ∈ ℝ+ ) → { 1 } ⊆ 𝐷 )
233 ssequn1 ( { 1 } ⊆ 𝐷 ↔ ( { 1 } ∪ 𝐷 ) = 𝐷 )
234 232 233 sylib ( ( 𝜑𝑥 ∈ ℝ+ ) → ( { 1 } ∪ 𝐷 ) = 𝐷 )
235 231 234 eqtr2id ( ( 𝜑𝑥 ∈ ℝ+ ) → 𝐷 = ( { 1 } ∪ ( 𝐷 ∖ { 1 } ) ) )
236 230 235 14 59 fsumsplit ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑓𝐷 ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) = ( Σ 𝑓 ∈ { 1 } ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) + Σ 𝑓 ∈ ( 𝐷 ∖ { 1 } ) ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) )
237 51 211 218 subdid ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) = ( ( ( log ‘ 𝑥 ) · 1 ) − ( ( log ‘ 𝑥 ) · ( ♯ ‘ 𝑊 ) ) ) )
238 228 236 237 3eqtr4rd ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) = Σ 𝑓𝐷 ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) )
239 167 238 oveq12d ( ( 𝜑𝑥 ∈ ℝ+ ) → ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) = ( Σ 𝑓𝐷 Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ) − Σ 𝑓𝐷 ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) )
240 60 116 239 3eqtr4d ( ( 𝜑𝑥 ∈ ℝ+ ) → Σ 𝑓𝐷 ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ) = ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) )
241 240 mpteq2dva ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑓𝐷 ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) )
242 rpssre + ⊆ ℝ
243 242 a1i ( 𝜑 → ℝ+ ⊆ ℝ )
244 3 13 syl ( 𝜑𝐷 ∈ Fin )
245 22 adantlr ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( 𝑓𝐴 ) ∈ ℂ )
246 245 cjcld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( ∗ ‘ ( 𝑓𝐴 ) ) ∈ ℂ )
247 62 59 subcld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ∈ ℂ )
248 246 247 mulcld ( ( ( 𝜑𝑥 ∈ ℝ+ ) ∧ 𝑓𝐷 ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ) ∈ ℂ )
249 248 anasss ( ( 𝜑 ∧ ( 𝑥 ∈ ℝ+𝑓𝐷 ) ) → ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ) ∈ ℂ )
250 23 adantr ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( ∗ ‘ ( 𝑓𝐴 ) ) ∈ ℂ )
251 247 an32s ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ∈ ℂ )
252 o1const ( ( ℝ+ ⊆ ℝ ∧ ( ∗ ‘ ( 𝑓𝐴 ) ) ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ ( ∗ ‘ ( 𝑓𝐴 ) ) ) ∈ 𝑂(1) )
253 242 23 252 sylancr ( ( 𝜑𝑓𝐷 ) → ( 𝑥 ∈ ℝ+ ↦ ( ∗ ‘ ( 𝑓𝐴 ) ) ) ∈ 𝑂(1) )
254 fveq1 ( 𝑓 = 1 → ( 𝑓 ‘ ( 𝐿𝑛 ) ) = ( 1 ‘ ( 𝐿𝑛 ) ) )
255 254 oveq1d ( 𝑓 = 1 → ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( ( 1 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
256 255 sumeq2sdv ( 𝑓 = 1 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) )
257 256 175 oveq12d ( 𝑓 = 1 → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · 1 ) ) )
258 257 adantl ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓 = 1 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · 1 ) ) )
259 49 recnd ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℂ )
260 259 mulid1d ( 𝑥 ∈ ℝ+ → ( ( log ‘ 𝑥 ) · 1 ) = ( log ‘ 𝑥 ) )
261 260 oveq2d ( 𝑥 ∈ ℝ+ → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · 1 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) )
262 258 261 sylan9eq ( ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓 = 1 ) ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) )
263 262 mpteq2dva ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓 = 1 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) )
264 1 2 3 4 5 6 rpvmasumlem ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
265 264 ad2antrr ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓 = 1 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 1 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
266 263 265 eqeltrd ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓 = 1 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ) ∈ 𝑂(1) )
267 179 oveq2d ( 𝑓1 → ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) = ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , - 1 , 0 ) ) )
268 267 oveq2d ( 𝑓1 → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , - 1 , 0 ) ) ) )
269 51 adantlr ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
270 mulcom ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ - 1 ∈ ℂ ) → ( ( log ‘ 𝑥 ) · - 1 ) = ( - 1 · ( log ‘ 𝑥 ) ) )
271 269 54 270 sylancl ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · - 1 ) = ( - 1 · ( log ‘ 𝑥 ) ) )
272 269 mulm1d ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( - 1 · ( log ‘ 𝑥 ) ) = - ( log ‘ 𝑥 ) )
273 271 272 eqtrd ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · - 1 ) = - ( log ‘ 𝑥 ) )
274 269 mul01d ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · 0 ) = 0 )
275 273 274 ifeq12d ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → if ( 𝑓𝑊 , ( ( log ‘ 𝑥 ) · - 1 ) , ( ( log ‘ 𝑥 ) · 0 ) ) = if ( 𝑓𝑊 , - ( log ‘ 𝑥 ) , 0 ) )
276 ovif2 ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , - 1 , 0 ) ) = if ( 𝑓𝑊 , ( ( log ‘ 𝑥 ) · - 1 ) , ( ( log ‘ 𝑥 ) · 0 ) )
277 negeq ( if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) = ( log ‘ 𝑥 ) → - if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) = - ( log ‘ 𝑥 ) )
278 negeq ( if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) = 0 → - if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) = - 0 )
279 278 183 eqtrdi ( if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) = 0 → - if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) = 0 )
280 277 279 ifsb - if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) = if ( 𝑓𝑊 , - ( log ‘ 𝑥 ) , 0 )
281 275 276 280 3eqtr4g ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , - 1 , 0 ) ) = - if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) )
282 281 oveq2d ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , - 1 , 0 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − - if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) ) )
283 62 an32s ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) ∈ ℂ )
284 ifcl ( ( ( log ‘ 𝑥 ) ∈ ℂ ∧ 0 ∈ ℂ ) → if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) ∈ ℂ )
285 269 55 284 sylancl ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) ∈ ℂ )
286 283 285 subnegd ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − - if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) ) )
287 282 286 eqtrd ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓𝑊 , - 1 , 0 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) ) )
288 268 287 sylan9eqr ( ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓1 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) ) )
289 288 an32s ( ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) ) )
290 289 mpteq2dva ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) )
291 3 ad2antrr ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) → 𝑁 ∈ ℕ )
292 simplr ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) → 𝑓𝐷 )
293 simpr ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) → 𝑓1 )
294 eqid ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) = ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) )
295 1 2 291 4 5 6 292 293 294 dchrmusumlema ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) → ∃ 𝑡𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) )
296 3 adantr ( ( 𝜑𝑓𝐷 ) → 𝑁 ∈ ℕ )
297 296 ad2antrr ( ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑁 ∈ ℕ )
298 292 adantr ( ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑓𝐷 )
299 simplr ( ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑓1 )
300 simprl ( ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → 𝑐 ∈ ( 0 [,) +∞ ) )
301 simprrl ( ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 )
302 simprrr ( ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) )
303 1 2 297 4 5 6 298 299 294 300 301 302 7 dchrvmaeq0 ( ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ( 𝑓𝑊𝑡 = 0 ) )
304 ifbi ( ( 𝑓𝑊𝑡 = 0 ) → if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) = if ( 𝑡 = 0 , ( log ‘ 𝑥 ) , 0 ) )
305 304 oveq2d ( ( 𝑓𝑊𝑡 = 0 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑡 = 0 , ( log ‘ 𝑥 ) , 0 ) ) )
306 305 mpteq2dv ( ( 𝑓𝑊𝑡 = 0 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑡 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) )
307 303 306 syl ( ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑡 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) )
308 1 2 297 4 5 6 298 299 294 300 301 302 dchrvmasumif ( ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑡 = 0 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) )
309 307 308 eqeltrd ( ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) ∧ ( 𝑐 ∈ ( 0 [,) +∞ ) ∧ ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) ) ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) )
310 309 rexlimdvaa ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) → ( ∃ 𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) ) )
311 310 exlimdv ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) → ( ∃ 𝑡𝑐 ∈ ( 0 [,) +∞ ) ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ⇝ 𝑡 ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( seq 1 ( + , ( 𝑎 ∈ ℕ ↦ ( ( 𝑓 ‘ ( 𝐿𝑎 ) ) / 𝑎 ) ) ) ‘ ( ⌊ ‘ 𝑦 ) ) − 𝑡 ) ) ≤ ( 𝑐 / 𝑦 ) ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) ) )
312 295 311 mpd ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) + if ( 𝑓𝑊 , ( log ‘ 𝑥 ) , 0 ) ) ) ∈ 𝑂(1) )
313 290 312 eqeltrd ( ( ( 𝜑𝑓𝐷 ) ∧ 𝑓1 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ) ∈ 𝑂(1) )
314 266 313 pm2.61dane ( ( 𝜑𝑓𝐷 ) → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ) ∈ 𝑂(1) )
315 250 251 253 314 o1mul2 ( ( 𝜑𝑓𝐷 ) → ( 𝑥 ∈ ℝ+ ↦ ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ) ) ∈ 𝑂(1) )
316 243 244 249 315 fsumo1 ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑓𝐷 ( ( ∗ ‘ ( 𝑓𝐴 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑓 ‘ ( 𝐿𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · if ( 𝑓 = 1 , 1 , if ( 𝑓𝑊 , - 1 , 0 ) ) ) ) ) ) ∈ 𝑂(1) )
317 241 316 eqeltrrd ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ϕ ‘ 𝑁 ) · Σ 𝑛 ∈ ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∩ 𝑇 ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) − ( ( log ‘ 𝑥 ) · ( 1 − ( ♯ ‘ 𝑊 ) ) ) ) ) ∈ 𝑂(1) )