trireciplem

Description: Lemma for trirecip . Show that the sum converges. (Contributed by Scott Fenton, 22-Apr-2014) (Revised by Mario Carneiro, 22-May-2014)

		Ref	Expression
	Hypothesis	trireciplem.1	$⊢ F = (n \in ℕ ⟼ \frac{1}{n (n + 1)})$
	Assertion	trireciplem	$⊢ seq 1 (+ F) ⇝ 1$

Proof

Step	Hyp	Ref	Expression
1		trireciplem.1	$⊢ F = (n \in ℕ ⟼ \frac{1}{n (n + 1)})$
2		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
3		1zzd	$⊢ ⊤ \to 1 \in ℤ$
4		1cnd	$⊢ ⊤ \to 1 \in ℂ$
5		nnex	$⊢ ℕ \in V$
6	5	mptex	$⊢ (n \in ℕ ⟼ \frac{1}{n + 1}) \in V$
7	6	a1i	$⊢ ⊤ \to (n \in ℕ ⟼ \frac{1}{n + 1}) \in V$
8		oveq1	$⊢ n = k \to n + 1 = k + 1$
9	8	oveq2d	$⊢ n = k \to \frac{1}{n + 1} = \frac{1}{k + 1}$
10		eqid	$⊢ (n \in ℕ ⟼ \frac{1}{n + 1}) = (n \in ℕ ⟼ \frac{1}{n + 1})$
11		ovex	$⊢ \frac{1}{k + 1} \in V$
12	9 10 11	fvmpt	$⊢ k \in ℕ \to (n \in ℕ ⟼ \frac{1}{n + 1}) (k) = \frac{1}{k + 1}$
13	12	adantl	$⊢ (⊤ \land k \in ℕ) \to (n \in ℕ ⟼ \frac{1}{n + 1}) (k) = \frac{1}{k + 1}$
14	2 3 4 3 7 13	divcnvshft	$⊢ ⊤ \to (n \in ℕ ⟼ \frac{1}{n + 1}) ⇝ 0$
15		seqex	$⊢ seq 1 (+ F) \in V$
16	15	a1i	$⊢ ⊤ \to seq 1 (+ F) \in V$
17		peano2nn	$⊢ k \in ℕ \to k + 1 \in ℕ$
18	17	adantl	$⊢ (⊤ \land k \in ℕ) \to k + 1 \in ℕ$
19	18	nnrecred	$⊢ (⊤ \land k \in ℕ) \to \frac{1}{k + 1} \in ℝ$
20	19	recnd	$⊢ (⊤ \land k \in ℕ) \to \frac{1}{k + 1} \in ℂ$
21	13 20	eqeltrd	$⊢ (⊤ \land k \in ℕ) \to (n \in ℕ ⟼ \frac{1}{n + 1}) (k) \in ℂ$
22	13	oveq2d	$⊢ (⊤ \land k \in ℕ) \to 1 - (n \in ℕ ⟼ \frac{1}{n + 1}) (k) = 1 - (\frac{1}{k + 1})$
23		elfznn	$⊢ j \in (1 \dots k) \to j \in ℕ$
24	23	adantl	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to j \in ℕ$
25	24	nncnd	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to j \in ℂ$
26		peano2cn	$⊢ j \in ℂ \to j + 1 \in ℂ$
27	25 26	syl	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to j + 1 \in ℂ$
28		peano2nn	$⊢ j \in ℕ \to j + 1 \in ℕ$
29	24 28	syl	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to j + 1 \in ℕ$
30	24 29	nnmulcld	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to j (j + 1) \in ℕ$
31	30	nncnd	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to j (j + 1) \in ℂ$
32	30	nnne0d	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to j (j + 1) \neq 0$
33	27 25 31 32	divsubdird	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to \frac{j + 1 - j}{j (j + 1)} = (\frac{j + 1}{j (j + 1)}) - (\frac{j}{j (j + 1)})$
34		ax-1cn	$⊢ 1 \in ℂ$
35		pncan2	$⊢ (j \in ℂ \land 1 \in ℂ) \to j + 1 - j = 1$
36	25 34 35	sylancl	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to j + 1 - j = 1$
37	36	oveq1d	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to \frac{j + 1 - j}{j (j + 1)} = \frac{1}{j (j + 1)}$
38	27	mulid1d	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to (j + 1) \cdot 1 = j + 1$
39	27 25	mulcomd	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to (j + 1) j = j (j + 1)$
40	38 39	oveq12d	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to \frac{(j + 1) \cdot 1}{(j + 1) j} = \frac{j + 1}{j (j + 1)}$
41		1cnd	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to 1 \in ℂ$
42	24	nnne0d	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to j \neq 0$
43	29	nnne0d	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to j + 1 \neq 0$
44	41 25 27 42 43	divcan5d	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to \frac{(j + 1) \cdot 1}{(j + 1) j} = \frac{1}{j}$
45	40 44	eqtr3d	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to \frac{j + 1}{j (j + 1)} = \frac{1}{j}$
46	25	mulid1d	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to j \cdot 1 = j$
47	46	oveq1d	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to \frac{j \cdot 1}{j (j + 1)} = \frac{j}{j (j + 1)}$
48	41 27 25 43 42	divcan5d	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to \frac{j \cdot 1}{j (j + 1)} = \frac{1}{j + 1}$
49	47 48	eqtr3d	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to \frac{j}{j (j + 1)} = \frac{1}{j + 1}$
50	45 49	oveq12d	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to (\frac{j + 1}{j (j + 1)}) - (\frac{j}{j (j + 1)}) = (\frac{1}{j}) - (\frac{1}{j + 1})$
51	33 37 50	3eqtr3d	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to \frac{1}{j (j + 1)} = (\frac{1}{j}) - (\frac{1}{j + 1})$
52	51	sumeq2dv	$⊢ (⊤ \land k \in ℕ) \to \sum_{j = 1}^{k} (\frac{1}{j (j + 1)}) = \sum_{j = 1}^{k} ((\frac{1}{j}) - (\frac{1}{j + 1}))$
53		oveq2	$⊢ n = j \to \frac{1}{n} = \frac{1}{j}$
54		oveq2	$⊢ n = j + 1 \to \frac{1}{n} = \frac{1}{j + 1}$
55		oveq2	$⊢ n = 1 \to \frac{1}{n} = \frac{1}{1}$
56		1div1e1	$⊢ \frac{1}{1} = 1$
57	55 56	eqtrdi	$⊢ n = 1 \to \frac{1}{n} = 1$
58		oveq2	$⊢ n = k + 1 \to \frac{1}{n} = \frac{1}{k + 1}$
59		nnz	$⊢ k \in ℕ \to k \in ℤ$
60	59	adantl	$⊢ (⊤ \land k \in ℕ) \to k \in ℤ$
61	18 2	eleqtrdi	$⊢ (⊤ \land k \in ℕ) \to k + 1 \in ℤ_{\geq 1}$
62		elfznn	$⊢ n \in (1 \dots k + 1) \to n \in ℕ$
63	62	adantl	$⊢ ((⊤ \land k \in ℕ) \land n \in (1 \dots k + 1)) \to n \in ℕ$
64	63	nnrecred	$⊢ ((⊤ \land k \in ℕ) \land n \in (1 \dots k + 1)) \to \frac{1}{n} \in ℝ$
65	64	recnd	$⊢ ((⊤ \land k \in ℕ) \land n \in (1 \dots k + 1)) \to \frac{1}{n} \in ℂ$
66	53 54 57 58 60 61 65	telfsum	$⊢ (⊤ \land k \in ℕ) \to \sum_{j = 1}^{k} ((\frac{1}{j}) - (\frac{1}{j + 1})) = 1 - (\frac{1}{k + 1})$
67	52 66	eqtrd	$⊢ (⊤ \land k \in ℕ) \to \sum_{j = 1}^{k} (\frac{1}{j (j + 1)}) = 1 - (\frac{1}{k + 1})$
68		id	$⊢ n = j \to n = j$
69		oveq1	$⊢ n = j \to n + 1 = j + 1$
70	68 69	oveq12d	$⊢ n = j \to n (n + 1) = j (j + 1)$
71	70	oveq2d	$⊢ n = j \to \frac{1}{n (n + 1)} = \frac{1}{j (j + 1)}$
72		ovex	$⊢ \frac{1}{j (j + 1)} \in V$
73	71 1 72	fvmpt	$⊢ j \in ℕ \to F (j) = \frac{1}{j (j + 1)}$
74	24 73	syl	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to F (j) = \frac{1}{j (j + 1)}$
75		simpr	$⊢ (⊤ \land k \in ℕ) \to k \in ℕ$
76	75 2	eleqtrdi	$⊢ (⊤ \land k \in ℕ) \to k \in ℤ_{\geq 1}$
77	30	nnrecred	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to \frac{1}{j (j + 1)} \in ℝ$
78	77	recnd	$⊢ ((⊤ \land k \in ℕ) \land j \in (1 \dots k)) \to \frac{1}{j (j + 1)} \in ℂ$
79	74 76 78	fsumser	$⊢ (⊤ \land k \in ℕ) \to \sum_{j = 1}^{k} (\frac{1}{j (j + 1)}) = seq 1 (+ F) (k)$
80	22 67 79	3eqtr2rd	$⊢ (⊤ \land k \in ℕ) \to seq 1 (+ F) (k) = 1 - (n \in ℕ ⟼ \frac{1}{n + 1}) (k)$
81	2 3 14 4 16 21 80	climsubc2	$⊢ ⊤ \to seq 1 (+ F) ⇝ (1 - 0)$
82	81	mptru	$⊢ seq 1 (+ F) ⇝ (1 - 0)$
83		1m0e1	$⊢ 1 - 0 = 1$
84	82 83	breqtri	$⊢ seq 1 (+ F) ⇝ 1$

Metamath Proof Explorer

Theorem trireciplem

Proof