2clim

Description: If two sequences converge to each other, they converge to the same limit. (Contributed by NM, 24-Dec-2005) (Proof shortened by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Hypotheses	2clim.1	$⊢ Z = ℤ_{\geq M}$
	2clim.2	$⊢ φ \to M \in ℤ$
	2clim.3	$⊢ φ \to G \in V$
	2clim.5	$⊢ (φ \land k \in Z) \to G (k) \in ℂ$
	2clim.6	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - G (k)\| < x$
	2clim.7	$⊢ φ \to F ⇝ A$
Assertion	2clim	$⊢ φ \to G ⇝ A$

Proof

Step	Hyp	Ref	Expression
1		2clim.1	$⊢ Z = ℤ_{\geq M}$
2		2clim.2	$⊢ φ \to M \in ℤ$
3		2clim.3	$⊢ φ \to G \in V$
4		2clim.5	$⊢ (φ \land k \in Z) \to G (k) \in ℂ$
5		2clim.6	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - G (k)\| < x$
6		2clim.7	$⊢ φ \to F ⇝ A$
7		rphalfcl	$⊢ y \in ℝ^{+} \to \frac{y}{2} \in ℝ^{+}$
8		breq2	$⊢ x = \frac{y}{2} \to (\|F (k) - G (k)\| < x \leftrightarrow \|F (k) - G (k)\| < \frac{y}{2})$
9	8	rexralbidv	$⊢ x = \frac{y}{2} \to (\exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - G (k)\| < x \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - G (k)\| < \frac{y}{2})$
10	9	rspccva	$⊢ (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - G (k)\| < x \land \frac{y}{2} \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - G (k)\| < \frac{y}{2}$
11	5 7 10	syl2an	$⊢ (φ \land y \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - G (k)\| < \frac{y}{2}$
12	2	adantr	$⊢ (φ \land y \in ℝ^{+}) \to M \in ℤ$
13	7	adantl	$⊢ (φ \land y \in ℝ^{+}) \to \frac{y}{2} \in ℝ^{+}$
14		eqidd	$⊢ ((φ \land y \in ℝ^{+}) \land k \in Z) \to F (k) = F (k)$
15	6	adantr	$⊢ (φ \land y \in ℝ^{+}) \to F ⇝ A$
16	1 12 13 14 15	climi	$⊢ (φ \land y \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < \frac{y}{2})$
17	1	rexanuz2	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} (\|F (k) - G (k)\| < \frac{y}{2} \land (F (k) \in ℂ \land \|F (k) - A\| < \frac{y}{2})) \leftrightarrow (\exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - G (k)\| < \frac{y}{2} \land \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < \frac{y}{2}))$
18	11 16 17	sylanbrc	$⊢ (φ \land y \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} (\|F (k) - G (k)\| < \frac{y}{2} \land (F (k) \in ℂ \land \|F (k) - A\| < \frac{y}{2}))$
19	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
20		an12	$⊢ (\|F (k) - G (k)\| < \frac{y}{2} \land (F (k) \in ℂ \land \|F (k) - A\| < \frac{y}{2})) \leftrightarrow (F (k) \in ℂ \land (\|F (k) - G (k)\| < \frac{y}{2} \land \|F (k) - A\| < \frac{y}{2}))$
21		simprr	$⊢ ((φ \land y \in ℝ^{+}) \land (k \in Z \land F (k) \in ℂ)) \to F (k) \in ℂ$
22	4	ad2ant2r	$⊢ ((φ \land y \in ℝ^{+}) \land (k \in Z \land F (k) \in ℂ)) \to G (k) \in ℂ$
23	21 22	abssubd	$⊢ ((φ \land y \in ℝ^{+}) \land (k \in Z \land F (k) \in ℂ)) \to \|F (k) - G (k)\| = \|G (k) - F (k)\|$
24	23	breq1d	$⊢ ((φ \land y \in ℝ^{+}) \land (k \in Z \land F (k) \in ℂ)) \to (\|F (k) - G (k)\| < \frac{y}{2} \leftrightarrow \|G (k) - F (k)\| < \frac{y}{2})$
25	24	anbi1d	$⊢ ((φ \land y \in ℝ^{+}) \land (k \in Z \land F (k) \in ℂ)) \to ((\|F (k) - G (k)\| < \frac{y}{2} \land \|F (k) - A\| < \frac{y}{2}) \leftrightarrow (\|G (k) - F (k)\| < \frac{y}{2} \land \|F (k) - A\| < \frac{y}{2}))$
26		climcl	$⊢ F ⇝ A \to A \in ℂ$
27	6 26	syl	$⊢ φ \to A \in ℂ$
28	27	ad2antrr	$⊢ ((φ \land y \in ℝ^{+}) \land (k \in Z \land F (k) \in ℂ)) \to A \in ℂ$
29		rpre	$⊢ y \in ℝ^{+} \to y \in ℝ$
30	29	ad2antlr	$⊢ ((φ \land y \in ℝ^{+}) \land (k \in Z \land F (k) \in ℂ)) \to y \in ℝ$
31		abs3lem	$⊢ ((G (k) \in ℂ \land A \in ℂ) \land (F (k) \in ℂ \land y \in ℝ)) \to ((\|G (k) - F (k)\| < \frac{y}{2} \land \|F (k) - A\| < \frac{y}{2}) \to \|G (k) - A\| < y)$
32	22 28 21 30 31	syl22anc	$⊢ ((φ \land y \in ℝ^{+}) \land (k \in Z \land F (k) \in ℂ)) \to ((\|G (k) - F (k)\| < \frac{y}{2} \land \|F (k) - A\| < \frac{y}{2}) \to \|G (k) - A\| < y)$
33	25 32	sylbid	$⊢ ((φ \land y \in ℝ^{+}) \land (k \in Z \land F (k) \in ℂ)) \to ((\|F (k) - G (k)\| < \frac{y}{2} \land \|F (k) - A\| < \frac{y}{2}) \to \|G (k) - A\| < y)$
34	33	anassrs	$⊢ (((φ \land y \in ℝ^{+}) \land k \in Z) \land F (k) \in ℂ) \to ((\|F (k) - G (k)\| < \frac{y}{2} \land \|F (k) - A\| < \frac{y}{2}) \to \|G (k) - A\| < y)$
35	34	expimpd	$⊢ ((φ \land y \in ℝ^{+}) \land k \in Z) \to ((F (k) \in ℂ \land (\|F (k) - G (k)\| < \frac{y}{2} \land \|F (k) - A\| < \frac{y}{2})) \to \|G (k) - A\| < y)$
36	20 35	biimtrid	$⊢ ((φ \land y \in ℝ^{+}) \land k \in Z) \to ((\|F (k) - G (k)\| < \frac{y}{2} \land (F (k) \in ℂ \land \|F (k) - A\| < \frac{y}{2})) \to \|G (k) - A\| < y)$
37	19 36	sylan2	$⊢ ((φ \land y \in ℝ^{+}) \land (j \in Z \land k \in ℤ_{\geq j})) \to ((\|F (k) - G (k)\| < \frac{y}{2} \land (F (k) \in ℂ \land \|F (k) - A\| < \frac{y}{2})) \to \|G (k) - A\| < y)$
38	37	anassrs	$⊢ (((φ \land y \in ℝ^{+}) \land j \in Z) \land k \in ℤ_{\geq j}) \to ((\|F (k) - G (k)\| < \frac{y}{2} \land (F (k) \in ℂ \land \|F (k) - A\| < \frac{y}{2})) \to \|G (k) - A\| < y)$
39	38	ralimdva	$⊢ ((φ \land y \in ℝ^{+}) \land j \in Z) \to (\forall k \in ℤ_{\geq j} (\|F (k) - G (k)\| < \frac{y}{2} \land (F (k) \in ℂ \land \|F (k) - A\| < \frac{y}{2})) \to \forall k \in ℤ_{\geq j} \|G (k) - A\| < y)$
40	39	reximdva	$⊢ (φ \land y \in ℝ^{+}) \to (\exists j \in Z \forall k \in ℤ_{\geq j} (\|F (k) - G (k)\| < \frac{y}{2} \land (F (k) \in ℂ \land \|F (k) - A\| < \frac{y}{2})) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|G (k) - A\| < y)$
41	18 40	mpd	$⊢ (φ \land y \in ℝ^{+}) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|G (k) - A\| < y$
42	41	ralrimiva	$⊢ φ \to \forall y \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|G (k) - A\| < y$
43		eqidd	$⊢ (φ \land k \in Z) \to G (k) = G (k)$
44	1 2 3 43 27 4	clim2c	$⊢ φ \to (G ⇝ A \leftrightarrow \forall y \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|G (k) - A\| < y)$
45	42 44	mpbird	$⊢ φ \to G ⇝ A$

Metamath Proof Explorer

Theorem 2clim

Proof