climi

Description: Convergence of a sequence of complex numbers. (Contributed by NM, 11-Jan-2007) (Revised by Mario Carneiro, 31-Jan-2014)

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

Step	Hyp	Ref	Expression
1		climi.1	$⊢ Z = ℤ_{\geq M}$
2		climi.2	$⊢ φ \to M \in ℤ$
3		climi.3	$⊢ φ \to C \in ℝ^{+}$
4		climi.4	$⊢ (φ \land k \in Z) \to F (k) = B$
5		climi.5	$⊢ φ \to F ⇝ A$
6		breq2	$⊢ x = C \to (\|B - A\| < x \leftrightarrow \|B - A\| < C)$
7	6	anbi2d	$⊢ x = C \to ((B \in ℂ \land \|B - A\| < x) \leftrightarrow (B \in ℂ \land \|B - A\| < C))$
8	7	rexralbidv	$⊢ x = C \to (\exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x) \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < C))$
9		climrel	$⊢ Rel ⇝$
10	9	brrelex1i	$⊢ F ⇝ A \to F \in V$
11	5 10	syl	$⊢ φ \to F \in V$
12	1 2 11 4	clim2	$⊢ φ \to (F ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x)))$
13	5 12	mpbid	$⊢ φ \to (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x))$
14	13	simprd	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x)$
15	8 14 3	rspcdva	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < C)$

Metamath Proof Explorer