emcllem3

Description: Lemma for emcl . The function H is the difference between F and 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})))$
Assertion	emcllem3	$⊢ N \in ℕ \to H (N) = F (N) - G (N)$

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		peano2nn	$⊢ N \in ℕ \to N + 1 \in ℕ$
5	4	nnrpd	$⊢ N \in ℕ \to N + 1 \in ℝ^{+}$
6		nnrp	$⊢ N \in ℕ \to N \in ℝ^{+}$
7	5 6	relogdivd	$⊢ N \in ℕ \to \log (\frac{N + 1}{N}) = \log (N + 1) - \log N$
8		nncn	$⊢ N \in ℕ \to N \in ℂ$
9		1cnd	$⊢ N \in ℕ \to 1 \in ℂ$
10		nnne0	$⊢ N \in ℕ \to N \neq 0$
11	8 9 8 10	divdird	$⊢ N \in ℕ \to \frac{N + 1}{N} = (\frac{N}{N}) + (\frac{1}{N})$
12	8 10	dividd	$⊢ N \in ℕ \to \frac{N}{N} = 1$
13	12	oveq1d	$⊢ N \in ℕ \to (\frac{N}{N}) + (\frac{1}{N}) = 1 + (\frac{1}{N})$
14	11 13	eqtr2d	$⊢ N \in ℕ \to 1 + (\frac{1}{N}) = \frac{N + 1}{N}$
15	14	fveq2d	$⊢ N \in ℕ \to \log (1 + (\frac{1}{N})) = \log (\frac{N + 1}{N})$
16		fzfid	$⊢ N \in ℕ \to (1 \dots N) \in Fin$
17		elfznn	$⊢ m \in (1 \dots N) \to m \in ℕ$
18	17	adantl	$⊢ (N \in ℕ \land m \in (1 \dots N)) \to m \in ℕ$
19	18	nnrecred	$⊢ (N \in ℕ \land m \in (1 \dots N)) \to \frac{1}{m} \in ℝ$
20	16 19	fsumrecl	$⊢ N \in ℕ \to \sum_{m = 1}^{N} (\frac{1}{m}) \in ℝ$
21	20	recnd	$⊢ N \in ℕ \to \sum_{m = 1}^{N} (\frac{1}{m}) \in ℂ$
22	6	relogcld	$⊢ N \in ℕ \to \log N \in ℝ$
23	22	recnd	$⊢ N \in ℕ \to \log N \in ℂ$
24	5	relogcld	$⊢ N \in ℕ \to \log (N + 1) \in ℝ$
25	24	recnd	$⊢ N \in ℕ \to \log (N + 1) \in ℂ$
26	21 23 25	nnncan1d	$⊢ N \in ℕ \to \sum_{m = 1}^{N} (\frac{1}{m}) - \log N - (\sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1)) = \log (N + 1) - \log N$
27	7 15 26	3eqtr4d	$⊢ N \in ℕ \to \log (1 + (\frac{1}{N})) = \sum_{m = 1}^{N} (\frac{1}{m}) - \log N - (\sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1))$
28		oveq2	$⊢ n = N \to \frac{1}{n} = \frac{1}{N}$
29	28	oveq2d	$⊢ n = N \to 1 + (\frac{1}{n}) = 1 + (\frac{1}{N})$
30	29	fveq2d	$⊢ n = N \to \log (1 + (\frac{1}{n})) = \log (1 + (\frac{1}{N}))$
31		fvex	$⊢ \log (1 + (\frac{1}{N})) \in V$
32	30 3 31	fvmpt	$⊢ N \in ℕ \to H (N) = \log (1 + (\frac{1}{N}))$
33		oveq2	$⊢ n = N \to (1 \dots n) = (1 \dots N)$
34	33	sumeq1d	$⊢ n = N \to \sum_{m = 1}^{n} (\frac{1}{m}) = \sum_{m = 1}^{N} (\frac{1}{m})$
35		fveq2	$⊢ n = N \to \log n = \log N$
36	34 35	oveq12d	$⊢ n = N \to \sum_{m = 1}^{n} (\frac{1}{m}) - \log n = \sum_{m = 1}^{N} (\frac{1}{m}) - \log N$
37		ovex	$⊢ \sum_{m = 1}^{N} (\frac{1}{m}) - \log N \in V$
38	36 1 37	fvmpt	$⊢ N \in ℕ \to F (N) = \sum_{m = 1}^{N} (\frac{1}{m}) - \log N$
39		fvoveq1	$⊢ n = N \to \log (n + 1) = \log (N + 1)$
40	34 39	oveq12d	$⊢ n = N \to \sum_{m = 1}^{n} (\frac{1}{m}) - \log (n + 1) = \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1)$
41		ovex	$⊢ \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1) \in V$
42	40 2 41	fvmpt	$⊢ N \in ℕ \to G (N) = \sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1)$
43	38 42	oveq12d	$⊢ N \in ℕ \to F (N) - G (N) = \sum_{m = 1}^{N} (\frac{1}{m}) - \log N - (\sum_{m = 1}^{N} (\frac{1}{m}) - \log (N + 1))$
44	27 32 43	3eqtr4d	$⊢ N \in ℕ \to H (N) = F (N) - G (N)$

Metamath Proof Explorer

Theorem emcllem3

Proof