lmmcvg

Description: Convergence property of a converging sequence. (Contributed by NM, 1-Jun-2007) (Revised by Mario Carneiro, 1-May-2014)

	Ref	Expression
Hypotheses	lmmbr.2	$⊢ J = MetOpen (D)$
	lmmbr.3	$⊢ φ \to D \in ∞Met (X)$
	lmmbr3.5	$⊢ Z = ℤ_{\geq M}$
	lmmbr3.6	$⊢ φ \to M \in ℤ$
	lmmbrf.7	$⊢ (φ \land k \in Z) \to F (k) = A$
	lmmcvg.8	$⊢ φ \to F \underset{t}{⇝} (J) P$
	lmmcvg.9	$⊢ φ \to R \in ℝ^{+}$
Assertion	lmmcvg	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} (A \in X \land A D P < R)$

Proof

Step	Hyp	Ref	Expression
1		lmmbr.2	$⊢ J = MetOpen (D)$
2		lmmbr.3	$⊢ φ \to D \in ∞Met (X)$
3		lmmbr3.5	$⊢ Z = ℤ_{\geq M}$
4		lmmbr3.6	$⊢ φ \to M \in ℤ$
5		lmmbrf.7	$⊢ (φ \land k \in Z) \to F (k) = A$
6		lmmcvg.8	$⊢ φ \to F \underset{t}{⇝} (J) P$
7		lmmcvg.9	$⊢ φ \to R \in ℝ^{+}$
8		breq2	$⊢ x = R \to (F (k) D P < x \leftrightarrow F (k) D P < R)$
9	8	3anbi3d	$⊢ x = R \to ((k \in dom F \land F (k) \in X \land F (k) D P < x) \leftrightarrow (k \in dom F \land F (k) \in X \land F (k) D P < R))$
10	9	rexralbidv	$⊢ x = R \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x) \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < R))$
11	1 2 3 4	lmmbr3	$⊢ φ \to (F \underset{t}{⇝} (J) P \leftrightarrow (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x)))$
12	6 11	mpbid	$⊢ φ \to (F \in (X ↑_{𝑝𝑚} ℂ) \land P \in X \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x))$
13	12	simp3d	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < x)$
14	10 13 7	rspcdva	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < R)$
15	3	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
16		3simpc	$⊢ (k \in dom F \land F (k) \in X \land F (k) D P < R) \to (F (k) \in X \land F (k) D P < R)$
17	5	eleq1d	$⊢ (φ \land k \in Z) \to (F (k) \in X \leftrightarrow A \in X)$
18	5	oveq1d	$⊢ (φ \land k \in Z) \to F (k) D P = A D P$
19	18	breq1d	$⊢ (φ \land k \in Z) \to (F (k) D P < R \leftrightarrow A D P < R)$
20	17 19	anbi12d	$⊢ (φ \land k \in Z) \to ((F (k) \in X \land F (k) D P < R) \leftrightarrow (A \in X \land A D P < R))$
21	16 20	syl5ib	$⊢ (φ \land k \in Z) \to ((k \in dom F \land F (k) \in X \land F (k) D P < R) \to (A \in X \land A D P < R))$
22	15 21	sylan2	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to ((k \in dom F \land F (k) \in X \land F (k) D P < R) \to (A \in X \land A D P < R))$
23	22	anassrs	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to ((k \in dom F \land F (k) \in X \land F (k) D P < R) \to (A \in X \land A D P < R))$
24	23	ralimdva	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < R) \to \forall k \in ℤ_{\geq j} (A \in X \land A D P < R))$
25	24	reximdva	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (k \in dom F \land F (k) \in X \land F (k) D P < R) \to \exists j \in Z \forall k \in ℤ_{\geq j} (A \in X \land A D P < R))$
26	14 25	mpd	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} (A \in X \land A D P < R)$

Metamath Proof Explorer

Theorem lmmcvg

Proof