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