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 sseldi ⊢ ( 𝜑 → 𝐴 ∈ ( 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 sseldi ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑓 ∈ 𝐷 ) → 𝑓 ∈ ( ( 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 syl5eqr ⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 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 syl5req ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ+ ) → 𝐷 = ( { 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) )