lmclim2

Description: A sequence in a metric space converges to a point iff the distance between the point and the elements of the sequence converges to 0. (Contributed by Jeff Madsen, 2-Sep-2009) (Proof shortened by Mario Carneiro, 5-Jun-2014)

	Ref	Expression
Hypotheses	lmclim2.2	$⊢ φ \to D \in Met (X)$
	lmclim2.3	$⊢ φ \to F : ℕ ⟶ X$
	lmclim2.4	$⊢ J = MetOpen (D)$
	lmclim2.5	$⊢ G = (x \in ℕ ⟼ F (x) D Y)$
	lmclim2.6	$⊢ φ \to Y \in X$
Assertion	lmclim2	$⊢ φ \to (F \underset{t}{⇝} (J) Y \leftrightarrow G ⇝ 0)$

Proof

Step	Hyp	Ref	Expression
1		lmclim2.2	$⊢ φ \to D \in Met (X)$
2		lmclim2.3	$⊢ φ \to F : ℕ ⟶ X$
3		lmclim2.4	$⊢ J = MetOpen (D)$
4		lmclim2.5	$⊢ G = (x \in ℕ ⟼ F (x) D Y)$
5		lmclim2.6	$⊢ φ \to Y \in X$
6		metxmet	$⊢ D \in Met (X) \to D \in ∞Met (X)$
7	1 6	syl	$⊢ φ \to D \in ∞Met (X)$
8		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
9		1zzd	$⊢ φ \to 1 \in ℤ$
10		eqidd	$⊢ (φ \land k \in ℕ) \to F (k) = F (k)$
11	3 7 8 9 10 2	lmmbrf	$⊢ φ \to (F \underset{t}{⇝} (J) Y \leftrightarrow (Y \in X \land \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) D Y < x))$
12		nnex	$⊢ ℕ \in V$
13	12	mptex	$⊢ (x \in ℕ ⟼ F (x) D Y) \in V$
14	4 13	eqeltri	$⊢ G \in V$
15	14	a1i	$⊢ φ \to G \in V$
16		fveq2	$⊢ x = k \to F (x) = F (k)$
17	16	oveq1d	$⊢ x = k \to F (x) D Y = F (k) D Y$
18		ovex	$⊢ F (k) D Y \in V$
19	17 4 18	fvmpt	$⊢ k \in ℕ \to G (k) = F (k) D Y$
20	19	adantl	$⊢ (φ \land k \in ℕ) \to G (k) = F (k) D Y$
21	1	adantr	$⊢ (φ \land k \in ℕ) \to D \in Met (X)$
22	2	ffvelrnda	$⊢ (φ \land k \in ℕ) \to F (k) \in X$
23	5	adantr	$⊢ (φ \land k \in ℕ) \to Y \in X$
24		metcl	$⊢ (D \in Met (X) \land F (k) \in X \land Y \in X) \to F (k) D Y \in ℝ$
25	21 22 23 24	syl3anc	$⊢ (φ \land k \in ℕ) \to F (k) D Y \in ℝ$
26	25	recnd	$⊢ (φ \land k \in ℕ) \to F (k) D Y \in ℂ$
27	8 9 15 20 26	clim0c	$⊢ φ \to (G ⇝ 0 \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} \|F (k) D Y\| < x)$
28		eluznn	$⊢ (j \in ℕ \land k \in ℤ_{\geq j}) \to k \in ℕ$
29		metge0	$⊢ (D \in Met (X) \land F (k) \in X \land Y \in X) \to 0 \leq F (k) D Y$
30	21 22 23 29	syl3anc	$⊢ (φ \land k \in ℕ) \to 0 \leq F (k) D Y$
31	25 30	absidd	$⊢ (φ \land k \in ℕ) \to \|F (k) D Y\| = F (k) D Y$
32	31	breq1d	$⊢ (φ \land k \in ℕ) \to (\|F (k) D Y\| < x \leftrightarrow F (k) D Y < x)$
33	28 32	sylan2	$⊢ (φ \land (j \in ℕ \land k \in ℤ_{\geq j})) \to (\|F (k) D Y\| < x \leftrightarrow F (k) D Y < x)$
34	33	anassrs	$⊢ ((φ \land j \in ℕ) \land k \in ℤ_{\geq j}) \to (\|F (k) D Y\| < x \leftrightarrow F (k) D Y < x)$
35	34	ralbidva	$⊢ (φ \land j \in ℕ) \to (\forall k \in ℤ_{\geq j} \|F (k) D Y\| < x \leftrightarrow \forall k \in ℤ_{\geq j} F (k) D Y < x)$
36	35	rexbidva	$⊢ φ \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} \|F (k) D Y\| < x \leftrightarrow \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) D Y < x)$
37	36	ralbidv	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} \|F (k) D Y\| < x \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) D Y < x)$
38	5	biantrurd	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) D Y < x \leftrightarrow (Y \in X \land \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) D Y < x))$
39	27 37 38	3bitrrd	$⊢ φ \to ((Y \in X \land \forall x \in ℝ^{+} \exists j \in ℕ \forall k \in ℤ_{\geq j} F (k) D Y < x) \leftrightarrow G ⇝ 0)$
40	11 39	bitrd	$⊢ φ \to (F \underset{t}{⇝} (J) Y \leftrightarrow G ⇝ 0)$

Metamath Proof Explorer

Theorem lmclim2

Proof