# 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}\in {ℝ}^{+}\to \frac{1}{{A}+1}\le \mathrm{log}\left({A}+1\right)-\mathrm{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↔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}}↔\mathrm{log}{\mathrm{e}}^{\frac{1}{{A}+1}}\le \mathrm{log}\left(\frac{{A}+1}{{A}}\right)\right)$
35 31 34 mpbid ${⊢}{A}\in {ℝ}^{+}\to \mathrm{log}{\mathrm{e}}^{\frac{1}{{A}+1}}\le \mathrm{log}\left(\frac{{A}+1}{{A}}\right)$
36 4 relogefd ${⊢}{A}\in {ℝ}^{+}\to \mathrm{log}{\mathrm{e}}^{\frac{1}{{A}+1}}=\frac{1}{{A}+1}$
37 3 9 relogdivd ${⊢}{A}\in {ℝ}^{+}\to \mathrm{log}\left(\frac{{A}+1}{{A}}\right)=\mathrm{log}\left({A}+1\right)-\mathrm{log}{A}$
38 35 36 37 3brtr3d ${⊢}{A}\in {ℝ}^{+}\to \frac{1}{{A}+1}\le \mathrm{log}\left({A}+1\right)-\mathrm{log}{A}$