Metamath Proof Explorer

Theorem logfacrlim2

Description: Write out logfacrlim as a sum of logs. (Contributed by Mario Carneiro, 18-May-2016) (Revised by Mario Carneiro, 22-May-2016)

Ref Expression
Assertion logfacrlim2 
|- ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) ~~>r 1

Proof

Step Hyp Ref Expression
1 1nn0 
 |-  1 e. NN0
2 logexprlim 
 |-  ( 1 e. NN0 -> ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 1 ) / x ) ) ~~>r ( ! ` 1 ) )
3 1 2 ax-mp 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 1 ) / x ) ) ~~>r ( ! ` 1 )
4 elfznn 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. NN )
5 4 nnrpd 
 |-  ( n e. ( 1 ... ( |_ ` x ) ) -> n e. RR+ )
6 rpdivcl 
 |-  ( ( x e. RR+ /\ n e. RR+ ) -> ( x / n ) e. RR+ )
7 5 6 sylan2 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( x / n ) e. RR+ )
8 7 relogcld 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. RR )
9 8 recnd 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( log ` ( x / n ) ) e. CC )
10 9 exp1d 
 |-  ( ( x e. RR+ /\ n e. ( 1 ... ( |_ ` x ) ) ) -> ( ( log ` ( x / n ) ) ^ 1 ) = ( log ` ( x / n ) ) )
11 10 sumeq2dv 
 |-  ( x e. RR+ -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 1 ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` ( x / n ) ) )
12 11 oveq1d 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 1 ) / x ) = ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` ( x / n ) ) / x ) )
13 fzfid 
 |-  ( x e. RR+ -> ( 1 ... ( |_ ` x ) ) e. Fin )
14 rpcn 
 |-  ( x e. RR+ -> x e. CC )
15 rpne0 
 |-  ( x e. RR+ -> x =/= 0 )
16 13 14 9 15 fsumdivc 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` ( x / n ) ) / x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) )
17 12 16 eqtrd 
 |-  ( x e. RR+ -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 1 ) / x ) = sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) )
18 17 mpteq2ia 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) ^ 1 ) / x ) ) = ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) )
19 fac1 
 |-  ( ! ` 1 ) = 1
20 3 18 19 3brtr3i 
 |-  ( x e. RR+ |-> sum_ n e. ( 1 ... ( |_ ` x ) ) ( ( log ` ( x / n ) ) / x ) ) ~~>r 1