Theorem logfac

Description: The logarithm of a factorial can be expressed as a finite sum of logs. (Contributed by Mario Carneiro, 17-Apr-2015)

	Ref	Expression
Assertion	logfac	⊢ ( 𝑁 ∈ ℕ0 → ( log ‘ ( ! ‘ 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( log ‘ 𝑘 ) )

Proof

Step	Hyp	Ref	Expression
1		elnn0	⊢ ( 𝑁 ∈ ℕ0 ↔ ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) )
2		rpmulcl	⊢ ( ( 𝑘 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 𝑘 · 𝑛 ) ∈ ℝ+ )
3	2	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑘 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ) → ( 𝑘 · 𝑛 ) ∈ ℝ+ )
4		fvi	⊢ ( 𝑘 ∈ V → ( I ‘ 𝑘 ) = 𝑘 )
5	4	elv	⊢ ( I ‘ 𝑘 ) = 𝑘
6		elfznn	⊢ ( 𝑘 ∈ ( 1 ... 𝑁 ) → 𝑘 ∈ ℕ )
7	6	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℕ )
8	7	nnrpd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → 𝑘 ∈ ℝ+ )
9	5 8	eqeltrid	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( I ‘ 𝑘 ) ∈ ℝ+ )
10		elnnuz	⊢ ( 𝑁 ∈ ℕ ↔ 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
11	10	biimpi	⊢ ( 𝑁 ∈ ℕ → 𝑁 ∈ ( ℤ≥ ‘ 1 ) )
12		relogmul	⊢ ( ( 𝑘 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( log ‘ ( 𝑘 · 𝑛 ) ) = ( ( log ‘ 𝑘 ) + ( log ‘ 𝑛 ) ) )
13	12	adantl	⊢ ( ( 𝑁 ∈ ℕ ∧ ( 𝑘 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) ) → ( log ‘ ( 𝑘 · 𝑛 ) ) = ( ( log ‘ 𝑘 ) + ( log ‘ 𝑛 ) ) )
14	5	fveq2i	⊢ ( log ‘ ( I ‘ 𝑘 ) ) = ( log ‘ 𝑘 )
15	14	a1i	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( log ‘ ( I ‘ 𝑘 ) ) = ( log ‘ 𝑘 ) )
16	3 9 11 13 15	seqhomo	⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( seq 1 ( · , I ) ‘ 𝑁 ) ) = ( seq 1 ( + , log ) ‘ 𝑁 ) )
17		facnn	⊢ ( 𝑁 ∈ ℕ → ( ! ‘ 𝑁 ) = ( seq 1 ( · , I ) ‘ 𝑁 ) )
18	17	fveq2d	⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( ! ‘ 𝑁 ) ) = ( log ‘ ( seq 1 ( · , I ) ‘ 𝑁 ) ) )
19		eqidd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( log ‘ 𝑘 ) = ( log ‘ 𝑘 ) )
20		relogcl	⊢ ( 𝑘 ∈ ℝ+ → ( log ‘ 𝑘 ) ∈ ℝ )
21	8 20	syl	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( log ‘ 𝑘 ) ∈ ℝ )
22	21	recnd	⊢ ( ( 𝑁 ∈ ℕ ∧ 𝑘 ∈ ( 1 ... 𝑁 ) ) → ( log ‘ 𝑘 ) ∈ ℂ )
23	19 11 22	fsumser	⊢ ( 𝑁 ∈ ℕ → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( log ‘ 𝑘 ) = ( seq 1 ( + , log ) ‘ 𝑁 ) )
24	16 18 23	3eqtr4d	⊢ ( 𝑁 ∈ ℕ → ( log ‘ ( ! ‘ 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( log ‘ 𝑘 ) )
25		log1	⊢ ( log ‘ 1 ) = 0
26		sum0	⊢ Σ 𝑘 ∈ ∅ ( log ‘ 𝑘 ) = 0
27	25 26	eqtr4i	⊢ ( log ‘ 1 ) = Σ 𝑘 ∈ ∅ ( log ‘ 𝑘 )
28		fveq2	⊢ ( 𝑁 = 0 → ( ! ‘ 𝑁 ) = ( ! ‘ 0 ) )
29		fac0	⊢ ( ! ‘ 0 ) = 1
30	28 29	eqtrdi	⊢ ( 𝑁 = 0 → ( ! ‘ 𝑁 ) = 1 )
31	30	fveq2d	⊢ ( 𝑁 = 0 → ( log ‘ ( ! ‘ 𝑁 ) ) = ( log ‘ 1 ) )
32		oveq2	⊢ ( 𝑁 = 0 → ( 1 ... 𝑁 ) = ( 1 ... 0 ) )
33		fz10	⊢ ( 1 ... 0 ) = ∅
34	32 33	eqtrdi	⊢ ( 𝑁 = 0 → ( 1 ... 𝑁 ) = ∅ )
35	34	sumeq1d	⊢ ( 𝑁 = 0 → Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( log ‘ 𝑘 ) = Σ 𝑘 ∈ ∅ ( log ‘ 𝑘 ) )
36	27 31 35	3eqtr4a	⊢ ( 𝑁 = 0 → ( log ‘ ( ! ‘ 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( log ‘ 𝑘 ) )
37	24 36	jaoi	⊢ ( ( 𝑁 ∈ ℕ ∨ 𝑁 = 0 ) → ( log ‘ ( ! ‘ 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( log ‘ 𝑘 ) )
38	1 37	sylbi	⊢ ( 𝑁 ∈ ℕ0 → ( log ‘ ( ! ‘ 𝑁 ) ) = Σ 𝑘 ∈ ( 1 ... 𝑁 ) ( log ‘ 𝑘 ) )