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

Metamath Proof Explorer

Theorem logdiflbnd

Description: Lower bound on the difference of logs. (Contributed by Mario Carneiro, 3-Jul-2017)

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

Proof

Step Hyp Ref Expression
1 rpre 
 |-  ( A e. RR+ -> A e. RR )
2 rpge0 
 |-  ( A e. RR+ -> 0 <_ A )
3 1 2 ge0p1rpd 
 |-  ( A e. RR+ -> ( A + 1 ) e. RR+ )
4 3 rprecred 
 |-  ( A e. RR+ -> ( 1 / ( A + 1 ) ) e. RR )
5 1red 
 |-  ( A e. RR+ -> 1 e. RR )
6 0le1 
 |-  0 <_ 1
7 6 a1i 
 |-  ( A e. RR+ -> 0 <_ 1 )
8 5 3 7 divge0d 
 |-  ( A e. RR+ -> 0 <_ ( 1 / ( A + 1 ) ) )
9 id 
 |-  ( A e. RR+ -> A e. RR+ )
10 5 9 ltaddrp2d 
 |-  ( A e. RR+ -> 1 < ( A + 1 ) )
11 1 5 readdcld 
 |-  ( A e. RR+ -> ( A + 1 ) e. RR )
12 11 recnd 
 |-  ( A e. RR+ -> ( A + 1 ) e. CC )
13 12 mulridd 
 |-  ( A e. RR+ -> ( ( A + 1 ) x. 1 ) = ( A + 1 ) )
14 10 13 breqtrrd 
 |-  ( A e. RR+ -> 1 < ( ( A + 1 ) x. 1 ) )
15 5 5 3 ltdivmuld 
 |-  ( A e. RR+ -> ( ( 1 / ( A + 1 ) ) < 1 <-> 1 < ( ( A + 1 ) x. 1 ) ) )
16 14 15 mpbird 
 |-  ( A e. RR+ -> ( 1 / ( A + 1 ) ) < 1 )
17 4 8 16 eflegeo 
 |-  ( A e. RR+ -> ( exp ` ( 1 / ( A + 1 ) ) ) <_ ( 1 / ( 1 - ( 1 / ( A + 1 ) ) ) ) )
18 5 recnd 
 |-  ( A e. RR+ -> 1 e. CC )
19 3 rpne0d 
 |-  ( A e. RR+ -> ( A + 1 ) =/= 0 )
20 12 18 12 19 divsubdird 
 |-  ( A e. RR+ -> ( ( ( A + 1 ) - 1 ) / ( A + 1 ) ) = ( ( ( A + 1 ) / ( A + 1 ) ) - ( 1 / ( A + 1 ) ) ) )
21 1 recnd 
 |-  ( A e. RR+ -> A e. CC )
22 21 18 pncand 
 |-  ( A e. RR+ -> ( ( A + 1 ) - 1 ) = A )
23 22 oveq1d 
 |-  ( A e. RR+ -> ( ( ( A + 1 ) - 1 ) / ( A + 1 ) ) = ( A / ( A + 1 ) ) )
24 12 19 dividd 
 |-  ( A e. RR+ -> ( ( A + 1 ) / ( A + 1 ) ) = 1 )
25 24 oveq1d 
 |-  ( A e. RR+ -> ( ( ( A + 1 ) / ( A + 1 ) ) - ( 1 / ( A + 1 ) ) ) = ( 1 - ( 1 / ( A + 1 ) ) ) )
26 20 23 25 3eqtr3rd 
 |-  ( A e. RR+ -> ( 1 - ( 1 / ( A + 1 ) ) ) = ( A / ( A + 1 ) ) )
27 26 oveq2d 
 |-  ( A e. RR+ -> ( 1 / ( 1 - ( 1 / ( A + 1 ) ) ) ) = ( 1 / ( A / ( A + 1 ) ) ) )
28 rpne0 
 |-  ( A e. RR+ -> A =/= 0 )
29 21 12 28 19 recdivd 
 |-  ( A e. RR+ -> ( 1 / ( A / ( A + 1 ) ) ) = ( ( A + 1 ) / A ) )
30 27 29 eqtrd 
 |-  ( A e. RR+ -> ( 1 / ( 1 - ( 1 / ( A + 1 ) ) ) ) = ( ( A + 1 ) / A ) )
31 17 30 breqtrd 
 |-  ( A e. RR+ -> ( exp ` ( 1 / ( A + 1 ) ) ) <_ ( ( A + 1 ) / A ) )
32 4 rpefcld 
 |-  ( A e. RR+ -> ( exp ` ( 1 / ( A + 1 ) ) ) e. RR+ )
33 3 9 rpdivcld 
 |-  ( A e. RR+ -> ( ( A + 1 ) / A ) e. RR+ )
34 32 33 logled 
 |-  ( A e. RR+ -> ( ( exp ` ( 1 / ( A + 1 ) ) ) <_ ( ( A + 1 ) / A ) <-> ( log ` ( exp ` ( 1 / ( A + 1 ) ) ) ) <_ ( log ` ( ( A + 1 ) / A ) ) ) )
35 31 34 mpbid 
 |-  ( A e. RR+ -> ( log ` ( exp ` ( 1 / ( A + 1 ) ) ) ) <_ ( log ` ( ( A + 1 ) / A ) ) )
36 4 relogefd 
 |-  ( A e. RR+ -> ( log ` ( exp ` ( 1 / ( A + 1 ) ) ) ) = ( 1 / ( A + 1 ) ) )
37 3 9 relogdivd 
 |-  ( A e. RR+ -> ( log ` ( ( A + 1 ) / A ) ) = ( ( log ` ( A + 1 ) ) - ( log ` A ) ) )
38 35 36 37 3brtr3d 
 |-  ( A e. RR+ -> ( 1 / ( A + 1 ) ) <_ ( ( log ` ( A + 1 ) ) - ( log ` A ) ) )