clim2f2

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	clim2f2.p	$⊢ Ⅎ k φ$
	clim2f2.k	$⊢ \underline{Ⅎ} k F$
	clim2f2.z	$⊢ Z = ℤ_{\geq M}$
	clim2f2.m	$⊢ φ \to M \in ℤ$
	clim2f2.f	$⊢ φ \to F \in V$
	clim2f2.b	$⊢ (φ \land k \in Z) \to F (k) = B$
Assertion	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)))$

Proof

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

Proof