Metamath Proof Explorer

Theorem climd

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A . (Contributed by Glauco Siliprandi, 26-Jun-2021)

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

Proof

Step	Hyp	Ref	Expression
1		climd.1	$⊢ Ⅎ k φ$
2		climd.2	$⊢ \underline{Ⅎ} k F$
3		climd.3	$⊢ Z = ℤ_{\geq M}$
4		climd.4	$⊢ φ \to M \in ℤ$
5		climd.5	$⊢ φ \to F ⇝ A$
6		climd.6	$⊢ (φ \land k \in Z) \to F (k) = B$
7		climd.7	$⊢ φ \to X \in ℝ^{+}$
8		climrel	$⊢ Rel ⇝$
9	8	brrelex1i	$⊢ F ⇝ A \to F \in V$
10	5 9	syl	$⊢ φ \to F \in V$
11	1 2 3 4 10 6	clim2f2	$⊢ φ \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)))$
12	5 11	mpbid	$⊢ φ \to (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x))$
13	12	simprd	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x)$
14		breq2	$⊢ x = X \to (\|B - A\| < x \leftrightarrow \|B - A\| < X)$
15	14	anbi2d	$⊢ x = X \to ((B \in ℂ \land \|B - A\| < x) \leftrightarrow (B \in ℂ \land \|B - A\| < X))$
16	15	rexralbidv	$⊢ x = X \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\| < X))$
17	16	rspcva	$⊢ (X \in ℝ^{+} \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x)) \to \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < X)$
18	7 13 17	syl2anc	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < X)$