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+n=1xlogxnx1

Proof

Step Hyp Ref Expression
1 1nn0 10
2 logexprlim 10x+n=1xlogxn1x1!
3 1 2 ax-mp x+n=1xlogxn1x1!
4 elfznn n1xn
5 4 nnrpd n1xn+
6 rpdivcl x+n+xn+
7 5 6 sylan2 x+n1xxn+
8 7 relogcld x+n1xlogxn
9 8 recnd x+n1xlogxn
10 9 exp1d x+n1xlogxn1=logxn
11 10 sumeq2dv x+n=1xlogxn1=n=1xlogxn
12 11 oveq1d x+n=1xlogxn1x=n=1xlogxnx
13 fzfid x+1xFin
14 rpcn x+x
15 rpne0 x+x0
16 13 14 9 15 fsumdivc x+n=1xlogxnx=n=1xlogxnx
17 12 16 eqtrd x+n=1xlogxn1x=n=1xlogxnx
18 17 mpteq2ia x+n=1xlogxn1x=x+n=1xlogxnx
19 fac1 1!=1
20 3 18 19 3brtr3i x+n=1xlogxnx1