clim2f

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 . Similar to clim2 , but without the disjoint var constraint F k . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	nf	$⊢ \underline{Ⅎ} k F$
	clim2f.z	$⊢ Z = ℤ_{\geq M}$
	clim2f.m	$⊢ φ \to M \in ℤ$
	clim2f.f	$⊢ φ \to F \in V$
	clim2f.b	$⊢ (φ \land k \in Z) \to F (k) = B$
Assertion	clim2f	$⊢ φ \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		nf	$⊢ \underline{Ⅎ} k F$
2		clim2f.z	$⊢ Z = ℤ_{\geq M}$
3		clim2f.m	$⊢ φ \to M \in ℤ$
4		clim2f.f	$⊢ φ \to F \in V$
5		clim2f.b	$⊢ (φ \land k \in Z) \to F (k) = B$
6		eqidd	$⊢ (φ \land k \in ℤ) \to F (k) = F (k)$
7	1 4 6	climf	$⊢ φ \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)))$
8	2	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
9	5	eleq1d	$⊢ (φ \land k \in Z) \to (F (k) \in ℂ \leftrightarrow B \in ℂ)$
10	5	fvoveq1d	$⊢ (φ \land k \in Z) \to \|F (k) - A\| = \|B - A\|$
11	10	breq1d	$⊢ (φ \land k \in Z) \to (\|F (k) - A\| < x \leftrightarrow \|B - A\| < x)$
12	9 11	anbi12d	$⊢ (φ \land k \in Z) \to ((F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow (B \in ℂ \land \|B - A\| < x))$
13	8 12	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))$
14	13	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))$
15	14	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))$
16	15	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))$
17	2	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))$
18	3 17	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))$
19	16 18	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))$
20	19	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))$
21	20	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)))$
22	7 21	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 clim2f

Proof