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