Metamath Proof Explorer

Theorem logfacbnd3

Description: Show the stronger statement log ( x ! ) = x log x - x + O ( log x ) alluded to in logfacrlim . (Contributed by Mario Carneiro, 20-May-2016)

Ref Expression
Assertion logfacbnd3 
|- ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) <_ ( ( log ` A ) + 1 ) )

Proof

Step Hyp Ref Expression
1 simpl 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> A e. RR+ )
2 1 rprege0d 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( A e. RR /\ 0 <_ A ) )
3 flge0nn0 
 |-  ( ( A e. RR /\ 0 <_ A ) -> ( |_ ` A ) e. NN0 )
4 2 3 syl 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( |_ ` A ) e. NN0 )
5 4 faccld 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( ! ` ( |_ ` A ) ) e. NN )
6 5 nnrpd 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( ! ` ( |_ ` A ) ) e. RR+ )
7 relogcl 
 |-  ( ( ! ` ( |_ ` A ) ) e. RR+ -> ( log ` ( ! ` ( |_ ` A ) ) ) e. RR )
8 6 7 syl 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( log ` ( ! ` ( |_ ` A ) ) ) e. RR )
9 rpre 
 |-  ( A e. RR+ -> A e. RR )
10 9 adantr 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> A e. RR )
11 relogcl 
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
12 11 adantr 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( log ` A ) e. RR )
13 peano2rem 
 |-  ( ( log ` A ) e. RR -> ( ( log ` A ) - 1 ) e. RR )
14 12 13 syl 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( ( log ` A ) - 1 ) e. RR )
15 10 14 remulcld 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( A x. ( ( log ` A ) - 1 ) ) e. RR )
16 8 15 resubcld 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) e. RR )
17 16 recnd 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) e. CC )
18 17 abscld 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) e. RR )
19 peano2rem 
 |-  ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) e. RR -> ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - 1 ) e. RR )
20 18 19 syl 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - 1 ) e. RR )
21 ax-1cn 
 |-  1 e. CC
22 subcl 
 |-  ( ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) e. CC /\ 1 e. CC ) -> ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) e. CC )
23 17 21 22 sylancl 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) e. CC )
24 23 abscld 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) ) e. RR )
25 abs1 
 |-  ( abs ` 1 ) = 1
26 25 oveq2i 
 |-  ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - ( abs ` 1 ) ) = ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - 1 )
27 abs2dif 
 |-  ( ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) e. CC /\ 1 e. CC ) -> ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - ( abs ` 1 ) ) <_ ( abs ` ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) ) )
28 17 21 27 sylancl 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - ( abs ` 1 ) ) <_ ( abs ` ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) ) )
29 26 28 eqbrtrrid 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - 1 ) <_ ( abs ` ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) ) )
30 fveq2 
 |-  ( x = A -> ( |_ ` x ) = ( |_ ` A ) )
31 30 oveq2d 
 |-  ( x = A -> ( 1 ... ( |_ ` x ) ) = ( 1 ... ( |_ ` A ) ) )
32 31 sumeq1d 
 |-  ( x = A -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) )
33 id 
 |-  ( x = A -> x = A )
34 fveq2 
 |-  ( x = A -> ( log ` x ) = ( log ` A ) )
35 34 oveq1d 
 |-  ( x = A -> ( ( log ` x ) - 1 ) = ( ( log ` A ) - 1 ) )
36 33 35 oveq12d 
 |-  ( x = A -> ( x x. ( ( log ` x ) - 1 ) ) = ( A x. ( ( log ` A ) - 1 ) ) )
37 32 36 oveq12d 
 |-  ( x = A -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) - ( A x. ( ( log ` A ) - 1 ) ) ) )
38 eqid 
 |-  ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) = ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) )
39 ovex 
 |-  ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) e. _V
40 37 38 39 fvmpt3i 
 |-  ( A e. RR+ -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` A ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) - ( A x. ( ( log ` A ) - 1 ) ) ) )
41 40 adantr 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` A ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) - ( A x. ( ( log ` A ) - 1 ) ) ) )
42 logfac 
 |-  ( ( |_ ` A ) e. NN0 -> ( log ` ( ! ` ( |_ ` A ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) )
43 4 42 syl 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( log ` ( ! ` ( |_ ` A ) ) ) = sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) )
44 43 oveq1d 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) = ( sum_ n e. ( 1 ... ( |_ ` A ) ) ( log ` n ) - ( A x. ( ( log ` A ) - 1 ) ) ) )
45 41 44 eqtr4d 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` A ) = ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) )
46 1rp 
 |-  1 e. RR+
47 fveq2 
 |-  ( x = 1 -> ( |_ ` x ) = ( |_ ` 1 ) )
48 1z 
 |-  1 e. ZZ
49 flid 
 |-  ( 1 e. ZZ -> ( |_ ` 1 ) = 1 )
50 48 49 ax-mp 
 |-  ( |_ ` 1 ) = 1
51 47 50 eqtrdi 
 |-  ( x = 1 -> ( |_ ` x ) = 1 )
52 51 oveq2d 
 |-  ( x = 1 -> ( 1 ... ( |_ ` x ) ) = ( 1 ... 1 ) )
53 52 sumeq1d 
 |-  ( x = 1 -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) = sum_ n e. ( 1 ... 1 ) ( log ` n ) )
54 0cn 
 |-  0 e. CC
55 fveq2 
 |-  ( n = 1 -> ( log ` n ) = ( log ` 1 ) )
56 log1 
 |-  ( log ` 1 ) = 0
57 55 56 eqtrdi 
 |-  ( n = 1 -> ( log ` n ) = 0 )
58 57 fsum1 
 |-  ( ( 1 e. ZZ /\ 0 e. CC ) -> sum_ n e. ( 1 ... 1 ) ( log ` n ) = 0 )
59 48 54 58 mp2an 
 |-  sum_ n e. ( 1 ... 1 ) ( log ` n ) = 0
60 53 59 eqtrdi 
 |-  ( x = 1 -> sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) = 0 )
61 id 
 |-  ( x = 1 -> x = 1 )
62 fveq2 
 |-  ( x = 1 -> ( log ` x ) = ( log ` 1 ) )
63 62 56 eqtrdi 
 |-  ( x = 1 -> ( log ` x ) = 0 )
64 63 oveq1d 
 |-  ( x = 1 -> ( ( log ` x ) - 1 ) = ( 0 - 1 ) )
65 61 64 oveq12d 
 |-  ( x = 1 -> ( x x. ( ( log ` x ) - 1 ) ) = ( 1 x. ( 0 - 1 ) ) )
66 54 21 subcli 
 |-  ( 0 - 1 ) e. CC
67 66 mulid2i 
 |-  ( 1 x. ( 0 - 1 ) ) = ( 0 - 1 )
68 65 67 eqtrdi 
 |-  ( x = 1 -> ( x x. ( ( log ` x ) - 1 ) ) = ( 0 - 1 ) )
69 60 68 oveq12d 
 |-  ( x = 1 -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) = ( 0 - ( 0 - 1 ) ) )
70 nncan 
 |-  ( ( 0 e. CC /\ 1 e. CC ) -> ( 0 - ( 0 - 1 ) ) = 1 )
71 54 21 70 mp2an 
 |-  ( 0 - ( 0 - 1 ) ) = 1
72 69 71 eqtrdi 
 |-  ( x = 1 -> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) = 1 )
73 72 38 39 fvmpt3i 
 |-  ( 1 e. RR+ -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` 1 ) = 1 )
74 46 73 mp1i 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` 1 ) = 1 )
75 45 74 oveq12d 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` A ) - ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` 1 ) ) = ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) )
76 75 fveq2d 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` A ) - ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` 1 ) ) ) = ( abs ` ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) ) )
77 ioorp 
 |-  ( 0 (,) +oo ) = RR+
78 77 eqcomi 
 |-  RR+ = ( 0 (,) +oo )
79 nnuz 
 |-  NN = ( ZZ>= ` 1 )
80 48 a1i 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> 1 e. ZZ )
81 1re 
 |-  1 e. RR
82 81 a1i 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> 1 e. RR )
83 pnfxr 
 |-  +oo e. RR*
84 83 a1i 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> +oo e. RR* )
85 1nn0 
 |-  1 e. NN0
86 81 85 nn0addge1i 
 |-  1 <_ ( 1 + 1 )
87 86 a1i 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> 1 <_ ( 1 + 1 ) )
88 0red 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> 0 e. RR )
89 rpre 
 |-  ( x e. RR+ -> x e. RR )
90 89 adantl 
 |-  ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> x e. RR )
91 relogcl 
 |-  ( x e. RR+ -> ( log ` x ) e. RR )
92 91 adantl 
 |-  ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( log ` x ) e. RR )
93 peano2rem 
 |-  ( ( log ` x ) e. RR -> ( ( log ` x ) - 1 ) e. RR )
94 92 93 syl 
 |-  ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( ( log ` x ) - 1 ) e. RR )
95 90 94 remulcld 
 |-  ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. RR+ ) -> ( x x. ( ( log ` x ) - 1 ) ) e. RR )
96 nnrp 
 |-  ( x e. NN -> x e. RR+ )
97 96 92 sylan2 
 |-  ( ( ( A e. RR+ /\ 1 <_ A ) /\ x e. NN ) -> ( log ` x ) e. RR )
98 advlog 
 |-  ( RR _D ( x e. RR+ |-> ( x x. ( ( log ` x ) - 1 ) ) ) ) = ( x e. RR+ |-> ( log ` x ) )
99 98 a1i 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( RR _D ( x e. RR+ |-> ( x x. ( ( log ` x ) - 1 ) ) ) ) = ( x e. RR+ |-> ( log ` x ) ) )
100 fveq2 
 |-  ( x = n -> ( log ` x ) = ( log ` n ) )
101 simp32 
 |-  ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> x <_ n )
102 logleb 
 |-  ( ( x e. RR+ /\ n e. RR+ ) -> ( x <_ n <-> ( log ` x ) <_ ( log ` n ) ) )
103 102 3ad2ant2 
 |-  ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> ( x <_ n <-> ( log ` x ) <_ ( log ` n ) ) )
104 101 103 mpbid 
 |-  ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ n e. RR+ ) /\ ( 1 <_ x /\ x <_ n /\ n <_ +oo ) ) -> ( log ` x ) <_ ( log ` n ) )
105 simprr 
 |-  ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> 1 <_ x )
106 simprl 
 |-  ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> x e. RR+ )
107 logleb 
 |-  ( ( 1 e. RR+ /\ x e. RR+ ) -> ( 1 <_ x <-> ( log ` 1 ) <_ ( log ` x ) ) )
108 46 106 107 sylancr 
 |-  ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( 1 <_ x <-> ( log ` 1 ) <_ ( log ` x ) ) )
109 105 108 mpbid 
 |-  ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> ( log ` 1 ) <_ ( log ` x ) )
110 56 109 eqbrtrrid 
 |-  ( ( ( A e. RR+ /\ 1 <_ A ) /\ ( x e. RR+ /\ 1 <_ x ) ) -> 0 <_ ( log ` x ) )
111 46 a1i 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> 1 e. RR+ )
112 1le1 
 |-  1 <_ 1
113 112 a1i 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> 1 <_ 1 )
114 simpr 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> 1 <_ A )
115 10 rexrd 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> A e. RR* )
116 pnfge 
 |-  ( A e. RR* -> A <_ +oo )
117 115 116 syl 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> A <_ +oo )
118 78 79 80 82 84 87 88 95 92 97 99 100 104 38 110 111 1 113 114 117 34 dvfsum2 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` A ) - ( ( x e. RR+ |-> ( sum_ n e. ( 1 ... ( |_ ` x ) ) ( log ` n ) - ( x x. ( ( log ` x ) - 1 ) ) ) ) ` 1 ) ) ) <_ ( log ` A ) )
119 76 118 eqbrtrrd 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) - 1 ) ) <_ ( log ` A ) )
120 20 24 12 29 119 letrd 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - 1 ) <_ ( log ` A ) )
121 18 82 12 lesubaddd 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( ( ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) - 1 ) <_ ( log ` A ) <-> ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) <_ ( ( log ` A ) + 1 ) ) )
122 120 121 mpbid 
 |-  ( ( A e. RR+ /\ 1 <_ A ) -> ( abs ` ( ( log ` ( ! ` ( |_ ` A ) ) ) - ( A x. ( ( log ` A ) - 1 ) ) ) ) <_ ( ( log ` A ) + 1 ) )