Theorem harmoniclbnd

Description: A bound on the harmonic series, as compared to the natural logarithm. (Contributed by Mario Carneiro, 13-Apr-2016)

	Ref	Expression
Assertion	harmoniclbnd	$$⊢A\in {ℝ}^{+}\to \log A\le \sum _{m=1}^{⌊A⌋}\left(\frac{1}{m}\right)$$

Proof

Step	Hyp	Ref	Expression
1		relogcl	$$⊢A\in {ℝ}^{+}\to \log A\in ℝ$$
2		rprege0	$$⊢A\in {ℝ}^{+}\to \left(A\in ℝ\wedge 0\le A\right)$$
3		flge0nn0	$$⊢\left(A\in ℝ\wedge 0\le A\right)\to ⌊A⌋\in {\mathbb{N}}_0$$
4	2 3	syl	$$⊢A\in {ℝ}^{+}\to ⌊A⌋\in {\mathbb{N}}_0$$
5		nn0p1nn	$$⊢⌊A⌋\in {\mathbb{N}}_0\to ⌊A⌋+1\in \mathbb{N}$$
6	4 5	syl	$$⊢A\in {ℝ}^{+}\to ⌊A⌋+1\in \mathbb{N}$$
7	6	nnrpd	$$⊢A\in {ℝ}^{+}\to ⌊A⌋+1\in {ℝ}^{+}$$
8		relogcl	$$⊢⌊A⌋+1\in {ℝ}^{+}\to \log \left(⌊A⌋+1\right)\in ℝ$$
9	7 8	syl	$$⊢A\in {ℝ}^{+}\to \log \left(⌊A⌋+1\right)\in ℝ$$
10		fzfid	$$⊢A\in {ℝ}^{+}\to \left(1\dots ⌊A⌋\right)\in \mathrm{Fin}$$
11		elfznn	$$⊢m\in \left(1\dots ⌊A⌋\right)\to m\in \mathbb{N}$$
12	11	adantl	$$⊢\left(A\in {ℝ}^{+}\wedge m\in \left(1\dots ⌊A⌋\right)\right)\to m\in \mathbb{N}$$
13	12	nnrecred	$$⊢\left(A\in {ℝ}^{+}\wedge m\in \left(1\dots ⌊A⌋\right)\right)\to \frac{1}{m}\in ℝ$$
14	10 13	fsumrecl	$$⊢A\in {ℝ}^{+}\to \sum _{m=1}^{⌊A⌋}\left(\frac{1}{m}\right)\in ℝ$$
15		rpre	$$⊢A\in {ℝ}^{+}\to A\in ℝ$$
16		fllep1	$$⊢A\in ℝ\to A\le ⌊A⌋+1$$
17	15 16	syl	$$⊢A\in {ℝ}^{+}\to A\le ⌊A⌋+1$$
18		id	$$⊢A\in {ℝ}^{+}\to A\in {ℝ}^{+}$$
19	18 7	logled	$$⊢A\in {ℝ}^{+}\to \left(A\le ⌊A⌋+1\leftrightarrow \log A\le \log \left(⌊A⌋+1\right)\right)$$
20	17 19	mpbid	$$⊢A\in {ℝ}^{+}\to \log A\le \log \left(⌊A⌋+1\right)$$
21		harmonicbnd3	$$⊢⌊A⌋\in {\mathbb{N}}_0\to \sum _{m=1}^{⌊A⌋}\left(\frac{1}{m}\right)-\log \left(⌊A⌋+1\right)\in \left[0,\gamma \right]$$
22	4 21	syl	$$⊢A\in {ℝ}^{+}\to \sum _{m=1}^{⌊A⌋}\left(\frac{1}{m}\right)-\log \left(⌊A⌋+1\right)\in \left[0,\gamma \right]$$
23		0re	$$⊢0\in ℝ$$
24		emre	$$⊢\gamma \in ℝ$$
25	23 24	elicc2i	$$⊢\sum _{m=1}^{⌊A⌋}\left(\frac{1}{m}\right)-\log \left(⌊A⌋+1\right)\in \left[0,\gamma \right]\leftrightarrow \left(\sum _{m=1}^{⌊A⌋}\left(\frac{1}{m}\right)-\log \left(⌊A⌋+1\right)\in ℝ\wedge 0\le \sum _{m=1}^{⌊A⌋}\left(\frac{1}{m}\right)-\log \left(⌊A⌋+1\right)\wedge \sum _{m=1}^{⌊A⌋}\left(\frac{1}{m}\right)-\log \left(⌊A⌋+1\right)\le \gamma \right)$$
26	25	simp2bi	$$⊢\sum _{m=1}^{⌊A⌋}\left(\frac{1}{m}\right)-\log \left(⌊A⌋+1\right)\in \left[0,\gamma \right]\to 0\le \sum _{m=1}^{⌊A⌋}\left(\frac{1}{m}\right)-\log \left(⌊A⌋+1\right)$$
27	22 26	syl	$$⊢A\in {ℝ}^{+}\to 0\le \sum _{m=1}^{⌊A⌋}\left(\frac{1}{m}\right)-\log \left(⌊A⌋+1\right)$$
28	14 9	subge0d	$$⊢A\in {ℝ}^{+}\to \left(0\le \sum _{m=1}^{⌊A⌋}\left(\frac{1}{m}\right)-\log \left(⌊A⌋+1\right)\leftrightarrow \log \left(⌊A⌋+1\right)\le \sum _{m=1}^{⌊A⌋}\left(\frac{1}{m}\right)\right)$$
29	27 28	mpbid	$$⊢A\in {ℝ}^{+}\to \log \left(⌊A⌋+1\right)\le \sum _{m=1}^{⌊A⌋}\left(\frac{1}{m}\right)$$
30	1 9 14 20 29	letrd	$$⊢A\in {ℝ}^{+}\to \log A\le \sum _{m=1}^{⌊A⌋}\left(\frac{1}{m}\right)$$