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 ... ( ⌊ ‘ 𝐴 ) ) ( ( Λ ‘ 𝑘 ) · ( ⌊ ‘ ( 𝐴 / 𝑘 ) ) ) )