emcllem5

Description: Lemma for emcl . The partial sums of the series T , which is used in the definition df-em , is in fact the same as G . (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})))$
	emcl.4	$⊢ T = (n \in ℕ ⟼ (\frac{1}{n}) - \log (1 + (\frac{1}{n})))$
Assertion	emcllem5	$⊢ G = seq 1 (+ T)$

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		emcl.4	$⊢ T = (n \in ℕ ⟼ (\frac{1}{n}) - \log (1 + (\frac{1}{n})))$
5		elfznn	$⊢ m \in (1 \dots n) \to m \in ℕ$
6	5	adantl	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to m \in ℕ$
7	6	nncnd	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to m \in ℂ$
8		1cnd	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to 1 \in ℂ$
9	6	nnne0d	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to m \neq 0$
10	7 8 7 9	divdird	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to \frac{m + 1}{m} = (\frac{m}{m}) + (\frac{1}{m})$
11	7 9	dividd	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to \frac{m}{m} = 1$
12	11	oveq1d	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to (\frac{m}{m}) + (\frac{1}{m}) = 1 + (\frac{1}{m})$
13	10 12	eqtrd	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to \frac{m + 1}{m} = 1 + (\frac{1}{m})$
14	13	fveq2d	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to \log (\frac{m + 1}{m}) = \log (1 + (\frac{1}{m}))$
15		peano2nn	$⊢ m \in ℕ \to m + 1 \in ℕ$
16	6 15	syl	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to m + 1 \in ℕ$
17	16	nnrpd	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to m + 1 \in ℝ^{+}$
18	6	nnrpd	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to m \in ℝ^{+}$
19	17 18	relogdivd	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to \log (\frac{m + 1}{m}) = \log (m + 1) - \log m$
20	14 19	eqtr3d	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to \log (1 + (\frac{1}{m})) = \log (m + 1) - \log m$
21	20	sumeq2dv	$⊢ n \in ℕ \to \sum_{m = 1}^{n} \log (1 + (\frac{1}{m})) = \sum_{m = 1}^{n} (\log (m + 1) - \log m)$
22		fveq2	$⊢ x = m \to \log x = \log m$
23		fveq2	$⊢ x = m + 1 \to \log x = \log (m + 1)$
24		fveq2	$⊢ x = 1 \to \log x = \log 1$
25		fveq2	$⊢ x = n + 1 \to \log x = \log (n + 1)$
26		nnz	$⊢ n \in ℕ \to n \in ℤ$
27		peano2nn	$⊢ n \in ℕ \to n + 1 \in ℕ$
28		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
29	27 28	eleqtrdi	$⊢ n \in ℕ \to n + 1 \in ℤ_{\geq 1}$
30		elfznn	$⊢ x \in (1 \dots n + 1) \to x \in ℕ$
31	30	adantl	$⊢ (n \in ℕ \land x \in (1 \dots n + 1)) \to x \in ℕ$
32	31	nnrpd	$⊢ (n \in ℕ \land x \in (1 \dots n + 1)) \to x \in ℝ^{+}$
33	32	relogcld	$⊢ (n \in ℕ \land x \in (1 \dots n + 1)) \to \log x \in ℝ$
34	33	recnd	$⊢ (n \in ℕ \land x \in (1 \dots n + 1)) \to \log x \in ℂ$
35	22 23 24 25 26 29 34	telfsum2	$⊢ n \in ℕ \to \sum_{m = 1}^{n} (\log (m + 1) - \log m) = \log (n + 1) - \log 1$
36		log1	$⊢ \log 1 = 0$
37	36	oveq2i	$⊢ \log (n + 1) - \log 1 = \log (n + 1) - 0$
38	27	nnrpd	$⊢ n \in ℕ \to n + 1 \in ℝ^{+}$
39	38	relogcld	$⊢ n \in ℕ \to \log (n + 1) \in ℝ$
40	39	recnd	$⊢ n \in ℕ \to \log (n + 1) \in ℂ$
41	40	subid1d	$⊢ n \in ℕ \to \log (n + 1) - 0 = \log (n + 1)$
42	37 41	syl5eq	$⊢ n \in ℕ \to \log (n + 1) - \log 1 = \log (n + 1)$
43	21 35 42	3eqtrd	$⊢ n \in ℕ \to \sum_{m = 1}^{n} \log (1 + (\frac{1}{m})) = \log (n + 1)$
44	43	oveq2d	$⊢ n \in ℕ \to \sum_{m = 1}^{n} (\frac{1}{m}) - \sum_{m = 1}^{n} \log (1 + (\frac{1}{m})) = \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1)$
45		fzfid	$⊢ n \in ℕ \to (1 \dots n) \in Fin$
46	6	nnrecred	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to \frac{1}{m} \in ℝ$
47	46	recnd	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to \frac{1}{m} \in ℂ$
48		1rp	$⊢ 1 \in ℝ^{+}$
49	18	rpreccld	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to \frac{1}{m} \in ℝ^{+}$
50		rpaddcl	$⊢ (1 \in ℝ^{+} \land \frac{1}{m} \in ℝ^{+}) \to 1 + (\frac{1}{m}) \in ℝ^{+}$
51	48 49 50	sylancr	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to 1 + (\frac{1}{m}) \in ℝ^{+}$
52	51	relogcld	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to \log (1 + (\frac{1}{m})) \in ℝ$
53	52	recnd	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to \log (1 + (\frac{1}{m})) \in ℂ$
54	45 47 53	fsumsub	$⊢ n \in ℕ \to \sum_{m = 1}^{n} ((\frac{1}{m}) - \log (1 + (\frac{1}{m}))) = \sum_{m = 1}^{n} (\frac{1}{m}) - \sum_{m = 1}^{n} \log (1 + (\frac{1}{m}))$
55		oveq2	$⊢ n = m \to \frac{1}{n} = \frac{1}{m}$
56	55	oveq2d	$⊢ n = m \to 1 + (\frac{1}{n}) = 1 + (\frac{1}{m})$
57	56	fveq2d	$⊢ n = m \to \log (1 + (\frac{1}{n})) = \log (1 + (\frac{1}{m}))$
58	55 57	oveq12d	$⊢ n = m \to (\frac{1}{n}) - \log (1 + (\frac{1}{n})) = (\frac{1}{m}) - \log (1 + (\frac{1}{m}))$
59		ovex	$⊢ (\frac{1}{m}) - \log (1 + (\frac{1}{m})) \in V$
60	58 4 59	fvmpt	$⊢ m \in ℕ \to T (m) = (\frac{1}{m}) - \log (1 + (\frac{1}{m}))$
61	6 60	syl	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to T (m) = (\frac{1}{m}) - \log (1 + (\frac{1}{m}))$
62		id	$⊢ n \in ℕ \to n \in ℕ$
63	62 28	eleqtrdi	$⊢ n \in ℕ \to n \in ℤ_{\geq 1}$
64	46 52	resubcld	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to (\frac{1}{m}) - \log (1 + (\frac{1}{m})) \in ℝ$
65	64	recnd	$⊢ (n \in ℕ \land m \in (1 \dots n)) \to (\frac{1}{m}) - \log (1 + (\frac{1}{m})) \in ℂ$
66	61 63 65	fsumser	$⊢ n \in ℕ \to \sum_{m = 1}^{n} ((\frac{1}{m}) - \log (1 + (\frac{1}{m}))) = seq 1 (+ T) (n)$
67	54 66	eqtr3d	$⊢ n \in ℕ \to \sum_{m = 1}^{n} (\frac{1}{m}) - \sum_{m = 1}^{n} \log (1 + (\frac{1}{m})) = seq 1 (+ T) (n)$
68	44 67	eqtr3d	$⊢ n \in ℕ \to \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1) = seq 1 (+ T) (n)$
69	68	mpteq2ia	$⊢ (n \in ℕ ⟼ \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1)) = (n \in ℕ ⟼ seq 1 (+ T) (n))$
70		1z	$⊢ 1 \in ℤ$
71		seqfn	$⊢ 1 \in ℤ \to seq 1 (+ T) Fn ℤ_{\geq 1}$
72	70 71	ax-mp	$⊢ seq 1 (+ T) Fn ℤ_{\geq 1}$
73	28	fneq2i	$⊢ seq 1 (+ T) Fn ℕ \leftrightarrow seq 1 (+ T) Fn ℤ_{\geq 1}$
74	72 73	mpbir	$⊢ seq 1 (+ T) Fn ℕ$
75		dffn5	$⊢ seq 1 (+ T) Fn ℕ \leftrightarrow seq 1 (+ T) = (n \in ℕ ⟼ seq 1 (+ T) (n))$
76	74 75	mpbi	$⊢ seq 1 (+ T) = (n \in ℕ ⟼ seq 1 (+ T) (n))$
77	69 2 76	3eqtr4i	$⊢ G = seq 1 (+ T)$

Metamath Proof Explorer

Theorem emcllem5

Proof