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 | |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | 1nn0 | |
|
2 | logexprlim | |
|
3 | 1 2 | ax-mp | |
4 | elfznn | |
|
5 | 4 | nnrpd | |
6 | rpdivcl | |
|
7 | 5 6 | sylan2 | |
8 | 7 | relogcld | |
9 | 8 | recnd | |
10 | 9 | exp1d | |
11 | 10 | sumeq2dv | |
12 | 11 | oveq1d | |
13 | fzfid | |
|
14 | rpcn | |
|
15 | rpne0 | |
|
16 | 13 14 9 15 | fsumdivc | |
17 | 12 16 | eqtrd | |
18 | 17 | mpteq2ia | |
19 | fac1 | |
|
20 | 3 18 19 | 3brtr3i | |