emcllem4

Description: Lemma for emcl . The difference between series F and G tends to zero. (Contributed by Mario Carneiro, 11-Jul-2014)

	Ref	Expression
Hypotheses	emcl.1	$⊢ F = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log n)$
	emcl.2	$⊢ G = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1))$
	emcl.3	$⊢ H = (n \in ℕ ⟼ \log (1 + (\frac{1}{n})))$
Assertion	emcllem4	$⊢ H ⇝ 0$

Proof

Step	Hyp	Ref	Expression
1		emcl.1	$⊢ F = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log n)$
2		emcl.2	$⊢ G = (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1))$
3		emcl.3	$⊢ H = (n \in ℕ ⟼ \log (1 + (\frac{1}{n})))$
4		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
5		1zzd	$⊢ ⊤ \to 1 \in ℤ$
6		ax-1cn	$⊢ 1 \in ℂ$
7		divcnv	$⊢ 1 \in ℂ \to (n \in ℕ ⟼ \frac{1}{n}) ⇝ 0$
8	6 7	mp1i	$⊢ ⊤ \to (n \in ℕ ⟼ \frac{1}{n}) ⇝ 0$
9		nnex	$⊢ ℕ \in V$
10	9	mptex	$⊢ (n \in ℕ ⟼ \log (1 + (\frac{1}{n}))) \in V$
11	3 10	eqeltri	$⊢ H \in V$
12	11	a1i	$⊢ ⊤ \to H \in V$
13		oveq2	$⊢ n = m \to \frac{1}{n} = \frac{1}{m}$
14		eqid	$⊢ (n \in ℕ ⟼ \frac{1}{n}) = (n \in ℕ ⟼ \frac{1}{n})$
15		ovex	$⊢ \frac{1}{m} \in V$
16	13 14 15	fvmpt	$⊢ m \in ℕ \to (n \in ℕ ⟼ \frac{1}{n}) (m) = \frac{1}{m}$
17	16	adantl	$⊢ (⊤ \land m \in ℕ) \to (n \in ℕ ⟼ \frac{1}{n}) (m) = \frac{1}{m}$
18		nnrecre	$⊢ m \in ℕ \to \frac{1}{m} \in ℝ$
19	18	adantl	$⊢ (⊤ \land m \in ℕ) \to \frac{1}{m} \in ℝ$
20	17 19	eqeltrd	$⊢ (⊤ \land m \in ℕ) \to (n \in ℕ ⟼ \frac{1}{n}) (m) \in ℝ$
21	13	oveq2d	$⊢ n = m \to 1 + (\frac{1}{n}) = 1 + (\frac{1}{m})$
22	21	fveq2d	$⊢ n = m \to \log (1 + (\frac{1}{n})) = \log (1 + (\frac{1}{m}))$
23		fvex	$⊢ \log (1 + (\frac{1}{m})) \in V$
24	22 3 23	fvmpt	$⊢ m \in ℕ \to H (m) = \log (1 + (\frac{1}{m}))$
25	24	adantl	$⊢ (⊤ \land m \in ℕ) \to H (m) = \log (1 + (\frac{1}{m}))$
26		1rp	$⊢ 1 \in ℝ^{+}$
27		nnrp	$⊢ m \in ℕ \to m \in ℝ^{+}$
28	27	adantl	$⊢ (⊤ \land m \in ℕ) \to m \in ℝ^{+}$
29	28	rpreccld	$⊢ (⊤ \land m \in ℕ) \to \frac{1}{m} \in ℝ^{+}$
30		rpaddcl	$⊢ (1 \in ℝ^{+} \land \frac{1}{m} \in ℝ^{+}) \to 1 + (\frac{1}{m}) \in ℝ^{+}$
31	26 29 30	sylancr	$⊢ (⊤ \land m \in ℕ) \to 1 + (\frac{1}{m}) \in ℝ^{+}$
32	31	rpred	$⊢ (⊤ \land m \in ℕ) \to 1 + (\frac{1}{m}) \in ℝ$
33		1re	$⊢ 1 \in ℝ$
34		ltaddrp	$⊢ (1 \in ℝ \land \frac{1}{m} \in ℝ^{+}) \to 1 < 1 + (\frac{1}{m})$
35	33 29 34	sylancr	$⊢ (⊤ \land m \in ℕ) \to 1 < 1 + (\frac{1}{m})$
36	32 35	rplogcld	$⊢ (⊤ \land m \in ℕ) \to \log (1 + (\frac{1}{m})) \in ℝ^{+}$
37	25 36	eqeltrd	$⊢ (⊤ \land m \in ℕ) \to H (m) \in ℝ^{+}$
38	37	rpred	$⊢ (⊤ \land m \in ℕ) \to H (m) \in ℝ$
39	31	relogcld	$⊢ (⊤ \land m \in ℕ) \to \log (1 + (\frac{1}{m})) \in ℝ$
40		efgt1p	$⊢ \frac{1}{m} \in ℝ^{+} \to 1 + (\frac{1}{m}) < e^{\frac{1}{m}}$
41	29 40	syl	$⊢ (⊤ \land m \in ℕ) \to 1 + (\frac{1}{m}) < e^{\frac{1}{m}}$
42	19	rpefcld	$⊢ (⊤ \land m \in ℕ) \to e^{\frac{1}{m}} \in ℝ^{+}$
43		logltb	$⊢ (1 + (\frac{1}{m}) \in ℝ^{+} \land e^{\frac{1}{m}} \in ℝ^{+}) \to (1 + (\frac{1}{m}) < e^{\frac{1}{m}} \leftrightarrow \log (1 + (\frac{1}{m})) < \log e^{\frac{1}{m}})$
44	31 42 43	syl2anc	$⊢ (⊤ \land m \in ℕ) \to (1 + (\frac{1}{m}) < e^{\frac{1}{m}} \leftrightarrow \log (1 + (\frac{1}{m})) < \log e^{\frac{1}{m}})$
45	41 44	mpbid	$⊢ (⊤ \land m \in ℕ) \to \log (1 + (\frac{1}{m})) < \log e^{\frac{1}{m}}$
46	19	relogefd	$⊢ (⊤ \land m \in ℕ) \to \log e^{\frac{1}{m}} = \frac{1}{m}$
47	45 46	breqtrd	$⊢ (⊤ \land m \in ℕ) \to \log (1 + (\frac{1}{m})) < \frac{1}{m}$
48	39 19 47	ltled	$⊢ (⊤ \land m \in ℕ) \to \log (1 + (\frac{1}{m})) \leq \frac{1}{m}$
49	48 25 17	3brtr4d	$⊢ (⊤ \land m \in ℕ) \to H (m) \leq (n \in ℕ ⟼ \frac{1}{n}) (m)$
50	37	rpge0d	$⊢ (⊤ \land m \in ℕ) \to 0 \leq H (m)$
51	4 5 8 12 20 38 49 50	climsqz2	$⊢ ⊤ \to H ⇝ 0$
52	51	mptru	$⊢ H ⇝ 0$

Metamath Proof Explorer

Theorem emcllem4

Proof