climf2

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A . Similar to clim , but without the disjoint var constraint ph k and F k . (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	climf2.1	$⊢ Ⅎ k φ$
	climf2.nf	$⊢ \underline{Ⅎ} k F$
	climf2.f	$⊢ φ \to F \in V$
	climf2.fv	$⊢ (φ \land k \in ℤ) \to F (k) = B$
Assertion	climf2	$⊢ φ \to (F ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x)))$

Proof

Step	Hyp	Ref	Expression
1		climf2.1	$⊢ Ⅎ k φ$
2		climf2.nf	$⊢ \underline{Ⅎ} k F$
3		climf2.f	$⊢ φ \to F \in V$
4		climf2.fv	$⊢ (φ \land k \in ℤ) \to F (k) = B$
5		climrel	$⊢ Rel ⇝$
6	5	brrelex2i	$⊢ F ⇝ A \to A \in V$
7	6	a1i	$⊢ φ \to (F ⇝ A \to A \in V)$
8		elex	$⊢ A \in ℂ \to A \in V$
9	8	adantr	$⊢ (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)) \to A \in V$
10	9	a1i	$⊢ φ \to ((A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)) \to A \in V)$
11		simpr	$⊢ (f = F \land y = A) \to y = A$
12	11	eleq1d	$⊢ (f = F \land y = A) \to (y \in ℂ \leftrightarrow A \in ℂ)$
13		nfv	$⊢ Ⅎ x (f = F \land y = A)$
14	2	nfeq2	$⊢ Ⅎ k f = F$
15		nfv	$⊢ Ⅎ k y = A$
16	14 15	nfan	$⊢ Ⅎ k (f = F \land y = A)$
17		fveq1	$⊢ f = F \to f (k) = F (k)$
18	17	adantr	$⊢ (f = F \land y = A) \to f (k) = F (k)$
19	18	eleq1d	$⊢ (f = F \land y = A) \to (f (k) \in ℂ \leftrightarrow F (k) \in ℂ)$
20		oveq12	$⊢ (f (k) = F (k) \land y = A) \to f (k) - y = F (k) - A$
21	17 20	sylan	$⊢ (f = F \land y = A) \to f (k) - y = F (k) - A$
22	21	fveq2d	$⊢ (f = F \land y = A) \to \|f (k) - y\| = \|F (k) - A\|$
23	22	breq1d	$⊢ (f = F \land y = A) \to (\|f (k) - y\| < x \leftrightarrow \|F (k) - A\| < x)$
24	19 23	anbi12d	$⊢ (f = F \land y = A) \to ((f (k) \in ℂ \land \|f (k) - y\| < x) \leftrightarrow (F (k) \in ℂ \land \|F (k) - A\| < x))$
25	16 24	ralbid	$⊢ (f = F \land y = A) \to (\forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x) \leftrightarrow \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
26	25	rexbidv	$⊢ (f = F \land y = A) \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
27	13 26	ralbid	$⊢ (f = F \land y = A) \to (\forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
28	12 27	anbi12d	$⊢ (f = F \land y = A) \to ((y \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x)) \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)))$
29		df-clim	$⊢ ⇝ = \{⟨f, y⟩ \| (y \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (f (k) \in ℂ \land \|f (k) - y\| < x))\}$
30	28 29	brabga	$⊢ (F \in V \land A \in V) \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)))$
31	30	ex	$⊢ F \in V \to (A \in V \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))))$
32	3 31	syl	$⊢ φ \to (A \in V \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))))$
33	7 10 32	pm5.21ndd	$⊢ φ \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)))$
34		eluzelz	$⊢ k \in ℤ_{\geq j} \to k \in ℤ$
35	4	eleq1d	$⊢ (φ \land k \in ℤ) \to (F (k) \in ℂ \leftrightarrow B \in ℂ)$
36	4	fvoveq1d	$⊢ (φ \land k \in ℤ) \to \|F (k) - A\| = \|B - A\|$
37	36	breq1d	$⊢ (φ \land k \in ℤ) \to (\|F (k) - A\| < x \leftrightarrow \|B - A\| < x)$
38	35 37	anbi12d	$⊢ (φ \land k \in ℤ) \to ((F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow (B \in ℂ \land \|B - A\| < x))$
39	34 38	sylan2	$⊢ (φ \land k \in ℤ_{\geq j}) \to ((F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow (B \in ℂ \land \|B - A\| < x))$
40	1 39	ralbida	$⊢ φ \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))$
41	40	rexbidv	$⊢ φ \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow \exists j \in ℤ \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x))$
42	41	ralbidv	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x))$
43	42	anbi2d	$⊢ φ \to ((A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)) \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x)))$
44	33 43	bitrd	$⊢ φ \to (F ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (B \in ℂ \land \|B - A\| < x)))$

Metamath Proof Explorer

Theorem climf2

Proof