Metamath Proof Explorer

Theorem logfacrlim

Description: Combine the estimates logfacubnd and logfaclbnd , to get log ( x ! ) = x log x + O ( x ) . Equation 9.2.9 of Shapiro, p. 329. This is a weak form of the even stronger statement, log ( x ! ) = x log x - x + O ( log x ) . (Contributed by Mario Carneiro, 16-Apr-2016) (Revised by Mario Carneiro, 21-May-2016)

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

Proof

Step Hyp Ref Expression
1 1red 
 |-  ( T. -> 1 e. RR )
2 1cnd 
 |-  ( T. -> 1 e. CC )
3 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
4 3 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( log ` x ) e. RR )
5 4 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( log ` x ) e. CC )
6 1cnd 
 |-  ( ( T. /\ x e. RR+ ) -> 1 e. CC )
7 rpcnne0 
 |-  ( x e. RR+ -> ( x e. CC /\ x =/= 0 ) )
8 7 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( x e. CC /\ x =/= 0 ) )
9 divdir 
 |-  ( ( ( log ` x ) e. CC /\ 1 e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( log ` x ) + 1 ) / x ) = ( ( ( log ` x ) / x ) + ( 1 / x ) ) )
10 5 6 8 9 syl3anc 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( log ` x ) + 1 ) / x ) = ( ( ( log ` x ) / x ) + ( 1 / x ) ) )
11 10 mpteq2dva 
 |-  ( T. -> ( x e. RR+ |-> ( ( ( log ` x ) + 1 ) / x ) ) = ( x e. RR+ |-> ( ( ( log ` x ) / x ) + ( 1 / x ) ) ) )
12 simpr 
 |-  ( ( T. /\ x e. RR+ ) -> x e. RR+ )
13 4 12 rerpdivcld 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( log ` x ) / x ) e. RR )
14 rpreccl 
 |-  ( x e. RR+ -> ( 1 / x ) e. RR+ )
15 14 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( 1 / x ) e. RR+ )
16 15 rpred 
 |-  ( ( T. /\ x e. RR+ ) -> ( 1 / x ) e. RR )
17 8 simpld 
 |-  ( ( T. /\ x e. RR+ ) -> x e. CC )
18 17 cxp1d 
 |-  ( ( T. /\ x e. RR+ ) -> ( x ^c 1 ) = x )
19 18 oveq2d 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( log ` x ) / ( x ^c 1 ) ) = ( ( log ` x ) / x ) )
20 19 mpteq2dva 
 |-  ( T. -> ( x e. RR+ |-> ( ( log ` x ) / ( x ^c 1 ) ) ) = ( x e. RR+ |-> ( ( log ` x ) / x ) ) )
21 1rp 
 |-  1 e. RR+
22 cxploglim 
 |-  ( 1 e. RR+ -> ( x e. RR+ |-> ( ( log ` x ) / ( x ^c 1 ) ) ) ~~>r 0 )
23 21 22 mp1i 
 |-  ( T. -> ( x e. RR+ |-> ( ( log ` x ) / ( x ^c 1 ) ) ) ~~>r 0 )
24 20 23 eqbrtrrd 
 |-  ( T. -> ( x e. RR+ |-> ( ( log ` x ) / x ) ) ~~>r 0 )
25 ax-1cn 
 |-  1 e. CC
26 divrcnv 
 |-  ( 1 e. CC -> ( x e. RR+ |-> ( 1 / x ) ) ~~>r 0 )
27 25 26 mp1i 
 |-  ( T. -> ( x e. RR+ |-> ( 1 / x ) ) ~~>r 0 )
28 13 16 24 27 rlimadd 
 |-  ( T. -> ( x e. RR+ |-> ( ( ( log ` x ) / x ) + ( 1 / x ) ) ) ~~>r ( 0 + 0 ) )
29 11 28 eqbrtrd 
 |-  ( T. -> ( x e. RR+ |-> ( ( ( log ` x ) + 1 ) / x ) ) ~~>r ( 0 + 0 ) )
30 00id 
 |-  ( 0 + 0 ) = 0
31 29 30 breqtrdi 
 |-  ( T. -> ( x e. RR+ |-> ( ( ( log ` x ) + 1 ) / x ) ) ~~>r 0 )
32 peano2re 
 |-  ( ( log ` x ) e. RR -> ( ( log ` x ) + 1 ) e. RR )
33 4 32 syl 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( log ` x ) + 1 ) e. RR )
34 33 12 rerpdivcld 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( log ` x ) + 1 ) / x ) e. RR )
35 34 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( ( log ` x ) + 1 ) / x ) e. CC )
36 rprege0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 <_ x ) )
37 36 adantl 
 |-  ( ( T. /\ x e. RR+ ) -> ( x e. RR /\ 0 <_ x ) )
38 flge0nn0 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( |_ ` x ) e. NN0 )
39 faccl 
 |-  ( ( |_ ` x ) e. NN0 -> ( ! ` ( |_ ` x ) ) e. NN )
40 37 38 39 3syl 
 |-  ( ( T. /\ x e. RR+ ) -> ( ! ` ( |_ ` x ) ) e. NN )
41 40 nnrpd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ! ` ( |_ ` x ) ) e. RR+ )
42 relogcl 
 |-  ( ( ! ` ( |_ ` x ) ) e. RR+ -> ( log ` ( ! ` ( |_ ` x ) ) ) e. RR )
43 41 42 syl 
 |-  ( ( T. /\ x e. RR+ ) -> ( log ` ( ! ` ( |_ ` x ) ) ) e. RR )
44 43 12 rerpdivcld 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) e. RR )
45 44 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) e. CC )
46 5 45 subcld 
 |-  ( ( T. /\ x e. RR+ ) -> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) e. CC )
47 logfacbnd3 
 |-  ( ( x e. RR+ /\ 1 <_ x ) -> ( abs ` ( ( log ` ( ! ` ( |_ ` x ) ) ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) <_ ( ( log ` x ) + 1 ) )
48 47 adantl 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( log ` ( ! ` ( |_ ` x ) ) ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) <_ ( ( log ` x ) + 1 ) )
49 43 recnd 
 |-  ( ( T. /\ x e. RR+ ) -> ( log ` ( ! ` ( |_ ` x ) ) ) e. CC )
50 49 adantrr 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` ( ! ` ( |_ ` x ) ) ) e. CC )
51 7 ad2antrl 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x e. CC /\ x =/= 0 ) )
52 51 simpld 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. CC )
53 5 adantrr 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` x ) e. CC )
54 subcl 
 |-  ( ( ( log ` x ) e. CC /\ 1 e. CC ) -> ( ( log ` x ) - 1 ) e. CC )
55 53 25 54 sylancl 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) - 1 ) e. CC )
56 52 55 mulcld 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x x. ( ( log ` x ) - 1 ) ) e. CC )
57 50 56 subcld 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` ( ! ` ( |_ ` x ) ) ) - ( x x. ( ( log ` x ) - 1 ) ) ) e. CC )
58 57 abscld 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( log ` ( ! ` ( |_ ` x ) ) ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) e. RR )
59 4 adantrr 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` x ) e. RR )
60 59 32 syl 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) + 1 ) e. RR )
61 rpregt0 
 |-  ( x e. RR+ -> ( x e. RR /\ 0 < x ) )
62 61 ad2antrl 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x e. RR /\ 0 < x ) )
63 lediv1 
 |-  ( ( ( abs ` ( ( log ` ( ! ` ( |_ ` x ) ) ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) e. RR /\ ( ( log ` x ) + 1 ) e. RR /\ ( x e. RR /\ 0 < x ) ) -> ( ( abs ` ( ( log ` ( ! ` ( |_ ` x ) ) ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) <_ ( ( log ` x ) + 1 ) <-> ( ( abs ` ( ( log ` ( ! ` ( |_ ` x ) ) ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) / x ) <_ ( ( ( log ` x ) + 1 ) / x ) ) )
64 58 60 62 63 syl3anc 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( abs ` ( ( log ` ( ! ` ( |_ ` x ) ) ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) <_ ( ( log ` x ) + 1 ) <-> ( ( abs ` ( ( log ` ( ! ` ( |_ ` x ) ) ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) / x ) <_ ( ( ( log ` x ) + 1 ) / x ) ) )
65 48 64 mpbid 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( abs ` ( ( log ` ( ! ` ( |_ ` x ) ) ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) / x ) <_ ( ( ( log ` x ) + 1 ) / x ) )
66 51 simprd 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> x =/= 0 )
67 55 52 66 divcan3d 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( x x. ( ( log ` x ) - 1 ) ) / x ) = ( ( log ` x ) - 1 ) )
68 67 oveq1d 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( x x. ( ( log ` x ) - 1 ) ) / x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) = ( ( ( log ` x ) - 1 ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) )
69 divsubdir 
 |-  ( ( ( x x. ( ( log ` x ) - 1 ) ) e. CC /\ ( log ` ( ! ` ( |_ ` x ) ) ) e. CC /\ ( x e. CC /\ x =/= 0 ) ) -> ( ( ( x x. ( ( log ` x ) - 1 ) ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) = ( ( ( x x. ( ( log ` x ) - 1 ) ) / x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) )
70 56 50 51 69 syl3anc 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( x x. ( ( log ` x ) - 1 ) ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) = ( ( ( x x. ( ( log ` x ) - 1 ) ) / x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) )
71 45 adantrr 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) e. CC )
72 1cnd 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 e. CC )
73 53 71 72 sub32d 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) - 1 ) = ( ( ( log ` x ) - 1 ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) )
74 68 70 73 3eqtr4rd 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) - 1 ) = ( ( ( x x. ( ( log ` x ) - 1 ) ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) )
75 74 fveq2d 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) - 1 ) ) = ( abs ` ( ( ( x x. ( ( log ` x ) - 1 ) ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) ) )
76 56 50 subcld 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( x x. ( ( log ` x ) - 1 ) ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) e. CC )
77 76 52 66 absdivd 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( x x. ( ( log ` x ) - 1 ) ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) / x ) ) = ( ( abs ` ( ( x x. ( ( log ` x ) - 1 ) ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) ) / ( abs ` x ) ) )
78 56 50 abssubd 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( x x. ( ( log ` x ) - 1 ) ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) ) = ( abs ` ( ( log ` ( ! ` ( |_ ` x ) ) ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) )
79 36 ad2antrl 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( x e. RR /\ 0 <_ x ) )
80 absid 
 |-  ( ( x e. RR /\ 0 <_ x ) -> ( abs ` x ) = x )
81 79 80 syl 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` x ) = x )
82 78 81 oveq12d 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( abs ` ( ( x x. ( ( log ` x ) - 1 ) ) - ( log ` ( ! ` ( |_ ` x ) ) ) ) ) / ( abs ` x ) ) = ( ( abs ` ( ( log ` ( ! ` ( |_ ` x ) ) ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) / x ) )
83 75 77 82 3eqtrd 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) - 1 ) ) = ( ( abs ` ( ( log ` ( ! ` ( |_ ` x ) ) ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) / x ) )
84 35 adantrr 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( log ` x ) + 1 ) / x ) e. CC )
85 84 subid1d 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( ( log ` x ) + 1 ) / x ) - 0 ) = ( ( ( log ` x ) + 1 ) / x ) )
86 85 fveq2d 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( ( log ` x ) + 1 ) / x ) - 0 ) ) = ( abs ` ( ( ( log ` x ) + 1 ) / x ) ) )
87 log1 
 |-  ( log ` 1 ) = 0
88 simprr 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ x )
89 12 adantrr 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR+ )
90 logleb 
 |-  ( ( 1 e. RR+ /\ x e. RR+ ) -> ( 1 <_ x <-> ( log ` 1 ) <_ ( log ` x ) ) )
91 21 89 90 sylancr 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 <_ x <-> ( log ` 1 ) <_ ( log ` x ) ) )
92 88 91 mpbid 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` 1 ) <_ ( log ` x ) )
93 87 92 eqbrtrrid 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 <_ ( log ` x ) )
94 59 93 ge0p1rpd 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( log ` x ) + 1 ) e. RR+ )
95 94 89 rpdivcld 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( ( ( log ` x ) + 1 ) / x ) e. RR+ )
96 rprege0 
 |-  ( ( ( ( log ` x ) + 1 ) / x ) e. RR+ -> ( ( ( ( log ` x ) + 1 ) / x ) e. RR /\ 0 <_ ( ( ( log ` x ) + 1 ) / x ) ) )
97 absid 
 |-  ( ( ( ( ( log ` x ) + 1 ) / x ) e. RR /\ 0 <_ ( ( ( log ` x ) + 1 ) / x ) ) -> ( abs ` ( ( ( log ` x ) + 1 ) / x ) ) = ( ( ( log ` x ) + 1 ) / x ) )
98 95 96 97 3syl 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( log ` x ) + 1 ) / x ) ) = ( ( ( log ` x ) + 1 ) / x ) )
99 86 98 eqtrd 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( ( log ` x ) + 1 ) / x ) - 0 ) ) = ( ( ( log ` x ) + 1 ) / x ) )
100 65 83 99 3brtr4d 
 |-  ( ( T. /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( abs ` ( ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) - 1 ) ) <_ ( abs ` ( ( ( ( log ` x ) + 1 ) / x ) - 0 ) ) )
101 1 2 31 35 46 100 rlimsqzlem 
 |-  ( T. -> ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ~~>r 1 )
102 101 mptru 
 |-  ( x e. RR+ |-> ( ( log ` x ) - ( ( log ` ( ! ` ( |_ ` x ) ) ) / x ) ) ) ~~>r 1