Metamath Proof Explorer


Theorem dchrvmasum2lem

Description: Give an expression for log x remarkably similar to sum_ n <_ x ( X ( n ) Lam ( n ) / n ) given in dchrvmasumlem1 . Part of Lemma 9.4.3 of Shapiro, p. 380. (Contributed by Mario Carneiro, 4-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 ( 𝜑𝐴 ∈ ℝ+ )
dchrvmasum2.2 ( 𝜑 → 1 ≤ 𝐴 )
Assertion dchrvmasum2lem ( 𝜑 → ( log ‘ 𝐴 ) = Σ 𝑑 ∈ ( 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 dchrvmasum2.2 ( 𝜑 → 1 ≤ 𝐴 )
11 2fveq3 ( 𝑛 = ( 𝑑 · 𝑚 ) → ( 𝑋 ‘ ( 𝐿𝑛 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) )
12 id ( 𝑛 = ( 𝑑 · 𝑚 ) → 𝑛 = ( 𝑑 · 𝑚 ) )
13 11 12 oveq12d ( 𝑛 = ( 𝑑 · 𝑚 ) → ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) )
14 oveq2 ( 𝑛 = ( 𝑑 · 𝑚 ) → ( 𝐴 / 𝑛 ) = ( 𝐴 / ( 𝑑 · 𝑚 ) ) )
15 14 fveq2d ( 𝑛 = ( 𝑑 · 𝑚 ) → ( log ‘ ( 𝐴 / 𝑛 ) ) = ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) )
16 13 15 oveq12d ( 𝑛 = ( 𝑑 · 𝑚 ) → ( ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) )
17 16 oveq2d ( 𝑛 = ( 𝑑 · 𝑚 ) → ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) ) = ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) ) )
18 9 rpred ( 𝜑𝐴 ∈ ℝ )
19 elrabi ( 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥𝑛 } → 𝑑 ∈ ℕ )
20 19 ad2antll ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥𝑛 } ) ) → 𝑑 ∈ ℕ )
21 mucl ( 𝑑 ∈ ℕ → ( μ ‘ 𝑑 ) ∈ ℤ )
22 20 21 syl ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥𝑛 } ) ) → ( μ ‘ 𝑑 ) ∈ ℤ )
23 22 zcnd ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥𝑛 } ) ) → ( μ ‘ 𝑑 ) ∈ ℂ )
24 7 adantr ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑋𝐷 )
25 elfzelz ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℤ )
26 25 adantl ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℤ )
27 4 1 5 2 24 26 dchrzrhcl ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑋 ‘ ( 𝐿𝑛 ) ) ∈ ℂ )
28 elfznn ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
29 28 adantl ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
30 29 nncnd ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℂ )
31 29 nnne0d ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ≠ 0 )
32 27 30 31 divcld ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) ∈ ℂ )
33 28 nnrpd ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℝ+ )
34 rpdivcl ( ( 𝐴 ∈ ℝ+𝑛 ∈ ℝ+ ) → ( 𝐴 / 𝑛 ) ∈ ℝ+ )
35 9 33 34 syl2an ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 / 𝑛 ) ∈ ℝ+ )
36 35 relogcld ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ ( 𝐴 / 𝑛 ) ) ∈ ℝ )
37 36 recnd ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( log ‘ ( 𝐴 / 𝑛 ) ) ∈ ℂ )
38 32 37 mulcld ( ( 𝜑𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) ∈ ℂ )
39 38 adantrr ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥𝑛 } ) ) → ( ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) ∈ ℂ )
40 23 39 mulcld ( ( 𝜑 ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥𝑛 } ) ) → ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) ) ∈ ℂ )
41 17 18 40 dvdsflsumcom ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥𝑛 } ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) ) )
42 2fveq3 ( 𝑛 = 1 → ( 𝑋 ‘ ( 𝐿𝑛 ) ) = ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) )
43 id ( 𝑛 = 1 → 𝑛 = 1 )
44 42 43 oveq12d ( 𝑛 = 1 → ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) = ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) )
45 oveq2 ( 𝑛 = 1 → ( 𝐴 / 𝑛 ) = ( 𝐴 / 1 ) )
46 45 fveq2d ( 𝑛 = 1 → ( log ‘ ( 𝐴 / 𝑛 ) ) = ( log ‘ ( 𝐴 / 1 ) ) )
47 44 46 oveq12d ( 𝑛 = 1 → ( ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) · ( log ‘ ( 𝐴 / 1 ) ) ) )
48 fzfid ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
49 fz1ssnn ( 1 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ℕ
50 49 a1i ( 𝜑 → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ⊆ ℕ )
51 flge1nn ( ( 𝐴 ∈ ℝ ∧ 1 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ )
52 18 10 51 syl2anc ( 𝜑 → ( ⌊ ‘ 𝐴 ) ∈ ℕ )
53 nnuz ℕ = ( ℤ ‘ 1 )
54 52 53 eleqtrdi ( 𝜑 → ( ⌊ ‘ 𝐴 ) ∈ ( ℤ ‘ 1 ) )
55 eluzfz1 ( ( ⌊ ‘ 𝐴 ) ∈ ( ℤ ‘ 1 ) → 1 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
56 54 55 syl ( 𝜑 → 1 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) )
57 47 48 50 56 38 musumsum ( 𝜑 → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥𝑛 } ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) ) = ( ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) · ( log ‘ ( 𝐴 / 1 ) ) ) )
58 4 1 5 2 7 dchrzrh1 ( 𝜑 → ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) = 1 )
59 58 oveq1d ( 𝜑 → ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) = ( 1 / 1 ) )
60 1div1e1 ( 1 / 1 ) = 1
61 59 60 eqtrdi ( 𝜑 → ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) = 1 )
62 9 rpcnd ( 𝜑𝐴 ∈ ℂ )
63 62 div1d ( 𝜑 → ( 𝐴 / 1 ) = 𝐴 )
64 63 fveq2d ( 𝜑 → ( log ‘ ( 𝐴 / 1 ) ) = ( log ‘ 𝐴 ) )
65 61 64 oveq12d ( 𝜑 → ( ( ( 𝑋 ‘ ( 𝐿 ‘ 1 ) ) / 1 ) · ( log ‘ ( 𝐴 / 1 ) ) ) = ( 1 · ( log ‘ 𝐴 ) ) )
66 9 relogcld ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℝ )
67 66 recnd ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℂ )
68 67 mulid2d ( 𝜑 → ( 1 · ( log ‘ 𝐴 ) ) = ( log ‘ 𝐴 ) )
69 57 65 68 3eqtrrd ( 𝜑 → ( log ‘ 𝐴 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑑 ∈ { 𝑥 ∈ ℕ ∣ 𝑥𝑛 } ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿𝑛 ) ) / 𝑛 ) · ( log ‘ ( 𝐴 / 𝑛 ) ) ) ) )
70 fzfid ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ∈ Fin )
71 7 adantr ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑋𝐷 )
72 elfzelz ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑑 ∈ ℤ )
73 72 adantl ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ∈ ℤ )
74 4 1 5 2 71 73 dchrzrhcl ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑋 ‘ ( 𝐿𝑑 ) ) ∈ ℂ )
75 fznnfl ( 𝐴 ∈ ℝ → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑𝐴 ) ) )
76 18 75 syl ( 𝜑 → ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑑 ∈ ℕ ∧ 𝑑𝐴 ) ) )
77 76 simprbda ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ∈ ℕ )
78 77 21 syl ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( μ ‘ 𝑑 ) ∈ ℤ )
79 78 zred ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( μ ‘ 𝑑 ) ∈ ℝ )
80 79 77 nndivred ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℝ )
81 80 recnd ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( μ ‘ 𝑑 ) / 𝑑 ) ∈ ℂ )
82 74 81 mulcld ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) ∈ ℂ )
83 7 ad2antrr ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑋𝐷 )
84 elfzelz ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) → 𝑚 ∈ ℤ )
85 84 adantl ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ∈ ℤ )
86 4 1 5 2 83 85 dchrzrhcl ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑋 ‘ ( 𝐿𝑚 ) ) ∈ ℂ )
87 elfznn ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑑 ∈ ℕ )
88 87 nnrpd ( 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑑 ∈ ℝ+ )
89 rpdivcl ( ( 𝐴 ∈ ℝ+𝑑 ∈ ℝ+ ) → ( 𝐴 / 𝑑 ) ∈ ℝ+ )
90 9 88 89 syl2an ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 / 𝑑 ) ∈ ℝ+ )
91 elfznn ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) → 𝑚 ∈ ℕ )
92 91 nnrpd ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) → 𝑚 ∈ ℝ+ )
93 rpdivcl ( ( ( 𝐴 / 𝑑 ) ∈ ℝ+𝑚 ∈ ℝ+ ) → ( ( 𝐴 / 𝑑 ) / 𝑚 ) ∈ ℝ+ )
94 90 92 93 syl2an ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝐴 / 𝑑 ) / 𝑚 ) ∈ ℝ+ )
95 94 relogcld ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ∈ ℝ )
96 91 adantl ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ∈ ℕ )
97 95 96 nndivred ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ∈ ℝ )
98 97 recnd ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ∈ ℂ )
99 86 98 mulcld ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ∈ ℂ )
100 70 82 99 fsummulc2 ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) )
101 74 adantr ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑋 ‘ ( 𝐿𝑑 ) ) ∈ ℂ )
102 79 adantr ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( μ ‘ 𝑑 ) ∈ ℝ )
103 102 recnd ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( μ ‘ 𝑑 ) ∈ ℂ )
104 77 nnrpd ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑑 ∈ ℝ+ )
105 104 adantr ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑑 ∈ ℝ+ )
106 105 rpcnne0d ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) )
107 div12 ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) ∈ ℂ ∧ ( μ ‘ 𝑑 ) ∈ ℂ ∧ ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) ) → ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) = ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) ) )
108 101 103 106 107 syl3anc ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) = ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) ) )
109 95 recnd ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ∈ ℂ )
110 96 nnrpd ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ∈ ℝ+ )
111 110 rpcnne0d ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) )
112 div12 ( ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) ∈ ℂ ∧ ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ∈ ℂ ∧ ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) ) → ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) = ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) )
113 86 109 111 112 syl3anc ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) = ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) )
114 108 113 oveq12d ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) = ( ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) ) )
115 105 rpcnd ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑑 ∈ ℂ )
116 105 rpne0d ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑑 ≠ 0 )
117 101 115 116 divcld ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) ∈ ℂ )
118 96 nncnd ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ∈ ℂ )
119 96 nnne0d ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑚 ≠ 0 )
120 86 118 119 divcld ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ∈ ℂ )
121 117 120 mulcld ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) ∈ ℂ )
122 103 109 121 mulassd ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( μ ‘ 𝑑 ) · ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ) · ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) ) = ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) ) ) )
123 103 117 109 120 mul4d ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) ) = ( ( ( μ ‘ 𝑑 ) · ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ) · ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) ) )
124 72 ad2antlr ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝑑 ∈ ℤ )
125 4 1 5 2 83 124 85 dchrzrhmul ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) = ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) · ( 𝑋 ‘ ( 𝐿𝑚 ) ) ) )
126 125 oveq1d ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) = ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) · ( 𝑋 ‘ ( 𝐿𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) )
127 divmuldiv ( ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) ∈ ℂ ∧ ( 𝑋 ‘ ( 𝐿𝑚 ) ) ∈ ℂ ) ∧ ( ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) ∧ ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) = ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) · ( 𝑋 ‘ ( 𝐿𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) )
128 101 86 106 111 127 syl22anc ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) = ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) · ( 𝑋 ‘ ( 𝐿𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) )
129 126 128 eqtr4d ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) = ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) )
130 62 ad2antrr ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → 𝐴 ∈ ℂ )
131 divdiv1 ( ( 𝐴 ∈ ℂ ∧ ( 𝑑 ∈ ℂ ∧ 𝑑 ≠ 0 ) ∧ ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) ) → ( ( 𝐴 / 𝑑 ) / 𝑚 ) = ( 𝐴 / ( 𝑑 · 𝑚 ) ) )
132 130 106 111 131 syl3anc ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( 𝐴 / 𝑑 ) / 𝑚 ) = ( 𝐴 / ( 𝑑 · 𝑚 ) ) )
133 132 eqcomd ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( 𝐴 / ( 𝑑 · 𝑚 ) ) = ( ( 𝐴 / 𝑑 ) / 𝑚 ) )
134 133 fveq2d ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) = ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) )
135 129 134 oveq12d ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) = ( ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) · ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ) )
136 121 109 mulcomd ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) · ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) ) = ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) ) )
137 135 136 eqtrd ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) = ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) ) )
138 137 oveq2d ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) ) = ( ( μ ‘ 𝑑 ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) ) ) )
139 122 123 138 3eqtr4d ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( μ ‘ 𝑑 ) · ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) / 𝑑 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) / 𝑚 ) ) ) = ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) ) )
140 114 139 eqtrd ( ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) = ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) ) )
141 140 sumeq2dv ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) ) )
142 100 141 eqtrd ( ( 𝜑𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) ) )
143 142 sumeq2dv ( 𝜑 → Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( μ ‘ 𝑑 ) · ( ( ( 𝑋 ‘ ( 𝐿 ‘ ( 𝑑 · 𝑚 ) ) ) / ( 𝑑 · 𝑚 ) ) · ( log ‘ ( 𝐴 / ( 𝑑 · 𝑚 ) ) ) ) ) )
144 41 69 143 3eqtr4d ( 𝜑 → ( log ‘ 𝐴 ) = Σ 𝑑 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( ( 𝑋 ‘ ( 𝐿𝑑 ) ) · ( ( μ ‘ 𝑑 ) / 𝑑 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑑 ) ) ) ( ( 𝑋 ‘ ( 𝐿𝑚 ) ) · ( ( log ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) )