# 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+ )`
` |-  ( A e. RR+ -> 1 < ( A + 1 ) )`
` |-  ( A e. RR+ -> ( A + 1 ) e. RR )`
12 11 recnd
` |-  ( A e. RR+ -> ( A + 1 ) e. CC )`
13 12 mulid1d
` |-  ( 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 ) ) )`