logdifbnd

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

		Ref	Expression
	Assertion	logdifbnd	$⊢ A \in ℝ^{+} \to \log (A + 1) - \log A \leq \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 \neq 0$
4	1 2 1 3	divdird	$⊢ A \in ℝ^{+} \to \frac{A + 1}{A} = (\frac{A}{A}) + (\frac{1}{A})$
5	1 3	dividd	$⊢ A \in ℝ^{+} \to \frac{A}{A} = 1$
6	5	oveq1d	$⊢ A \in ℝ^{+} \to (\frac{A}{A}) + (\frac{1}{A}) = 1 + (\frac{1}{A})$
7	4 6	eqtr2d	$⊢ A \in ℝ^{+} \to 1 + (\frac{1}{A}) = \frac{A + 1}{A}$
8	7	fveq2d	$⊢ A \in ℝ^{+} \to \log (1 + (\frac{1}{A})) = \log (\frac{A + 1}{A})$
9		1rp	$⊢ 1 \in ℝ^{+}$
10		rpaddcl	$⊢ (A \in ℝ^{+} \land 1 \in ℝ^{+}) \to A + 1 \in ℝ^{+}$
11	9 10	mpan2	$⊢ A \in ℝ^{+} \to A + 1 \in ℝ^{+}$
12		relogdiv	$⊢ (A + 1 \in ℝ^{+} \land A \in ℝ^{+}) \to \log (\frac{A + 1}{A}) = \log (A + 1) - \log A$
13	11 12	mpancom	$⊢ A \in ℝ^{+} \to \log (\frac{A + 1}{A}) = \log (A + 1) - \log A$
14	8 13	eqtrd	$⊢ A \in ℝ^{+} \to \log (1 + (\frac{1}{A})) = \log (A + 1) - \log A$
15		rpreccl	$⊢ A \in ℝ^{+} \to \frac{1}{A} \in ℝ^{+}$
16		rpaddcl	$⊢ (1 \in ℝ^{+} \land \frac{1}{A} \in ℝ^{+}) \to 1 + (\frac{1}{A}) \in ℝ^{+}$
17	9 15 16	sylancr	$⊢ A \in ℝ^{+} \to 1 + (\frac{1}{A}) \in ℝ^{+}$
18	17	reeflogd	$⊢ A \in ℝ^{+} \to e^{\log (1 + (\frac{1}{A}))} = 1 + (\frac{1}{A})$
19	17	rpred	$⊢ A \in ℝ^{+} \to 1 + (\frac{1}{A}) \in ℝ$
20	15	rpred	$⊢ A \in ℝ^{+} \to \frac{1}{A} \in ℝ$
21	20	reefcld	$⊢ A \in ℝ^{+} \to e^{\frac{1}{A}} \in ℝ$
22		efgt1p	$⊢ \frac{1}{A} \in ℝ^{+} \to 1 + (\frac{1}{A}) < e^{\frac{1}{A}}$
23	15 22	syl	$⊢ A \in ℝ^{+} \to 1 + (\frac{1}{A}) < e^{\frac{1}{A}}$
24	19 21 23	ltled	$⊢ A \in ℝ^{+} \to 1 + (\frac{1}{A}) \leq e^{\frac{1}{A}}$
25	18 24	eqbrtrd	$⊢ A \in ℝ^{+} \to e^{\log (1 + (\frac{1}{A}))} \leq e^{\frac{1}{A}}$
26		relogcl	$⊢ A + 1 \in ℝ^{+} \to \log (A + 1) \in ℝ$
27	11 26	syl	$⊢ A \in ℝ^{+} \to \log (A + 1) \in ℝ$
28		relogcl	$⊢ A \in ℝ^{+} \to \log A \in ℝ$
29	27 28	resubcld	$⊢ A \in ℝ^{+} \to \log (A + 1) - \log A \in ℝ$
30	14 29	eqeltrd	$⊢ A \in ℝ^{+} \to \log (1 + (\frac{1}{A})) \in ℝ$
31		efle	$⊢ (\log (1 + (\frac{1}{A})) \in ℝ \land \frac{1}{A} \in ℝ) \to (\log (1 + (\frac{1}{A})) \leq \frac{1}{A} \leftrightarrow e^{\log (1 + (\frac{1}{A}))} \leq e^{\frac{1}{A}})$
32	30 20 31	syl2anc	$⊢ A \in ℝ^{+} \to (\log (1 + (\frac{1}{A})) \leq \frac{1}{A} \leftrightarrow e^{\log (1 + (\frac{1}{A}))} \leq e^{\frac{1}{A}})$
33	25 32	mpbird	$⊢ A \in ℝ^{+} \to \log (1 + (\frac{1}{A})) \leq \frac{1}{A}$
34	14 33	eqbrtrrd	$⊢ A \in ℝ^{+} \to \log (A + 1) - \log A \leq \frac{1}{A}$

Metamath Proof Explorer

Theorem logdifbnd

Proof