This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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 mullidd ⊢ ( 𝜑 → ( 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 ‘ ( ( 𝐴 / 𝑑 ) / 𝑚 ) ) / 𝑚 ) ) ) )