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	$$⊢N\in {\mathbb{N}}_0\to \log N!=\sum _{k=1}^N\log k$$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$$⊢N\in {\mathbb{N}}_0\leftrightarrow \left(N\in \mathbb{N}\vee N=0\right)$$
2		rpmulcl	$$⊢\left(k\in {ℝ}^{+}\wedge n\in {ℝ}^{+}\right)\to kn\in {ℝ}^{+}$$
3	2	adantl	$$⊢\left(N\in \mathbb{N}\wedge \left(k\in {ℝ}^{+}\wedge n\in {ℝ}^{+}\right)\right)\to kn\in {ℝ}^{+}$$
4		fvi	$$⊢k\in \mathrm{V}\to \mathrm{I}\left(k\right)=k$$
5	4	elv	$$⊢\mathrm{I}\left(k\right)=k$$
6		elfznn	$$⊢k\in \left(1\dots N\right)\to k\in \mathbb{N}$$
7	6	adantl	$$⊢\left(N\in \mathbb{N}\wedge k\in \left(1\dots N\right)\right)\to k\in \mathbb{N}$$
8	7	nnrpd	$$⊢\left(N\in \mathbb{N}\wedge k\in \left(1\dots N\right)\right)\to k\in {ℝ}^{+}$$
9	5 8	eqeltrid	$$⊢\left(N\in \mathbb{N}\wedge k\in \left(1\dots N\right)\right)\to \mathrm{I}\left(k\right)\in {ℝ}^{+}$$
10		elnnuz	$$⊢N\in \mathbb{N}\leftrightarrow N\in {\mathbb{Z}}_{\ge 1}$$
11	10	biimpi	$$⊢N\in \mathbb{N}\to N\in {\mathbb{Z}}_{\ge 1}$$
12		relogmul	$$⊢\left(k\in {ℝ}^{+}\wedge n\in {ℝ}^{+}\right)\to \log kn=\log k+\log n$$
13	12	adantl	$$⊢\left(N\in \mathbb{N}\wedge \left(k\in {ℝ}^{+}\wedge n\in {ℝ}^{+}\right)\right)\to \log kn=\log k+\log n$$
14	5	fveq2i	$$⊢\log \mathrm{I}\left(k\right)=\log k$$
15	14	a1i	$$⊢\left(N\in \mathbb{N}\wedge k\in \left(1\dots N\right)\right)\to \log \mathrm{I}\left(k\right)=\log k$$
16	3 9 11 13 15	seqhomo	$$⊢N\in \mathbb{N}\to \log seq1\left(\times ,\mathrm{I}\right)\left(N\right)=seq1\left(+,log\right)\left(N\right)$$
17		facnn	$$⊢N\in \mathbb{N}\to N!=seq1\left(\times ,\mathrm{I}\right)\left(N\right)$$
18	17	fveq2d	$$⊢N\in \mathbb{N}\to \log N!=\log seq1\left(\times ,\mathrm{I}\right)\left(N\right)$$
19		eqidd	$$⊢\left(N\in \mathbb{N}\wedge k\in \left(1\dots N\right)\right)\to \log k=\log k$$
20		relogcl	$$⊢k\in {ℝ}^{+}\to \log k\in ℝ$$
21	8 20	syl	$$⊢\left(N\in \mathbb{N}\wedge k\in \left(1\dots N\right)\right)\to \log k\in ℝ$$
22	21	recnd	$$⊢\left(N\in \mathbb{N}\wedge k\in \left(1\dots N\right)\right)\to \log k\in ℂ$$
23	19 11 22	fsumser	$$⊢N\in \mathbb{N}\to \sum _{k=1}^N\log k=seq1\left(+,log\right)\left(N\right)$$
24	16 18 23	3eqtr4d	$$⊢N\in \mathbb{N}\to \log N!=\sum _{k=1}^N\log k$$
25		log1	$$⊢\log 1=0$$
26		sum0	$$⊢\sum _{k\in \varnothing }\log k=0$$
27	25 26	eqtr4i	$$⊢\log 1=\sum _{k\in \varnothing }\log k$$
28		fveq2	$$⊢N=0\to N!=0!$$
29		fac0	$$⊢0!=1$$
30	28 29	eqtrdi	$$⊢N=0\to N!=1$$
31	30	fveq2d	$$⊢N=0\to \log N!=\log 1$$
32		oveq2	$$⊢N=0\to \left(1\dots N\right)=\left(1\dots 0\right)$$
33		fz10	$$⊢\left(1\dots 0\right)=\varnothing$$
34	32 33	eqtrdi	$$⊢N=0\to \left(1\dots N\right)=\varnothing$$
35	34	sumeq1d	$$⊢N=0\to \sum _{k=1}^N\log k=\sum _{k\in \varnothing }\log k$$
36	27 31 35	3eqtr4a	$$⊢N=0\to \log N!=\sum _{k=1}^N\log k$$
37	24 36	jaoi	$$⊢\left(N\in \mathbb{N}\vee N=0\right)\to \log N!=\sum _{k=1}^N\log k$$
38	1 37	sylbi	$$⊢N\in {\mathbb{N}}_0\to \log N!=\sum _{k=1}^N\log k$$