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

Metamath Proof Explorer

Theorem logfac2

Description: Another expression for the logarithm of a factorial, in terms of the von Mangoldt function. Equation 9.2.7 of Shapiro, p. 329. (Contributed by Mario Carneiro, 15-Apr-2016) (Revised by Mario Carneiro, 3-May-2016)

Ref Expression
Assertion logfac2 ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑘 ) · ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) )

Proof

Step Hyp Ref Expression
1 flge0nn0 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℕ0 )
2 logfac ⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℕ0 → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( log ‘ 𝑛 ) )
3 1 2 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( log ‘ 𝑛 ) )
4 fzfid ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
5 fzfid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin )
6 ssrab2 ⊢ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ⊆ ( 1 ... ( ⌊ ‘ 𝐴 ) )
7 ssfi ⊢ ( ( ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∈ Fin ∧ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ⊆ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ∈ Fin )
8 5 6 7 sylancl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ∈ Fin )
9 flcl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
10 9 adantr ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ⌊ ‘ 𝐴 ) ∈ ℤ )
11 fznn ⊢ ( ( ⌊ ‘ 𝐴 ) ∈ ℤ → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) ) )
12 10 11 syl ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ↔ ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) ) )
13 12 anbi1d ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ↔ ( ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ) )
14 nnre ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℝ )
15 14 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑘 ∈ ℝ )
16 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ∈ ℕ )
17 16 ad2antrl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑛 ∈ ℕ )
18 17 nnred ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑛 ∈ ℝ )
19 reflcl ⊢ ( 𝐴 ∈ ℝ → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
20 19 ad3antrrr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → ( ⌊ ‘ 𝐴 ) ∈ ℝ )
21 simprr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑘 ∥ 𝑛 )
22 nnz ⊢ ( 𝑘 ∈ ℕ → 𝑘 ∈ ℤ )
23 22 ad2antlr ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑘 ∈ ℤ )
24 dvdsle ⊢ ( ( 𝑘 ∈ ℤ ∧ 𝑛 ∈ ℕ ) → ( 𝑘 ∥ 𝑛 → 𝑘 ≤ 𝑛 ) )
25 23 17 24 syl2anc ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → ( 𝑘 ∥ 𝑛 → 𝑘 ≤ 𝑛 ) )
26 21 25 mpd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑘 ≤ 𝑛 )
27 elfzle2 ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑛 ≤ ( ⌊ ‘ 𝐴 ) )
28 27 ad2antrl ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑛 ≤ ( ⌊ ‘ 𝐴 ) )
29 15 18 20 26 28 letrd ⊢ ( ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ℕ ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑘 ≤ ( ⌊ ‘ 𝐴 ) )
30 29 expl ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝑘 ∈ ℕ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) → 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) )
31 30 pm4.71rd ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝑘 ∈ ℕ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ↔ ( 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ) ) )
32 an12 ⊢ ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛 ) ) ↔ ( 𝑘 ∈ ℕ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) )
33 an21 ⊢ ( ( ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ↔ ( 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ∧ ( 𝑘 ∈ ℕ ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ) )
34 31 32 33 3bitr4g ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛 ) ) ↔ ( ( 𝑘 ∈ ℕ ∧ 𝑘 ≤ ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ) )
35 13 34 bitr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) ↔ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛 ) ) ) )
36 breq2 ⊢ ( 𝑥 = 𝑛 → ( 𝑘 ∥ 𝑥 ↔ 𝑘 ∥ 𝑛 ) )
37 36 elrab ⊢ ( 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ↔ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) )
38 37 anbi2i ⊢ ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) ↔ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∥ 𝑛 ) ) )
39 breq1 ⊢ ( 𝑥 = 𝑘 → ( 𝑥 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛 ) )
40 39 elrab ⊢ ( 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ↔ ( 𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛 ) )
41 40 anbi2i ⊢ ( ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ↔ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ ( 𝑘 ∈ ℕ ∧ 𝑘 ∥ 𝑛 ) ) )
42 35 38 41 3bitr4g ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) ↔ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ) ) )
43 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → 𝑘 ∈ ℕ )
44 43 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑘 ∈ ℕ )
45 vmacl ⊢ ( 𝑘 ∈ ℕ → ( Λ ‘ 𝑘 ) ∈ ℝ )
46 44 45 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑘 ) ∈ ℝ )
47 46 recnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( Λ ‘ 𝑘 ) ∈ ℂ )
48 47 adantrr ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∧ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) ) → ( Λ ‘ 𝑘 ) ∈ ℂ )
49 4 4 8 42 48 fsumcom2 ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ( Λ ‘ 𝑘 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( Λ ‘ 𝑘 ) )
50 fsumconst ⊢ ( ( { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ∈ Fin ∧ ( Λ ‘ 𝑘 ) ∈ ℂ ) → Σ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ( Λ ‘ 𝑘 ) = ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) · ( Λ ‘ 𝑘 ) ) )
51 8 47 50 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ( Λ ‘ 𝑘 ) = ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) · ( Λ ‘ 𝑘 ) ) )
52 fzfid ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ∈ Fin )
53 simpll ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝐴 ∈ ℝ )
54 eqid ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ↦ ( 𝑘 · 𝑚 ) ) = ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ↦ ( 𝑘 · 𝑚 ) )
55 53 44 54 dvdsflf1o ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ↦ ( 𝑘 · 𝑚 ) ) : ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) –1-1-onto→ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } )
56 52 55 hasheqf1od ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ) = ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) )
57 simpl ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → 𝐴 ∈ ℝ )
58 nndivre ⊢ ( ( 𝐴 ∈ ℝ ∧ 𝑘 ∈ ℕ ) → ( 𝐴 / 𝑘 ) ∈ ℝ )
59 57 43 58 syl2an ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( 𝐴 / 𝑘 ) ∈ ℝ )
60 nngt0 ⊢ ( 𝑘 ∈ ℕ → 0 < 𝑘 )
61 14 60 jca ⊢ ( 𝑘 ∈ ℕ → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
62 43 61 syl ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) → ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) )
63 divge0 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ ( 𝑘 ∈ ℝ ∧ 0 < 𝑘 ) ) → 0 ≤ ( 𝐴 / 𝑘 ) )
64 62 63 sylan2 ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 0 ≤ ( 𝐴 / 𝑘 ) )
65 flge0nn0 ⊢ ( ( ( 𝐴 / 𝑘 ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / 𝑘 ) ) → ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ∈ ℕ0 )
66 59 64 65 syl2anc ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ∈ ℕ0 )
67 hashfz1 ⊢ ( ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ) = ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) )
68 66 67 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) ) = ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) )
69 56 68 eqtr3d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) = ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) )
70 69 oveq1d ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ♯ ‘ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ) · ( Λ ‘ 𝑘 ) ) = ( ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) · ( Λ ‘ 𝑘 ) ) )
71 59 flcld ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ∈ ℤ )
72 71 zcnd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ∈ ℂ )
73 72 47 mulcomd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → ( ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) · ( Λ ‘ 𝑘 ) ) = ( ( Λ ‘ 𝑘 ) · ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) )
74 51 70 73 3eqtrd ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ( Λ ‘ 𝑘 ) = ( ( Λ ‘ 𝑘 ) · ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) )
75 74 sumeq2dv ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑛 ∈ { 𝑥 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ∣ 𝑘 ∥ 𝑥 } ( Λ ‘ 𝑘 ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑘 ) · ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) )
76 16 adantl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → 𝑛 ∈ ℕ )
77 vmasum ⊢ ( 𝑛 ∈ ℕ → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( Λ ‘ 𝑘 ) = ( log ‘ 𝑛 ) )
78 76 77 syl ⊢ ( ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ) → Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( Λ ‘ 𝑘 ) = ( log ‘ 𝑛 ) )
79 78 sumeq2dv ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) Σ 𝑘 ∈ { 𝑥 ∈ ℕ ∣ 𝑥 ∥ 𝑛 } ( Λ ‘ 𝑘 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( log ‘ 𝑛 ) )
80 49 75 79 3eqtr3d ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑘 ) · ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( log ‘ 𝑛 ) )
81 3 80 eqtr4d ⊢ ( ( 𝐴 ∈ ℝ ∧ 0 ≤ 𝐴 ) → ( log ‘ ( ! ‘ ( ⌊ ‘ 𝐴 ) ) ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑘 ) · ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) )