clim2

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A , with more general quantifier restrictions than clim . (Contributed by NM, 6-Jan-2007) (Revised by Mario Carneiro, 31-Jan-2014)

	Ref	Expression
Hypotheses	clim2.1	$⊢ Z = ℤ_{\geq M}$
	clim2.2	$⊢ φ \to M \in ℤ$
	clim2.3	$⊢ φ \to F \in V$
	clim2.4	$⊢ (φ \land k \in Z) \to F (k) = B$
Assertion	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)))$

Proof

Step	Hyp	Ref	Expression
1		clim2.1	$⊢ Z = ℤ_{\geq M}$
2		clim2.2	$⊢ φ \to M \in ℤ$
3		clim2.3	$⊢ φ \to F \in V$
4		clim2.4	$⊢ (φ \land k \in Z) \to F (k) = B$
5		eqidd	$⊢ (φ \land k \in ℤ) \to F (k) = F (k)$
6	3 5	clim	$⊢ φ \to (F ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)))$
7	1	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
8	4	eleq1d	$⊢ (φ \land k \in Z) \to (F (k) \in ℂ \leftrightarrow B \in ℂ)$
9	4	fvoveq1d	$⊢ (φ \land k \in Z) \to \|F (k) - A\| = \|B - A\|$
10	9	breq1d	$⊢ (φ \land k \in Z) \to (\|F (k) - A\| < x \leftrightarrow \|B - A\| < x)$
11	8 10	anbi12d	$⊢ (φ \land k \in Z) \to ((F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow (B \in ℂ \land \|B - A\| < x))$
12	7 11	sylan2	$⊢ (φ \land (j \in Z \land k \in ℤ_{\geq j})) \to ((F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow (B \in ℂ \land \|B - A\| < x))$
13	12	anassrs	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to ((F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow (B \in ℂ \land \|B - A\| < x))$
14	13	ralbidva	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x))$
15	14	rexbidva	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x))$
16	1	rexuz3	$⊢ M \in ℤ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
17	2 16	syl	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
18	15 17	bitr3d	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
19	18	ralbidv	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
20	19	anbi2d	$⊢ φ \to ((A \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x)) \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)))$
21	6 20	bitr4d	$⊢ φ \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)))$

Metamath Proof Explorer

Theorem clim2

Proof