Theorem logdiflbnd

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

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

Proof

Step	Hyp	Ref	Expression
1		rpre	$$⊢A\in {ℝ}^{+}\to A\in ℝ$$
2		rpge0	$$⊢A\in {ℝ}^{+}\to 0\le A$$
3	1 2	ge0p1rpd	$$⊢A\in {ℝ}^{+}\to A+1\in {ℝ}^{+}$$
4	3	rprecred	$$⊢A\in {ℝ}^{+}\to \frac{1}{A+1}\in ℝ$$
5		1red	$$⊢A\in {ℝ}^{+}\to 1\in ℝ$$
6		0le1	$$⊢0\le 1$$
7	6	a1i	$$⊢A\in {ℝ}^{+}\to 0\le 1$$
8	5 3 7	divge0d	$$⊢A\in {ℝ}^{+}\to 0\le \frac{1}{A+1}$$
9		id	$$⊢A\in {ℝ}^{+}\to A\in {ℝ}^{+}$$
10	5 9	ltaddrp2d	$$⊢A\in {ℝ}^{+}\to 1<A+1$$
11	1 5	readdcld	$$⊢A\in {ℝ}^{+}\to A+1\in ℝ$$
12	11	recnd	$$⊢A\in {ℝ}^{+}\to A+1\in ℂ$$
13	12	mulid1d	$$⊢A\in {ℝ}^{+}\to \left(A+1\right)\cdot 1=A+1$$
14	10 13	breqtrrd	$$⊢A\in {ℝ}^{+}\to 1<\left(A+1\right)\cdot 1$$
15	5 5 3	ltdivmuld	$$⊢A\in {ℝ}^{+}\to \left(\frac{1}{A+1}<1\leftrightarrow 1<\left(A+1\right)\cdot 1\right)$$
16	14 15	mpbird	$$⊢A\in {ℝ}^{+}\to \frac{1}{A+1}<1$$
17	4 8 16	eflegeo	$$⊢A\in {ℝ}^{+}\to {\mathrm{e}}^{\frac{1}{A+1}}\le \frac{1}{1-\left(\frac{1}{A+1}\right)}$$
18	5	recnd	$$⊢A\in {ℝ}^{+}\to 1\in ℂ$$
19	3	rpne0d	$$⊢A\in {ℝ}^{+}\to A+1\ne 0$$
20	12 18 12 19	divsubdird	$$⊢A\in {ℝ}^{+}\to \frac{A+1-1}{A+1}=\left(\frac{A+1}{A+1}\right)-\left(\frac{1}{A+1}\right)$$
21	1	recnd	$$⊢A\in {ℝ}^{+}\to A\in ℂ$$
22	21 18	pncand	$$⊢A\in {ℝ}^{+}\to A+1-1=A$$
23	22	oveq1d	$$⊢A\in {ℝ}^{+}\to \frac{A+1-1}{A+1}=\frac{A}{A+1}$$
24	12 19	dividd	$$⊢A\in {ℝ}^{+}\to \frac{A+1}{A+1}=1$$
25	24	oveq1d	$$⊢A\in {ℝ}^{+}\to \left(\frac{A+1}{A+1}\right)-\left(\frac{1}{A+1}\right)=1-\left(\frac{1}{A+1}\right)$$
26	20 23 25	3eqtr3rd	$$⊢A\in {ℝ}^{+}\to 1-\left(\frac{1}{A+1}\right)=\frac{A}{A+1}$$
27	26	oveq2d	$$⊢A\in {ℝ}^{+}\to \frac{1}{1-\left(\frac{1}{A+1}\right)}=\frac{1}{\frac{A}{A+1}}$$
28		rpne0	$$⊢A\in {ℝ}^{+}\to A\ne 0$$
29	21 12 28 19	recdivd	$$⊢A\in {ℝ}^{+}\to \frac{1}{\frac{A}{A+1}}=\frac{A+1}{A}$$
30	27 29	eqtrd	$$⊢A\in {ℝ}^{+}\to \frac{1}{1-\left(\frac{1}{A+1}\right)}=\frac{A+1}{A}$$
31	17 30	breqtrd	$$⊢A\in {ℝ}^{+}\to {\mathrm{e}}^{\frac{1}{A+1}}\le \frac{A+1}{A}$$
32	4	rpefcld	$$⊢A\in {ℝ}^{+}\to {\mathrm{e}}^{\frac{1}{A+1}}\in {ℝ}^{+}$$
33	3 9	rpdivcld	$$⊢A\in {ℝ}^{+}\to \frac{A+1}{A}\in {ℝ}^{+}$$
34	32 33	logled	$$⊢A\in {ℝ}^{+}\to \left({\mathrm{e}}^{\frac{1}{A+1}}\le \frac{A+1}{A}\leftrightarrow \log {\mathrm{e}}^{\frac{1}{A+1}}\le \log \left(\frac{A+1}{A}\right)\right)$$
35	31 34	mpbid	$$⊢A\in {ℝ}^{+}\to \log {\mathrm{e}}^{\frac{1}{A+1}}\le \log \left(\frac{A+1}{A}\right)$$
36	4	relogefd	$$⊢A\in {ℝ}^{+}\to \log {\mathrm{e}}^{\frac{1}{A+1}}=\frac{1}{A+1}$$
37	3 9	relogdivd	$$⊢A\in {ℝ}^{+}\to \log \left(\frac{A+1}{A}\right)=\log \left(A+1\right)-\log A$$
38	35 36 37	3brtr3d	$$⊢A\in {ℝ}^{+}\to \frac{1}{A+1}\le \log \left(A+1\right)-\log A$$