lmle

Description: If the distance from each member of a converging sequence to a given point is less than or equal to a given amount, so is the convergence value. (Contributed by NM, 23-Dec-2007) (Proof shortened by Mario Carneiro, 1-May-2014)

	Ref	Expression
Hypotheses	lmle.1	$⊢ Z = ℤ_{\geq M}$
	lmle.3	$⊢ J = MetOpen (D)$
	lmle.4	$⊢ φ \to D \in ∞Met (X)$
	lmle.6	$⊢ φ \to M \in ℤ$
	lmle.7	$⊢ φ \to F \underset{t}{⇝} (J) P$
	lmle.8	$⊢ φ \to Q \in X$
	lmle.9	$⊢ φ \to R \in ℝ^{*}$
	lmle.10	$⊢ (φ \land k \in Z) \to Q D F (k) \leq R$
Assertion	lmle	$⊢ φ \to Q D P \leq R$

Proof

Step	Hyp	Ref	Expression
1		lmle.1	$⊢ Z = ℤ_{\geq M}$
2		lmle.3	$⊢ J = MetOpen (D)$
3		lmle.4	$⊢ φ \to D \in ∞Met (X)$
4		lmle.6	$⊢ φ \to M \in ℤ$
5		lmle.7	$⊢ φ \to F \underset{t}{⇝} (J) P$
6		lmle.8	$⊢ φ \to Q \in X$
7		lmle.9	$⊢ φ \to R \in ℝ^{*}$
8		lmle.10	$⊢ (φ \land k \in Z) \to Q D F (k) \leq R$
9	2	mopntopon	$⊢ D \in ∞Met (X) \to J \in TopOn (X)$
10	3 9	syl	$⊢ φ \to J \in TopOn (X)$
11		lmrel	$⊢ Rel \underset{t}{⇝} (J)$
12		releldm	$⊢ (Rel \underset{t}{⇝} (J) \land F \underset{t}{⇝} (J) P) \to F \in dom \underset{t}{⇝} (J)$
13	11 5 12	sylancr	$⊢ φ \to F \in dom \underset{t}{⇝} (J)$
14	1 10 4 13	lmff	$⊢ φ \to \exists j \in Z ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X$
15		eqid	$⊢ ℤ_{\geq j} = ℤ_{\geq j}$
16	10	adantr	$⊢ (φ \land (j \in Z \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)) \to J \in TopOn (X)$
17		simprl	$⊢ (φ \land (j \in Z \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)) \to j \in Z$
18	17 1	eleqtrdi	$⊢ (φ \land (j \in Z \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)) \to j \in ℤ_{\geq M}$
19		eluzelz	$⊢ j \in ℤ_{\geq M} \to j \in ℤ$
20	18 19	syl	$⊢ (φ \land (j \in Z \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)) \to j \in ℤ$
21	5	adantr	$⊢ (φ \land (j \in Z \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)) \to F \underset{t}{⇝} (J) P$
22		oveq2	$⊢ x = F (k) \to Q D x = Q D F (k)$
23	22	breq1d	$⊢ x = F (k) \to (Q D x \leq R \leftrightarrow Q D F (k) \leq R)$
24		fvres	$⊢ k \in ℤ_{\geq j} \to ({F ↾}_{ℤ_{\geq j}}) (k) = F (k)$
25	24	adantl	$⊢ ((φ \land (j \in Z \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)) \land k \in ℤ_{\geq j}) \to ({F ↾}_{ℤ_{\geq j}}) (k) = F (k)$
26		simprr	$⊢ (φ \land (j \in Z \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)) \to ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X$
27	26	ffvelrnda	$⊢ ((φ \land (j \in Z \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)) \land k \in ℤ_{\geq j}) \to ({F ↾}_{ℤ_{\geq j}}) (k) \in X$
28	25 27	eqeltrrd	$⊢ ((φ \land (j \in Z \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)) \land k \in ℤ_{\geq j}) \to F (k) \in X$
29	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
30	17 29	sylan	$⊢ ((φ \land (j \in Z \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)) \land k \in ℤ_{\geq j}) \to k \in Z$
31	8	adantlr	$⊢ ((φ \land (j \in Z \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)) \land k \in Z) \to Q D F (k) \leq R$
32	30 31	syldan	$⊢ ((φ \land (j \in Z \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)) \land k \in ℤ_{\geq j}) \to Q D F (k) \leq R$
33	23 28 32	elrabd	$⊢ ((φ \land (j \in Z \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)) \land k \in ℤ_{\geq j}) \to F (k) \in \{x \in X \| Q D x \leq R\}$
34		eqid	$⊢ \{x \in X \| Q D x \leq R\} = \{x \in X \| Q D x \leq R\}$
35	2 34	blcld	$⊢ (D \in ∞Met (X) \land Q \in X \land R \in ℝ^{*}) \to \{x \in X \| Q D x \leq R\} \in Clsd (J)$
36	3 6 7 35	syl3anc	$⊢ φ \to \{x \in X \| Q D x \leq R\} \in Clsd (J)$
37	36	adantr	$⊢ (φ \land (j \in Z \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)) \to \{x \in X \| Q D x \leq R\} \in Clsd (J)$
38	15 16 20 21 33 37	lmcld	$⊢ (φ \land (j \in Z \land ({F ↾}_{ℤ_{\geq j}}) : ℤ_{\geq j} ⟶ X)) \to P \in \{x \in X \| Q D x \leq R\}$
39	14 38	rexlimddv	$⊢ φ \to P \in \{x \in X \| Q D x \leq R\}$
40		oveq2	$⊢ x = P \to Q D x = Q D P$
41	40	breq1d	$⊢ x = P \to (Q D x \leq R \leftrightarrow Q D P \leq R)$
42	41	elrab	$⊢ P \in \{x \in X \| Q D x \leq R\} \leftrightarrow (P \in X \land Q D P \leq R)$
43	42	simprbi	$⊢ P \in \{x \in X \| Q D x \leq R\} \to Q D P \leq R$
44	39 43	syl	$⊢ φ \to Q D P \leq R$

Metamath Proof Explorer

Theorem lmle

Proof