Theorem logdifbnd

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

	Ref	Expression
Assertion	logdifbnd	$$⊢A\in {ℝ}^{+}\to \log \left(A+1\right)-\log A\le \frac{1}{A}$$

Proof

Step	Hyp	Ref	Expression
1		rpcn	$$⊢A\in {ℝ}^{+}\to A\in ℂ$$
2		1cnd	$$⊢A\in {ℝ}^{+}\to 1\in ℂ$$
3		rpne0	$$⊢A\in {ℝ}^{+}\to A\ne 0$$
4	1 2 1 3	divdird	$$⊢A\in {ℝ}^{+}\to \frac{A+1}{A}=\left(\frac{A}{A}\right)+\left(\frac{1}{A}\right)$$
5	1 3	dividd	$$⊢A\in {ℝ}^{+}\to \frac{A}{A}=1$$
6	5	oveq1d	$$⊢A\in {ℝ}^{+}\to \left(\frac{A}{A}\right)+\left(\frac{1}{A}\right)=1+\left(\frac{1}{A}\right)$$
7	4 6	eqtr2d	$$⊢A\in {ℝ}^{+}\to 1+\left(\frac{1}{A}\right)=\frac{A+1}{A}$$
8	7	fveq2d	$$⊢A\in {ℝ}^{+}\to \log \left(1+\left(\frac{1}{A}\right)\right)=\log \left(\frac{A+1}{A}\right)$$
9		1rp	$$⊢1\in {ℝ}^{+}$$
10		rpaddcl	$$⊢\left(A\in {ℝ}^{+}\wedge 1\in {ℝ}^{+}\right)\to A+1\in {ℝ}^{+}$$
11	9 10	mpan2	$$⊢A\in {ℝ}^{+}\to A+1\in {ℝ}^{+}$$
12		relogdiv	$$⊢\left(A+1\in {ℝ}^{+}\wedge A\in {ℝ}^{+}\right)\to \log \left(\frac{A+1}{A}\right)=\log \left(A+1\right)-\log A$$
13	11 12	mpancom	$$⊢A\in {ℝ}^{+}\to \log \left(\frac{A+1}{A}\right)=\log \left(A+1\right)-\log A$$
14	8 13	eqtrd	$$⊢A\in {ℝ}^{+}\to \log \left(1+\left(\frac{1}{A}\right)\right)=\log \left(A+1\right)-\log A$$
15		rpreccl	$$⊢A\in {ℝ}^{+}\to \frac{1}{A}\in {ℝ}^{+}$$
16		rpaddcl	$$⊢\left(1\in {ℝ}^{+}\wedge \frac{1}{A}\in {ℝ}^{+}\right)\to 1+\left(\frac{1}{A}\right)\in {ℝ}^{+}$$
17	9 15 16	sylancr	$$⊢A\in {ℝ}^{+}\to 1+\left(\frac{1}{A}\right)\in {ℝ}^{+}$$
18	17	reeflogd	$$⊢A\in {ℝ}^{+}\to {\mathrm{e}}^{\log \left(1+\left(\frac{1}{A}\right)\right)}=1+\left(\frac{1}{A}\right)$$
19	17	rpred	$$⊢A\in {ℝ}^{+}\to 1+\left(\frac{1}{A}\right)\in ℝ$$
20	15	rpred	$$⊢A\in {ℝ}^{+}\to \frac{1}{A}\in ℝ$$
21	20	reefcld	$$⊢A\in {ℝ}^{+}\to {\mathrm{e}}^{\frac{1}{A}}\in ℝ$$
22		efgt1p	$$⊢\frac{1}{A}\in {ℝ}^{+}\to 1+\left(\frac{1}{A}\right)<{\mathrm{e}}^{\frac{1}{A}}$$
23	15 22	syl	$$⊢A\in {ℝ}^{+}\to 1+\left(\frac{1}{A}\right)<{\mathrm{e}}^{\frac{1}{A}}$$
24	19 21 23	ltled	$$⊢A\in {ℝ}^{+}\to 1+\left(\frac{1}{A}\right)\le {\mathrm{e}}^{\frac{1}{A}}$$
25	18 24	eqbrtrd	$$⊢A\in {ℝ}^{+}\to {\mathrm{e}}^{\log \left(1+\left(\frac{1}{A}\right)\right)}\le {\mathrm{e}}^{\frac{1}{A}}$$
26		relogcl	$$⊢A+1\in {ℝ}^{+}\to \log \left(A+1\right)\in ℝ$$
27	11 26	syl	$$⊢A\in {ℝ}^{+}\to \log \left(A+1\right)\in ℝ$$
28		relogcl	$$⊢A\in {ℝ}^{+}\to \log A\in ℝ$$
29	27 28	resubcld	$$⊢A\in {ℝ}^{+}\to \log \left(A+1\right)-\log A\in ℝ$$
30	14 29	eqeltrd	$$⊢A\in {ℝ}^{+}\to \log \left(1+\left(\frac{1}{A}\right)\right)\in ℝ$$
31		efle	$$⊢\left(\log \left(1+\left(\frac{1}{A}\right)\right)\in ℝ\wedge \frac{1}{A}\in ℝ\right)\to \left(\log \left(1+\left(\frac{1}{A}\right)\right)\le \frac{1}{A}\leftrightarrow {\mathrm{e}}^{\log \left(1+\left(\frac{1}{A}\right)\right)}\le {\mathrm{e}}^{\frac{1}{A}}\right)$$
32	30 20 31	syl2anc	$$⊢A\in {ℝ}^{+}\to \left(\log \left(1+\left(\frac{1}{A}\right)\right)\le \frac{1}{A}\leftrightarrow {\mathrm{e}}^{\log \left(1+\left(\frac{1}{A}\right)\right)}\le {\mathrm{e}}^{\frac{1}{A}}\right)$$
33	25 32	mpbird	$$⊢A\in {ℝ}^{+}\to \log \left(1+\left(\frac{1}{A}\right)\right)\le \frac{1}{A}$$
34	14 33	eqbrtrrd	$$⊢A\in {ℝ}^{+}\to \log \left(A+1\right)-\log A\le \frac{1}{A}$$