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 ) )