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 β€˜ π‘š ) / π‘š ) ) ) )