climf

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 F k . (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Hypotheses	climf.nf	$⊢ \underline{Ⅎ} k F$
	climf.f	$⊢ φ \to F \in V$
	climf.fv	$⊢ (φ \land k \in ℤ) \to F (k) = B$
Assertion	climf	$⊢ φ \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		climf.nf	$⊢ \underline{Ⅎ} k F$
2		climf.f	$⊢ φ \to F \in V$
3		climf.fv	$⊢ (φ \land k \in ℤ) \to F (k) = B$
4		climrel	$⊢ Rel ⇝$
5	4	brrelex2i	$⊢ F ⇝ A \to A \in V$
6	5	a1i	$⊢ φ \to (F ⇝ A \to A \in V)$
7		elex	$⊢ A \in ℂ \to A \in V$
8	7	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$
9	8	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)$
10		simpr	$⊢ (f = F \land y = A) \to y = A$
11	10	eleq1d	$⊢ (f = F \land y = A) \to (y \in ℂ \leftrightarrow A \in ℂ)$
12		nfv	$⊢ Ⅎ x (f = F \land y = A)$
13	1	nfeq2	$⊢ Ⅎ k f = F$
14		nfv	$⊢ Ⅎ k y = A$
15	13 14	nfan	$⊢ Ⅎ k (f = F \land y = A)$
16		fveq1	$⊢ f = F \to f (k) = F (k)$
17	16	adantr	$⊢ (f = F \land y = A) \to f (k) = F (k)$
18	17	eleq1d	$⊢ (f = F \land y = A) \to (f (k) \in ℂ \leftrightarrow F (k) \in ℂ)$
19		oveq12	$⊢ (f (k) = F (k) \land y = A) \to f (k) - y = F (k) - A$
20	16 19	sylan	$⊢ (f = F \land y = A) \to f (k) - y = F (k) - A$
21	20	fveq2d	$⊢ (f = F \land y = A) \to \|f (k) - y\| = \|F (k) - A\|$
22	21	breq1d	$⊢ (f = F \land y = A) \to (\|f (k) - y\| < x \leftrightarrow \|F (k) - A\| < x)$
23	18 22	anbi12d	$⊢ (f = F \land y = A) \to ((f (k) \in ℂ \land \|f (k) - y\| < x) \leftrightarrow (F (k) \in ℂ \land \|F (k) - A\| < x))$
24	15 23	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))$
25	24	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))$
26	12 25	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))$
27	11 26	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)))$
28		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))\}$
29	27 28	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)))$
30	29	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))))$
31	2 30	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))))$
32	6 9 31	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)))$
33		eluzelz	$⊢ k \in ℤ_{\geq j} \to k \in ℤ$
34	3	eleq1d	$⊢ (φ \land k \in ℤ) \to (F (k) \in ℂ \leftrightarrow B \in ℂ)$
35	3	fvoveq1d	$⊢ (φ \land k \in ℤ) \to \|F (k) - A\| = \|B - A\|$
36	35	breq1d	$⊢ (φ \land k \in ℤ) \to (\|F (k) - A\| < x \leftrightarrow \|B - A\| < x)$
37	34 36	anbi12d	$⊢ (φ \land k \in ℤ) \to ((F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow (B \in ℂ \land \|B - A\| < x))$
38	33 37	sylan2	$⊢ (φ \land k \in ℤ_{\geq j}) \to ((F (k) \in ℂ \land \|F (k) - A\| < x) \leftrightarrow (B \in ℂ \land \|B - A\| < x))$
39	38	ralbidva	$⊢ φ \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))$
40	39	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))$
41	40	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))$
42	41	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)))$
43	32 42	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 climf

Proof