Metamath Proof Explorer

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 e. NN0 -> ( log ` ( ! ` N ) ) = sum_ k e. ( 1 ... N ) ( log ` k ) )

Proof

Step Hyp Ref Expression
1 elnn0 
 |-  ( N e. NN0 <-> ( N e. NN \/ N = 0 ) )
2 rpmulcl 
 |-  ( ( k e. RR+ /\ n e. RR+ ) -> ( k x. n ) e. RR+ )
3 2 adantl 
 |-  ( ( N e. NN /\ ( k e. RR+ /\ n e. RR+ ) ) -> ( k x. n ) e. RR+ )
4 fvi 
 |-  ( k e. _V -> ( _I ` k ) = k )
5 4 elv 
 |-  ( _I ` k ) = k
6 elfznn 
 |-  ( k e. ( 1 ... N ) -> k e. NN )
7 6 adantl 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> k e. NN )
8 7 nnrpd 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> k e. RR+ )
9 5 8 eqeltrid 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( _I ` k ) e. RR+ )
10 elnnuz 
 |-  ( N e. NN <-> N e. ( ZZ>= ` 1 ) )
11 10 biimpi 
 |-  ( N e. NN -> N e. ( ZZ>= ` 1 ) )
12 relogmul 
 |-  ( ( k e. RR+ /\ n e. RR+ ) -> ( log ` ( k x. n ) ) = ( ( log ` k ) + ( log ` n ) ) )
13 12 adantl 
 |-  ( ( N e. NN /\ ( k e. RR+ /\ n e. RR+ ) ) -> ( log ` ( k x. n ) ) = ( ( log ` k ) + ( log ` n ) ) )
14 5 fveq2i 
 |-  ( log ` ( _I ` k ) ) = ( log ` k )
15 14 a1i 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( log ` ( _I ` k ) ) = ( log ` k ) )
16 3 9 11 13 15 seqhomo 
 |-  ( N e. NN -> ( log ` ( seq 1 ( x. , _I ) ` N ) ) = ( seq 1 ( + , log ) ` N ) )
17 facnn 
 |-  ( N e. NN -> ( ! ` N ) = ( seq 1 ( x. , _I ) ` N ) )
18 17 fveq2d 
 |-  ( N e. NN -> ( log ` ( ! ` N ) ) = ( log ` ( seq 1 ( x. , _I ) ` N ) ) )
19 eqidd 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( log ` k ) = ( log ` k ) )
20 relogcl 
 |-  ( k e. RR+ -> ( log ` k ) e. RR )
21 8 20 syl 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( log ` k ) e. RR )
22 21 recnd 
 |-  ( ( N e. NN /\ k e. ( 1 ... N ) ) -> ( log ` k ) e. CC )
23 19 11 22 fsumser 
 |-  ( N e. NN -> sum_ k e. ( 1 ... N ) ( log ` k ) = ( seq 1 ( + , log ) ` N ) )
24 16 18 23 3eqtr4d 
 |-  ( N e. NN -> ( log ` ( ! ` N ) ) = sum_ k e. ( 1 ... N ) ( log ` k ) )
25 log1 
 |-  ( log ` 1 ) = 0
26 sum0 
 |-  sum_ k e. (/) ( log ` k ) = 0
27 25 26 eqtr4i 
 |-  ( log ` 1 ) = sum_ k e. (/) ( log ` k )
28 fveq2 
 |-  ( N = 0 -> ( ! ` N ) = ( ! ` 0 ) )
29 fac0 
 |-  ( ! ` 0 ) = 1
30 28 29 eqtrdi 
 |-  ( N = 0 -> ( ! ` N ) = 1 )
31 30 fveq2d 
 |-  ( N = 0 -> ( log ` ( ! ` N ) ) = ( log ` 1 ) )
32 oveq2 
 |-  ( N = 0 -> ( 1 ... N ) = ( 1 ... 0 ) )
33 fz10 
 |-  ( 1 ... 0 ) = (/)
34 32 33 eqtrdi 
 |-  ( N = 0 -> ( 1 ... N ) = (/) )
35 34 sumeq1d 
 |-  ( N = 0 -> sum_ k e. ( 1 ... N ) ( log ` k ) = sum_ k e. (/) ( log ` k ) )
36 27 31 35 3eqtr4a 
 |-  ( N = 0 -> ( log ` ( ! ` N ) ) = sum_ k e. ( 1 ... N ) ( log ` k ) )
37 24 36 jaoi 
 |-  ( ( N e. NN \/ N = 0 ) -> ( log ` ( ! ` N ) ) = sum_ k e. ( 1 ... N ) ( log ` k ) )
38 1 37 sylbi 
 |-  ( N e. NN0 -> ( log ` ( ! ` N ) ) = sum_ k e. ( 1 ... N ) ( log ` k ) )