Metamath Proof Explorer

Theorem dchrvmasumlem1

Description: An alternative expression for a Dirichlet-weighted von Mangoldt sum in terms of the Möbius function. Equation 9.4.11 of Shapiro, p. 377. (Contributed by Mario Carneiro, 3-May-2016)

Ref Expression
Hypotheses rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
rpvmasum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
rpvmasum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
rpvmasum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
dchrisum.b ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
dchrisum.n1 ⊢ ( 𝜑 → 𝑋 ≠ 1 )
dchrvmasum.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
Assertion dchrvmasumlem1 ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) )

Proof

Step Hyp Ref Expression
1 rpvmasum.z ⊢ 𝑍 = ( ℤ/nℤ ‘ 𝑁 )
2 rpvmasum.l ⊢ 𝐿 = ( ℤRHom ‘ 𝑍 )
3 rpvmasum.a ⊢ ( 𝜑 → 𝑁 ∈ ℕ )
4 rpvmasum.g ⊢ 𝐺 = ( DChr ‘ 𝑁 )
5 rpvmasum.d ⊢ 𝐷 = ( Base ‘ 𝐺 )
6 rpvmasum.1 ⊢ 1 = ( 0g ‘ 𝐺 )
7 dchrisum.b ⊢ ( 𝜑 → 𝑋 ∈ 𝐷 )
8 dchrisum.n1 ⊢ ( 𝜑 → 𝑋 ≠ 1 )
9 dchrvmasum.a ⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
10 2fveq3 ⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) )
11 oveq2 ⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( ( μ ‘ 𝑑 ) / 𝑛 ) = ( ( μ ‘ 𝑑 ) / ( 𝑑 · 𝑚 ) ) )
12 fvoveq1 ⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( log ‘ ( 𝑛 / 𝑑 ) ) = ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) )
13 11 12 oveq12d ⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( ( ( μ ‘ 𝑑 ) / 𝑛 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) = ( ( ( μ ‘ 𝑑 ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) )
14 10 13 oveq12d ⊢ ( 𝑛 = ( 𝑑 · 𝑚 ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( ( μ ‘ 𝑑 ) / 𝑛 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) · ( ( ( μ ‘ 𝑑 ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) ) )
15 9 rpred ⊢ ( 𝜑 → 𝐴 ∈ ℝ )
16 7 adantr ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑋 ∈ 𝐷 )
17 elfzelz ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℤ )
18 17 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℤ )
19 4 1 5 2 16 18 dchrzrhcl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
20 19 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) ∈ ℂ )
21 elrabi ⊢ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } → 𝑑 ∈ ℕ )
22 21 ad2antll ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → 𝑑 ∈ ℕ )
23 mucl ⊢ ( 𝑑 ∈ ℕ → ( μ ‘ 𝑑 ) ∈ ℤ )
24 22 23 syl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → ( μ ‘ 𝑑 ) ∈ ℤ )
25 24 zred ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → ( μ ‘ 𝑑 ) ∈ ℝ )
26 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
27 26 ad2antrl ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → 𝑛 ∈ ℕ )
28 25 27 nndivred ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → ( ( μ ‘ 𝑑 ) / 𝑛 ) ∈ ℝ )
29 28 recnd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → ( ( μ ‘ 𝑑 ) / 𝑛 ) ∈ ℂ )
30 27 nnrpd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → 𝑛 ∈ ℝ+ )
31 22 nnrpd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → 𝑑 ∈ ℝ+ )
32 30 31 rpdivcld ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → ( 𝑛 / 𝑑 ) ∈ ℝ+ )
33 32 relogcld ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → ( log ‘ ( 𝑛 / 𝑑 ) ) ∈ ℝ )
34 33 recnd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → ( log ‘ ( 𝑛 / 𝑑 ) ) ∈ ℂ )
35 29 34 mulcld ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → ( ( ( μ ‘ 𝑑 ) / 𝑛 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) ∈ ℂ )
36 20 35 mulcld ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( ( μ ‘ 𝑑 ) / 𝑛 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) ) ∈ ℂ )
37 14 15 36 dvdsflsumcom ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( ( μ ‘ 𝑑 ) / 𝑛 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) · ( ( ( μ ‘ 𝑑 ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) ) )
38 vmaf ⊢ Λ : ℕ ⟶ ℝ
39 38 a1i ⊢ ( 𝜑 → Λ : ℕ ⟶ ℝ )
40 ax-resscn ⊢ ℝ ⊆ ℂ
41 fss ⊢ ( ( Λ : ℕ ⟶ ℝ ∧ ℝ ⊆ ℂ ) → Λ : ℕ ⟶ ℂ )
42 39 40 41 sylancl ⊢ ( 𝜑 → Λ : ℕ ⟶ ℂ )
43 vmasum ⊢ ( 𝑚 ∈ ℕ → Σ 𝑖 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ( Λ ‘ 𝑖 ) = ( log ‘ 𝑚 ) )
44 43 adantl ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → Σ 𝑖 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ( Λ ‘ 𝑖 ) = ( log ‘ 𝑚 ) )
45 44 eqcomd ⊢ ( ( 𝜑 ∧ 𝑚 ∈ ℕ ) → ( log ‘ 𝑚 ) = Σ 𝑖 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ( Λ ‘ 𝑖 ) )
46 45 mpteq2dva ⊢ ( 𝜑 → ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) = ( 𝑚 ∈ ℕ ↦ Σ 𝑖 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑚 } ( Λ ‘ 𝑖 ) ) )
47 42 46 muinv ⊢ ( 𝜑 → Λ = ( 𝑛 ∈ ℕ ↦ Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) ‘ ( 𝑛 / 𝑑 ) ) ) ) )
48 47 fveq1d ⊢ ( 𝜑 → ( Λ ‘ 𝑛 ) = ( ( 𝑛 ∈ ℕ ↦ Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) ‘ ( 𝑛 / 𝑑 ) ) ) ) ‘ 𝑛 ) )
49 sumex ⊢ Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) ‘ ( 𝑛 / 𝑑 ) ) ) ∈ V
50 eqid ⊢ ( 𝑛 ∈ ℕ ↦ Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) ‘ ( 𝑛 / 𝑑 ) ) ) ) = ( 𝑛 ∈ ℕ ↦ Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) ‘ ( 𝑛 / 𝑑 ) ) ) )
51 50 fvmpt2 ⊢ ( ( 𝑛 ∈ ℕ ∧ Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) ‘ ( 𝑛 / 𝑑 ) ) ) ∈ V ) → ( ( 𝑛 ∈ ℕ ↦ Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) ‘ ( 𝑛 / 𝑑 ) ) ) ) ‘ 𝑛 ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) ‘ ( 𝑛 / 𝑑 ) ) ) )
52 26 49 51 sylancl ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → ( ( 𝑛 ∈ ℕ ↦ Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) ‘ ( 𝑛 / 𝑑 ) ) ) ) ‘ 𝑛 ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) ‘ ( 𝑛 / 𝑑 ) ) ) )
53 48 52 sylan9eq ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑛 ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) ‘ ( 𝑛 / 𝑑 ) ) ) )
54 breq1 ⊢ ( 𝑥 = 𝑑 → ( 𝑥 ∥ 𝑛 ↔ 𝑑 ∥ 𝑛 ) )
55 54 elrab ⊢ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ∥ 𝑛 ) )
56 55 simprbi ⊢ ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } → 𝑑 ∥ 𝑛 )
57 56 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → 𝑑 ∥ 𝑛 )
58 26 adantl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
59 nndivdvds ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑑 ∈ ℕ ) → ( 𝑑 ∥ 𝑛 ↔ ( 𝑛 / 𝑑 ) ∈ ℕ ) )
60 58 21 59 syl2an ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → ( 𝑑 ∥ 𝑛 ↔ ( 𝑛 / 𝑑 ) ∈ ℕ ) )
61 57 60 mpbid ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → ( 𝑛 / 𝑑 ) ∈ ℕ )
62 fveq2 ⊢ ( 𝑚 = ( 𝑛 / 𝑑 ) → ( log ‘ 𝑚 ) = ( log ‘ ( 𝑛 / 𝑑 ) ) )
63 eqid ⊢ ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) = ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) )
64 fvex ⊢ ( log ‘ ( 𝑛 / 𝑑 ) ) ∈ V
65 62 63 64 fvmpt ⊢ ( ( 𝑛 / 𝑑 ) ∈ ℕ → ( ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) ‘ ( 𝑛 / 𝑑 ) ) = ( log ‘ ( 𝑛 / 𝑑 ) ) )
66 61 65 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → ( ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) ‘ ( 𝑛 / 𝑑 ) ) = ( log ‘ ( 𝑛 / 𝑑 ) ) )
67 66 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → ( ( μ ‘ 𝑑 ) · ( ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) ‘ ( 𝑛 / 𝑑 ) ) ) = ( ( μ ‘ 𝑑 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) )
68 67 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( ( 𝑚 ∈ ℕ ↦ ( log ‘ 𝑚 ) ) ‘ ( 𝑛 / 𝑑 ) ) ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) )
69 53 68 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑛 ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) )
70 69 oveq1d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) = ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) / 𝑛 ) )
71 fzfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... 𝑛 ) ∈ Fin )
72 dvdsssfz1 ⊢ ( 𝑛 ∈ ℕ → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ⊆ ( 1 ... 𝑛 ) )
73 58 72 syl ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ⊆ ( 1 ... 𝑛 ) )
74 71 73 ssfid ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ∈ Fin )
75 58 nncnd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℂ )
76 24 zcnd ⊢ ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) → ( μ ‘ 𝑑 ) ∈ ℂ )
77 76 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → ( μ ‘ 𝑑 ) ∈ ℂ )
78 34 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → ( log ‘ ( 𝑛 / 𝑑 ) ) ∈ ℂ )
79 77 78 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → ( ( μ ‘ 𝑑 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) ∈ ℂ )
80 58 nnne0d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ≠ 0 )
81 74 75 79 80 fsumdivc ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( μ ‘ 𝑑 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) / 𝑛 ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( ( μ ‘ 𝑑 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) / 𝑛 ) )
82 21 adantl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → 𝑑 ∈ ℕ )
83 82 23 syl ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → ( μ ‘ 𝑑 ) ∈ ℤ )
84 83 zcnd ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → ( μ ‘ 𝑑 ) ∈ ℂ )
85 75 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → 𝑛 ∈ ℂ )
86 80 adantr ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → 𝑛 ≠ 0 )
87 84 78 85 86 div23d ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → ( ( ( μ ‘ 𝑑 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) / 𝑛 ) = ( ( ( μ ‘ 𝑑 ) / 𝑛 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) )
88 87 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( ( μ ‘ 𝑑 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) / 𝑛 ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( ( μ ‘ 𝑑 ) / 𝑛 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) )
89 70 81 88 3eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( ( μ ‘ 𝑑 ) / 𝑛 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) )
90 89 oveq2d ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( ( μ ‘ 𝑑 ) / 𝑛 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) ) )
91 35 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) → ( ( ( μ ‘ 𝑑 ) / 𝑛 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) ∈ ℂ )
92 74 19 91 fsummulc2 ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( ( μ ‘ 𝑑 ) / 𝑛 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( ( μ ‘ 𝑑 ) / 𝑛 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) ) )
93 90 92 eqtrd ⊢ ( ( 𝜑 ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( ( μ ‘ 𝑑 ) / 𝑛 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) ) )
94 93 sumeq2dv ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( ( μ ‘ 𝑑 ) / 𝑛 ) · ( log ‘ ( 𝑛 / 𝑑 ) ) ) ) )
95 fzfid ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ∈ Fin )
96 7 adantr ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑋 ∈ 𝐷 )
97 elfzelz ⊢ ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑑 ∈ ℤ )
98 97 adantl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ∈ ℤ )
99 4 1 5 2 96 98 dchrzrhcl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ∈ ℂ )
100 fznnfl ⊢ ( 𝐴 ∈ ℝ → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴 ) ) )
101 15 100 syl ⊢ ( 𝜑 → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑 ≤ 𝐴 ) ) )
102 101 simprbda ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ∈ ℕ )
103 102 23 syl ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( μ ‘ 𝑑 ) ∈ ℤ )
104 103 zred ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( μ ‘ 𝑑 ) ∈ ℝ )
105 104 102 nndivred ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℝ )
106 105 recnd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℂ )
107 99 106 mulcld ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ )
108 7 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑋 ∈ 𝐷 )
109 elfzelz ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) → 𝑚 ∈ ℤ )
110 109 adantl ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ∈ ℤ )
111 4 1 5 2 108 110 dchrzrhcl ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ∈ ℂ )
112 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) → 𝑚 ∈ ℕ )
113 112 adantl ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ∈ ℕ )
114 113 nnrpd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ∈ ℝ+ )
115 114 relogcld ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ )
116 115 113 nndivred ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( log ‘ 𝑚 ) / 𝑚 ) ∈ ℝ )
117 116 recnd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( log ‘ 𝑚 ) / 𝑚 ) ∈ ℂ )
118 111 117 mulcld ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ∈ ℂ )
119 95 107 118 fsummulc2 ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) )
120 99 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) ∈ ℂ )
121 106 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℂ )
122 120 121 111 117 mul4d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) · ( ( ( μ ‘ 𝑑 ) / 𝑑 ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) )
123 97 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑑 ∈ ℤ )
124 4 1 5 2 108 123 110 dchrzrhmul ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) )
125 104 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( μ ‘ 𝑑 ) ∈ ℝ )
126 125 recnd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( μ ‘ 𝑑 ) ∈ ℂ )
127 115 recnd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( log ‘ 𝑚 ) ∈ ℂ )
128 102 nnrpd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ∈ ℝ+ )
129 128 adantr ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑑 ∈ ℝ+ )
130 129 114 rpmulcld ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑑 · 𝑚 ) ∈ ℝ+ )
131 130 rpcnne0d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑑 · 𝑚 ) ∈ ℂ ∧ ( 𝑑 · 𝑚 ) ≠ 0 ) )
132 div23 ⊢ ( ( ( μ ‘ 𝑑 ) ∈ ℂ ∧ ( log ‘ 𝑚 ) ∈ ℂ ∧ ( ( 𝑑 · 𝑚 ) ∈ ℂ ∧ ( 𝑑 · 𝑚 ) ≠ 0 ) ) → ( ( ( μ ‘ 𝑑 ) · ( log ‘ 𝑚 ) ) / ( 𝑑 · 𝑚 ) ) = ( ( ( μ ‘ 𝑑 ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ 𝑚 ) ) )
133 126 127 131 132 syl3anc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( μ ‘ 𝑑 ) · ( log ‘ 𝑚 ) ) / ( 𝑑 · 𝑚 ) ) = ( ( ( μ ‘ 𝑑 ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ 𝑚 ) ) )
134 129 rpcnne0d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) )
135 114 rpcnne0d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) )
136 divmuldiv ⊢ ( ( ( ( μ ‘ 𝑑 ) ∈ ℂ ∧ ( log ‘ 𝑚 ) ∈ ℂ ) ∧ ( ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) ∧ ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) ) ) → ( ( ( μ ‘ 𝑑 ) / 𝑑 ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) = ( ( ( μ ‘ 𝑑 ) · ( log ‘ 𝑚 ) ) / ( 𝑑 · 𝑚 ) ) )
137 126 127 134 135 136 syl22anc ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( μ ‘ 𝑑 ) / 𝑑 ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) = ( ( ( μ ‘ 𝑑 ) · ( log ‘ 𝑚 ) ) / ( 𝑑 · 𝑚 ) ) )
138 113 nncnd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ∈ ℂ )
139 129 rpcnd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑑 ∈ ℂ )
140 129 rpne0d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑑 ≠ 0 )
141 138 139 140 divcan3d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑑 · 𝑚 ) / 𝑑 ) = 𝑚 )
142 141 fveq2d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) = ( log ‘ 𝑚 ) )
143 142 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( μ ‘ 𝑑 ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) = ( ( ( μ ‘ 𝑑 ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ 𝑚 ) ) )
144 133 137 143 3eqtr4rd ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( μ ‘ 𝑑 ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) = ( ( ( μ ‘ 𝑑 ) / 𝑑 ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) )
145 124 144 oveq12d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) · ( ( ( μ ‘ 𝑑 ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) ) · ( ( ( μ ‘ 𝑑 ) / 𝑑 ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) )
146 122 145 eqtr4d ⊢ ( ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) = ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) · ( ( ( μ ‘ 𝑑 ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) ) )
147 146 sumeq2dv ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) · ( ( ( μ ‘ 𝑑 ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) ) )
148 119 147 eqtrd ⊢ ( ( 𝜑 ∧ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) · ( ( ( μ ‘ 𝑑 ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) ) )
149 148 sumeq2dv ⊢ ( 𝜑 → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) · ( ( ( μ ‘ 𝑑 ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( ( 𝑑 · 𝑚 ) / 𝑑 ) ) ) ) )
150 37 94 149 3eqtr4d ⊢ ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑛 ) ) · ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿 ‘ 𝑚 ) ) · ( ( log ‘ 𝑚 ) / 𝑚 ) ) ) )