This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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