Metamath Proof Explorer


Theorem logdifbnd

Description: Bound on the difference of logs. (Contributed by Mario Carneiro, 23-May-2016)

Ref Expression
Assertion logdifbnd
|- ( A e. RR+ -> ( ( log ` ( A + 1 ) ) - ( log ` A ) ) <_ ( 1 / A ) )

Proof

Step Hyp Ref Expression
1 rpcn
 |-  ( A e. RR+ -> A e. CC )
2 1cnd
 |-  ( A e. RR+ -> 1 e. CC )
3 rpne0
 |-  ( A e. RR+ -> A =/= 0 )
4 1 2 1 3 divdird
 |-  ( A e. RR+ -> ( ( A + 1 ) / A ) = ( ( A / A ) + ( 1 / A ) ) )
5 1 3 dividd
 |-  ( A e. RR+ -> ( A / A ) = 1 )
6 5 oveq1d
 |-  ( A e. RR+ -> ( ( A / A ) + ( 1 / A ) ) = ( 1 + ( 1 / A ) ) )
7 4 6 eqtr2d
 |-  ( A e. RR+ -> ( 1 + ( 1 / A ) ) = ( ( A + 1 ) / A ) )
8 7 fveq2d
 |-  ( A e. RR+ -> ( log ` ( 1 + ( 1 / A ) ) ) = ( log ` ( ( A + 1 ) / A ) ) )
9 1rp
 |-  1 e. RR+
10 rpaddcl
 |-  ( ( A e. RR+ /\ 1 e. RR+ ) -> ( A + 1 ) e. RR+ )
11 9 10 mpan2
 |-  ( A e. RR+ -> ( A + 1 ) e. RR+ )
12 relogdiv
 |-  ( ( ( A + 1 ) e. RR+ /\ A e. RR+ ) -> ( log ` ( ( A + 1 ) / A ) ) = ( ( log ` ( A + 1 ) ) - ( log ` A ) ) )
13 11 12 mpancom
 |-  ( A e. RR+ -> ( log ` ( ( A + 1 ) / A ) ) = ( ( log ` ( A + 1 ) ) - ( log ` A ) ) )
14 8 13 eqtrd
 |-  ( A e. RR+ -> ( log ` ( 1 + ( 1 / A ) ) ) = ( ( log ` ( A + 1 ) ) - ( log ` A ) ) )
15 rpreccl
 |-  ( A e. RR+ -> ( 1 / A ) e. RR+ )
16 rpaddcl
 |-  ( ( 1 e. RR+ /\ ( 1 / A ) e. RR+ ) -> ( 1 + ( 1 / A ) ) e. RR+ )
17 9 15 16 sylancr
 |-  ( A e. RR+ -> ( 1 + ( 1 / A ) ) e. RR+ )
18 17 reeflogd
 |-  ( A e. RR+ -> ( exp ` ( log ` ( 1 + ( 1 / A ) ) ) ) = ( 1 + ( 1 / A ) ) )
19 17 rpred
 |-  ( A e. RR+ -> ( 1 + ( 1 / A ) ) e. RR )
20 15 rpred
 |-  ( A e. RR+ -> ( 1 / A ) e. RR )
21 20 reefcld
 |-  ( A e. RR+ -> ( exp ` ( 1 / A ) ) e. RR )
22 efgt1p
 |-  ( ( 1 / A ) e. RR+ -> ( 1 + ( 1 / A ) ) < ( exp ` ( 1 / A ) ) )
23 15 22 syl
 |-  ( A e. RR+ -> ( 1 + ( 1 / A ) ) < ( exp ` ( 1 / A ) ) )
24 19 21 23 ltled
 |-  ( A e. RR+ -> ( 1 + ( 1 / A ) ) <_ ( exp ` ( 1 / A ) ) )
25 18 24 eqbrtrd
 |-  ( A e. RR+ -> ( exp ` ( log ` ( 1 + ( 1 / A ) ) ) ) <_ ( exp ` ( 1 / A ) ) )
26 relogcl
 |-  ( ( A + 1 ) e. RR+ -> ( log ` ( A + 1 ) ) e. RR )
27 11 26 syl
 |-  ( A e. RR+ -> ( log ` ( A + 1 ) ) e. RR )
28 relogcl
 |-  ( A e. RR+ -> ( log ` A ) e. RR )
29 27 28 resubcld
 |-  ( A e. RR+ -> ( ( log ` ( A + 1 ) ) - ( log ` A ) ) e. RR )
30 14 29 eqeltrd
 |-  ( A e. RR+ -> ( log ` ( 1 + ( 1 / A ) ) ) e. RR )
31 efle
 |-  ( ( ( log ` ( 1 + ( 1 / A ) ) ) e. RR /\ ( 1 / A ) e. RR ) -> ( ( log ` ( 1 + ( 1 / A ) ) ) <_ ( 1 / A ) <-> ( exp ` ( log ` ( 1 + ( 1 / A ) ) ) ) <_ ( exp ` ( 1 / A ) ) ) )
32 30 20 31 syl2anc
 |-  ( A e. RR+ -> ( ( log ` ( 1 + ( 1 / A ) ) ) <_ ( 1 / A ) <-> ( exp ` ( log ` ( 1 + ( 1 / A ) ) ) ) <_ ( exp ` ( 1 / A ) ) ) )
33 25 32 mpbird
 |-  ( A e. RR+ -> ( log ` ( 1 + ( 1 / A ) ) ) <_ ( 1 / A ) )
34 14 33 eqbrtrrd
 |-  ( A e. RR+ -> ( ( log ` ( A + 1 ) ) - ( log ` A ) ) <_ ( 1 / A ) )