climuzlem

Description: Express the predicate: The limit of complex number sequence F is A , or F converges to A . (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	climuzlem.1	$⊢ φ \to M \in ℤ$
	climuzlem.2	$⊢ Z = ℤ_{\geq M}$
	climuzlem.3	$⊢ φ \to F : Z ⟶ ℂ$
Assertion	climuzlem	$⊢ φ \to (F ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x))$

Proof

Step	Hyp	Ref	Expression
1		climuzlem.1	$⊢ φ \to M \in ℤ$
2		climuzlem.2	$⊢ Z = ℤ_{\geq M}$
3		climuzlem.3	$⊢ φ \to F : Z ⟶ ℂ$
4		climcl	$⊢ F ⇝ A \to A \in ℂ$
5	4	adantl	$⊢ (φ \land F ⇝ A) \to A \in ℂ$
6		id	$⊢ F ⇝ A \to F ⇝ A$
7		climrel	$⊢ Rel ⇝$
8	7	brrelex1i	$⊢ F ⇝ A \to F \in V$
9		eqidd	$⊢ (F ⇝ A \land k \in ℤ) \to F (k) = F (k)$
10	8 9	clim	$⊢ F ⇝ A \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)))$
11	6 10	mpbid	$⊢ F ⇝ A \to (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
12	11	simprd	$⊢ F ⇝ A \to \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)$
13	12	adantl	$⊢ (φ \land F ⇝ A) \to \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)$
14		simpr	$⊢ (φ \land \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)) \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)$
15	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))$
16	1 15	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))$
17	16	adantr	$⊢ (φ \land \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)) \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	14 17	mpbird	$⊢ (φ \land \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)) \to \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)$
19		simpr	$⊢ (F (k) \in ℂ \land \|F (k) - A\| < x) \to \|F (k) - A\| < x$
20	19	ralimi	$⊢ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \to \forall k \in ℤ_{\geq j} \|F (k) - A\| < x$
21	20	reximi	$⊢ \exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x$
22	21	a1i	$⊢ (φ \land \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)) \to (\exists j \in Z \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x)$
23	18 22	mpd	$⊢ (φ \land \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x$
24	23	ex	$⊢ φ \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x)$
25	24	adantr	$⊢ (φ \land x \in ℝ^{+}) \to (\exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \to \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x)$
26	25	ralimdva	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x)$
27	26	adantr	$⊢ (φ \land F ⇝ A) \to (\forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x) \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x)$
28	13 27	mpd	$⊢ (φ \land F ⇝ A) \to \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x$
29	5 28	jca	$⊢ (φ \land F ⇝ A) \to (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x)$
30		simprl	$⊢ (φ \land (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x)) \to A \in ℂ$
31		nfv	$⊢ Ⅎ j φ$
32		nfre1	$⊢ Ⅎ j \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)$
33	2	uzssz2	$⊢ Z \subseteq ℤ$
34	33	sseli	$⊢ j \in Z \to j \in ℤ$
35	34	3ad2ant2	$⊢ (φ \land j \in Z \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \to j \in ℤ$
36		simpll	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to φ$
37	2	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
38	37	adantll	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to k \in Z$
39	3	ffvelrnda	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
40	36 38 39	syl2anc	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) \in ℂ$
41	40	adantr	$⊢ (((φ \land j \in Z) \land k \in ℤ_{\geq j}) \land \|F (k) - A\| < x) \to F (k) \in ℂ$
42		simpr	$⊢ (((φ \land j \in Z) \land k \in ℤ_{\geq j}) \land \|F (k) - A\| < x) \to \|F (k) - A\| < x$
43	41 42	jca	$⊢ (((φ \land j \in Z) \land k \in ℤ_{\geq j}) \land \|F (k) - A\| < x) \to (F (k) \in ℂ \land \|F (k) - A\| < x)$
44	43	ex	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to (\|F (k) - A\| < x \to (F (k) \in ℂ \land \|F (k) - A\| < x))$
45	44	ralimdva	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} \|F (k) - A\| < x \to \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
46	45	3impia	$⊢ (φ \land j \in Z \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \to \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)$
47		rspe	$⊢ (j \in ℤ \land \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)) \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)$
48	35 46 47	syl2anc	$⊢ (φ \land j \in Z \land \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)$
49	48	3exp	$⊢ φ \to (j \in Z \to (\forall k \in ℤ_{\geq j} \|F (k) - A\| < x \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)))$
50	31 32 49	rexlimd	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x \to \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
51	50	ralimdv	$⊢ φ \to (\forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x \to \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
52	51	imp	$⊢ (φ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x) \to \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)$
53	52	adantrl	$⊢ (φ \land (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x)) \to \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x)$
54	30 53	jca	$⊢ (φ \land (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x)) \to (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall k \in ℤ_{\geq j} (F (k) \in ℂ \land \|F (k) - A\| < x))$
55	2	fvexi	$⊢ Z \in V$
56	55	a1i	$⊢ φ \to Z \in V$
57	3 56	fexd	$⊢ φ \to F \in V$
58		eqidd	$⊢ (φ \land k \in ℤ) \to F (k) = F (k)$
59	57 58	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)))$
60	59	adantr	$⊢ (φ \land (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x)) \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)))$
61	54 60	mpbird	$⊢ (φ \land (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x)) \to F ⇝ A$
62	29 61	impbida	$⊢ φ \to (F ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in Z \forall k \in ℤ_{\geq j} \|F (k) - A\| < x))$

Metamath Proof Explorer

Theorem climuzlem

Proof