serf0

Description: If an infinite series converges, its underlying sequence converges to zero. (Contributed by NM, 2-Sep-2005) (Revised by Mario Carneiro, 16-Feb-2014)

	Ref	Expression
Hypotheses	caucvgb.1	$⊢ Z = ℤ_{\geq M}$
	serf0.2	$⊢ φ \to M \in ℤ$
	serf0.3	$⊢ φ \to F \in V$
	serf0.4	$⊢ φ \to seq M (+ F) \in dom ⇝$
	serf0.5	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
Assertion	serf0	$⊢ φ \to F ⇝ 0$

Proof

Step	Hyp	Ref	Expression
1		caucvgb.1	$⊢ Z = ℤ_{\geq M}$
2		serf0.2	$⊢ φ \to M \in ℤ$
3		serf0.3	$⊢ φ \to F \in V$
4		serf0.4	$⊢ φ \to seq M (+ F) \in dom ⇝$
5		serf0.5	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
6	1	caucvgb	$⊢ (M \in ℤ \land seq M (+ F) \in dom ⇝) \to (seq M (+ F) \in dom ⇝ \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall m \in ℤ_{\geq j} (seq M (+ F) (m) \in ℂ \land \|seq M (+ F) (m) - seq M (+ F) (j)\| < x))$
7	2 4 6	syl2anc	$⊢ φ \to (seq M (+ F) \in dom ⇝ \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall m \in ℤ_{\geq j} (seq M (+ F) (m) \in ℂ \land \|seq M (+ F) (m) - seq M (+ F) (j)\| < x))$
8	4 7	mpbid	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall m \in ℤ_{\geq j} (seq M (+ F) (m) \in ℂ \land \|seq M (+ F) (m) - seq M (+ F) (j)\| < x)$
9	1	cau3	$⊢ \forall x \in ℝ^{+} \exists j \in Z \forall m \in ℤ_{\geq j} (seq M (+ F) (m) \in ℂ \land \|seq M (+ F) (m) - seq M (+ F) (j)\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in Z \forall m \in ℤ_{\geq j} (seq M (+ F) (m) \in ℂ \land \forall k \in ℤ_{\geq m} \|seq M (+ F) (m) - seq M (+ F) (k)\| < x)$
10	8 9	sylib	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall m \in ℤ_{\geq j} (seq M (+ F) (m) \in ℂ \land \forall k \in ℤ_{\geq m} \|seq M (+ F) (m) - seq M (+ F) (k)\| < x)$
11	1	peano2uzs	$⊢ j \in Z \to j + 1 \in Z$
12	11	adantl	$⊢ (φ \land j \in Z) \to j + 1 \in Z$
13		eluzelz	$⊢ m \in ℤ_{\geq j} \to m \in ℤ$
14		uzid	$⊢ m \in ℤ \to m \in ℤ_{\geq m}$
15		peano2uz	$⊢ m \in ℤ_{\geq m} \to m + 1 \in ℤ_{\geq m}$
16		fveq2	$⊢ k = m + 1 \to seq M (+ F) (k) = seq M (+ F) (m + 1)$
17	16	oveq2d	$⊢ k = m + 1 \to seq M (+ F) (m) - seq M (+ F) (k) = seq M (+ F) (m) - seq M (+ F) (m + 1)$
18	17	fveq2d	$⊢ k = m + 1 \to \|seq M (+ F) (m) - seq M (+ F) (k)\| = \|seq M (+ F) (m) - seq M (+ F) (m + 1)\|$
19	18	breq1d	$⊢ k = m + 1 \to (\|seq M (+ F) (m) - seq M (+ F) (k)\| < x \leftrightarrow \|seq M (+ F) (m) - seq M (+ F) (m + 1)\| < x)$
20	19	rspcv	$⊢ m + 1 \in ℤ_{\geq m} \to (\forall k \in ℤ_{\geq m} \|seq M (+ F) (m) - seq M (+ F) (k)\| < x \to \|seq M (+ F) (m) - seq M (+ F) (m + 1)\| < x)$
21	13 14 15 20	4syl	$⊢ m \in ℤ_{\geq j} \to (\forall k \in ℤ_{\geq m} \|seq M (+ F) (m) - seq M (+ F) (k)\| < x \to \|seq M (+ F) (m) - seq M (+ F) (m + 1)\| < x)$
22	21	adantld	$⊢ m \in ℤ_{\geq j} \to ((seq M (+ F) (m) \in ℂ \land \forall k \in ℤ_{\geq m} \|seq M (+ F) (m) - seq M (+ F) (k)\| < x) \to \|seq M (+ F) (m) - seq M (+ F) (m + 1)\| < x)$
23	22	ralimia	$⊢ \forall m \in ℤ_{\geq j} (seq M (+ F) (m) \in ℂ \land \forall k \in ℤ_{\geq m} \|seq M (+ F) (m) - seq M (+ F) (k)\| < x) \to \forall m \in ℤ_{\geq j} \|seq M (+ F) (m) - seq M (+ F) (m + 1)\| < x$
24		simpr	$⊢ (φ \land j \in Z) \to j \in Z$
25	24 1	eleqtrdi	$⊢ (φ \land j \in Z) \to j \in ℤ_{\geq M}$
26		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
27	25 26	syl	$⊢ (φ \land j \in Z) \to j \in ℤ$
28		eluzp1m1	$⊢ (j \in ℤ \land k \in ℤ_{\geq (j + 1)}) \to k - 1 \in ℤ_{\geq j}$
29	27 28	sylan	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to k - 1 \in ℤ_{\geq j}$
30		fveq2	$⊢ m = k - 1 \to seq M (+ F) (m) = seq M (+ F) (k - 1)$
31		fvoveq1	$⊢ m = k - 1 \to seq M (+ F) (m + 1) = seq M (+ F) (k - 1 + 1)$
32	30 31	oveq12d	$⊢ m = k - 1 \to seq M (+ F) (m) - seq M (+ F) (m + 1) = seq M (+ F) (k - 1) - seq M (+ F) (k - 1 + 1)$
33	32	fveq2d	$⊢ m = k - 1 \to \|seq M (+ F) (m) - seq M (+ F) (m + 1)\| = \|seq M (+ F) (k - 1) - seq M (+ F) (k - 1 + 1)\|$
34	33	breq1d	$⊢ m = k - 1 \to (\|seq M (+ F) (m) - seq M (+ F) (m + 1)\| < x \leftrightarrow \|seq M (+ F) (k - 1) - seq M (+ F) (k - 1 + 1)\| < x)$
35	34	rspcv	$⊢ k - 1 \in ℤ_{\geq j} \to (\forall m \in ℤ_{\geq j} \|seq M (+ F) (m) - seq M (+ F) (m + 1)\| < x \to \|seq M (+ F) (k - 1) - seq M (+ F) (k - 1 + 1)\| < x)$
36	29 35	syl	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to (\forall m \in ℤ_{\geq j} \|seq M (+ F) (m) - seq M (+ F) (m + 1)\| < x \to \|seq M (+ F) (k - 1) - seq M (+ F) (k - 1 + 1)\| < x)$
37	1 2 5	serf	$⊢ φ \to seq M (+ F) : Z ⟶ ℂ$
38	37	ad2antrr	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to seq M (+ F) : Z ⟶ ℂ$
39	1	uztrn2	$⊢ (j \in Z \land k - 1 \in ℤ_{\geq j}) \to k - 1 \in Z$
40	24 29 39	syl2an2r	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to k - 1 \in Z$
41	38 40	ffvelrnd	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to seq M (+ F) (k - 1) \in ℂ$
42	1	uztrn2	$⊢ (j + 1 \in Z \land k \in ℤ_{\geq (j + 1)}) \to k \in Z$
43	12 42	sylan	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to k \in Z$
44	38 43	ffvelrnd	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to seq M (+ F) (k) \in ℂ$
45	41 44	abssubd	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to \|seq M (+ F) (k - 1) - seq M (+ F) (k)\| = \|seq M (+ F) (k) - seq M (+ F) (k - 1)\|$
46		eluzelz	$⊢ k \in ℤ_{\geq (j + 1)} \to k \in ℤ$
47	46	adantl	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to k \in ℤ$
48	47	zcnd	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to k \in ℂ$
49		ax-1cn	$⊢ 1 \in ℂ$
50		npcan	$⊢ (k \in ℂ \land 1 \in ℂ) \to k - 1 + 1 = k$
51	48 49 50	sylancl	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to k - 1 + 1 = k$
52	51	fveq2d	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to seq M (+ F) (k - 1 + 1) = seq M (+ F) (k)$
53	52	oveq2d	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to seq M (+ F) (k - 1) - seq M (+ F) (k - 1 + 1) = seq M (+ F) (k - 1) - seq M (+ F) (k)$
54	53	fveq2d	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to \|seq M (+ F) (k - 1) - seq M (+ F) (k - 1 + 1)\| = \|seq M (+ F) (k - 1) - seq M (+ F) (k)\|$
55	2	ad2antrr	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to M \in ℤ$
56		eluzp1p1	$⊢ j \in ℤ_{\geq M} \to j + 1 \in ℤ_{\geq (M + 1)}$
57	25 56	syl	$⊢ (φ \land j \in Z) \to j + 1 \in ℤ_{\geq (M + 1)}$
58		eqid	$⊢ ℤ_{\geq (M + 1)} = ℤ_{\geq (M + 1)}$
59	58	uztrn2	$⊢ (j + 1 \in ℤ_{\geq (M + 1)} \land k \in ℤ_{\geq (j + 1)}) \to k \in ℤ_{\geq (M + 1)}$
60	57 59	sylan	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to k \in ℤ_{\geq (M + 1)}$
61		seqm1	$⊢ (M \in ℤ \land k \in ℤ_{\geq (M + 1)}) \to seq M (+ F) (k) = seq M (+ F) (k - 1) + F (k)$
62	55 60 61	syl2anc	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to seq M (+ F) (k) = seq M (+ F) (k - 1) + F (k)$
63	62	oveq1d	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to seq M (+ F) (k) - seq M (+ F) (k - 1) = seq M (+ F) (k - 1) + F (k) - seq M (+ F) (k - 1)$
64	5	adantlr	$⊢ ((φ \land j \in Z) \land k \in Z) \to F (k) \in ℂ$
65	43 64	syldan	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to F (k) \in ℂ$
66	41 65	pncan2d	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to seq M (+ F) (k - 1) + F (k) - seq M (+ F) (k - 1) = F (k)$
67	63 66	eqtr2d	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to F (k) = seq M (+ F) (k) - seq M (+ F) (k - 1)$
68	67	fveq2d	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to \|F (k)\| = \|seq M (+ F) (k) - seq M (+ F) (k - 1)\|$
69	45 54 68	3eqtr4d	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to \|seq M (+ F) (k - 1) - seq M (+ F) (k - 1 + 1)\| = \|F (k)\|$
70	69	breq1d	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to (\|seq M (+ F) (k - 1) - seq M (+ F) (k - 1 + 1)\| < x \leftrightarrow \|F (k)\| < x)$
71	36 70	sylibd	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq (j + 1)}) \to (\forall m \in ℤ_{\geq j} \|seq M (+ F) (m) - seq M (+ F) (m + 1)\| < x \to \|F (k)\| < x)$
72	71	ralrimdva	$⊢ (φ \land j \in Z) \to (\forall m \in ℤ_{\geq j} \|seq M (+ F) (m) - seq M (+ F) (m + 1)\| < x \to \forall k \in ℤ_{\geq (j + 1)} \|F (k)\| < x)$
73	23 72	syl5	$⊢ (φ \land j \in Z) \to (\forall m \in ℤ_{\geq j} (seq M (+ F) (m) \in ℂ \land \forall k \in ℤ_{\geq m} \|seq M (+ F) (m) - seq M (+ F) (k)\| < x) \to \forall k \in ℤ_{\geq (j + 1)} \|F (k)\| < x)$
74		fveq2	$⊢ n = j + 1 \to ℤ_{\geq n} = ℤ_{\geq (j + 1)}$
75	74	raleqdv	$⊢ n = j + 1 \to (\forall k \in ℤ_{\geq n} \|F (k)\| < x \leftrightarrow \forall k \in ℤ_{\geq (j + 1)} \|F (k)\| < x)$
76	75	rspcev	$⊢ (j + 1 \in Z \land \forall k \in ℤ_{\geq (j + 1)} \|F (k)\| < x) \to \exists n \in Z \forall k \in ℤ_{\geq n} \|F (k)\| < x$
77	12 73 76	syl6an	$⊢ (φ \land j \in Z) \to (\forall m \in ℤ_{\geq j} (seq M (+ F) (m) \in ℂ \land \forall k \in ℤ_{\geq m} \|seq M (+ F) (m) - seq M (+ F) (k)\| < x) \to \exists n \in Z \forall k \in ℤ_{\geq n} \|F (k)\| < x)$
78	77	rexlimdva	$⊢ φ \to (\exists j \in Z \forall m \in ℤ_{\geq j} (seq M (+ F) (m) \in ℂ \land \forall k \in ℤ_{\geq m} \|seq M (+ F) (m) - seq M (+ F) (k)\| < x) \to \exists n \in Z \forall k \in ℤ_{\geq n} \|F (k)\| < x)$
79	78	ralimdv	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall m \in ℤ_{\geq j} (seq M (+ F) (m) \in ℂ \land \forall k \in ℤ_{\geq m} \|seq M (+ F) (m) - seq M (+ F) (k)\| < x) \to \forall x \in ℝ^{+} \exists n \in Z \forall k \in ℤ_{\geq n} \|F (k)\| < x)$
80	10 79	mpd	$⊢ φ \to \forall x \in ℝ^{+} \exists n \in Z \forall k \in ℤ_{\geq n} \|F (k)\| < x$
81		eqidd	$⊢ (φ \land k \in Z) \to F (k) = F (k)$
82	1 2 3 81 5	clim0c	$⊢ φ \to (F ⇝ 0 \leftrightarrow \forall x \in ℝ^{+} \exists n \in Z \forall k \in ℤ_{\geq n} \|F (k)\| < x)$
83	80 82	mpbird	$⊢ φ \to F ⇝ 0$

Metamath Proof Explorer

Theorem serf0

Proof