harmonicbnd3

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

		Ref	Expression
	Assertion	harmonicbnd3	$⊢ N \in ℕ_{0} \to \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) \in [0, γ]$

Proof

Step	Hyp	Ref	Expression
1		elnn0	$⊢ N \in ℕ_{0} \leftrightarrow (N \in ℕ \lor N = 0)$
2		0re	$⊢ 0 \in ℝ$
3		emre	$⊢ γ \in ℝ$
4		2re	$⊢ 2 \in ℝ$
5		ere	$⊢ e \in ℝ$
6		egt2lt3	$⊢ (2 < e \land e < 3)$
7	6	simpli	$⊢ 2 < e$
8	4 5 7	ltleii	$⊢ 2 \leq e$
9		2rp	$⊢ 2 \in ℝ^{+}$
10		epr	$⊢ e \in ℝ^{+}$
11		logleb	$⊢ (2 \in ℝ^{+} \land e \in ℝ^{+}) \to (2 \leq e \leftrightarrow \log 2 \leq \log e)$
12	9 10 11	mp2an	$⊢ 2 \leq e \leftrightarrow \log 2 \leq \log e$
13	8 12	mpbi	$⊢ \log 2 \leq \log e$
14		loge	$⊢ \log e = 1$
15	13 14	breqtri	$⊢ \log 2 \leq 1$
16		1re	$⊢ 1 \in ℝ$
17		relogcl	$⊢ 2 \in ℝ^{+} \to \log 2 \in ℝ$
18	9 17	ax-mp	$⊢ \log 2 \in ℝ$
19	16 18	subge0i	$⊢ 0 \leq 1 - \log 2 \leftrightarrow \log 2 \leq 1$
20	15 19	mpbir	$⊢ 0 \leq 1 - \log 2$
21	3	leidi	$⊢ γ \leq γ$
22		iccss	$⊢ ((0 \in ℝ \land γ \in ℝ) \land (0 \leq 1 - \log 2 \land γ \leq γ)) \to [1 - \log 2, γ] \subseteq [0, γ]$
23	2 3 20 21 22	mp4an	$⊢ [1 - \log 2, γ] \subseteq [0, γ]$
24		harmonicbnd2	$⊢ N \in ℕ \to \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) \in [1 - \log 2, γ]$
25	23 24	sselid	$⊢ N \in ℕ \to \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) \in [0, γ]$
26		oveq2	$⊢ N = 0 \to (1 \dots N) = (1 \dots 0)$
27		fz10	$⊢ (1 \dots 0) = \emptyset$
28	26 27	eqtrdi	$⊢ N = 0 \to (1 \dots N) = \emptyset$
29	28	sumeq1d	$⊢ N = 0 \to \sum_{m = 1}^{N} (\frac{1}{m}) = \sum_{m \in \emptyset} (\frac{1}{m})$
30		sum0	$⊢ \sum_{m \in \emptyset} (\frac{1}{m}) = 0$
31	29 30	eqtrdi	$⊢ N = 0 \to \sum_{m = 1}^{N} (\frac{1}{m}) = 0$
32		fv0p1e1	$⊢ N = 0 \to \log (N + 1) = \log 1$
33		log1	$⊢ \log 1 = 0$
34	32 33	eqtrdi	$⊢ N = 0 \to \log (N + 1) = 0$
35	31 34	oveq12d	$⊢ N = 0 \to \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) = 0 - 0$
36		0m0e0	$⊢ 0 - 0 = 0$
37	35 36	eqtrdi	$⊢ N = 0 \to \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) = 0$
38	2	leidi	$⊢ 0 \leq 0$
39		emgt0	$⊢ 0 < γ$
40	2 3 39	ltleii	$⊢ 0 \leq γ$
41	2 3	elicc2i	$⊢ 0 \in [0, γ] \leftrightarrow (0 \in ℝ \land 0 \leq 0 \land 0 \leq γ)$
42	2 38 40 41	mpbir3an	$⊢ 0 \in [0, γ]$
43	37 42	eqeltrdi	$⊢ N = 0 \to \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) \in [0, γ]$
44	25 43	jaoi	$⊢ (N \in ℕ \lor N = 0) \to \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) \in [0, γ]$
45	1 44	sylbi	$⊢ N \in ℕ_{0} \to \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) \in [0, γ]$

Metamath Proof Explorer

Theorem harmonicbnd3

Proof