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 ) )