climsuse

Description: A subsequence G of a converging sequence F , converges to the same limit. I is the strictly increasing and it is used to index the subsequence. (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypotheses	climsuse.1	$⊢ Ⅎ k φ$
	climsuse.3	$⊢ \underline{Ⅎ} k F$
	climsuse.2	$⊢ \underline{Ⅎ} k G$
	climsuse.4	$⊢ \underline{Ⅎ} k I$
	climsuse.5	$⊢ Z = ℤ_{\geq M}$
	climsuse.6	$⊢ φ \to M \in ℤ$
	climsuse.7	$⊢ φ \to F \in X$
	climsuse.8	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
	climsuse.9	$⊢ φ \to F ⇝ A$
	climsuse.10	$⊢ φ \to I (M) \in Z$
	climsuse.11	$⊢ (φ \land k \in Z) \to I (k + 1) \in ℤ_{\geq (I (k) + 1)}$
	climsuse.12	$⊢ φ \to G \in Y$
	climsuse.13	$⊢ (φ \land k \in Z) \to G (k) = F (I (k))$
Assertion	climsuse	$⊢ φ \to G ⇝ A$

Proof

Step	Hyp	Ref	Expression
1		climsuse.1	$⊢ Ⅎ k φ$
2		climsuse.3	$⊢ \underline{Ⅎ} k F$
3		climsuse.2	$⊢ \underline{Ⅎ} k G$
4		climsuse.4	$⊢ \underline{Ⅎ} k I$
5		climsuse.5	$⊢ Z = ℤ_{\geq M}$
6		climsuse.6	$⊢ φ \to M \in ℤ$
7		climsuse.7	$⊢ φ \to F \in X$
8		climsuse.8	$⊢ (φ \land k \in Z) \to F (k) \in ℂ$
9		climsuse.9	$⊢ φ \to F ⇝ A$
10		climsuse.10	$⊢ φ \to I (M) \in Z$
11		climsuse.11	$⊢ (φ \land k \in Z) \to I (k + 1) \in ℤ_{\geq (I (k) + 1)}$
12		climsuse.12	$⊢ φ \to G \in Y$
13		climsuse.13	$⊢ (φ \land k \in Z) \to G (k) = F (I (k))$
14		climcl	$⊢ F ⇝ A \to A \in ℂ$
15	9 14	syl	$⊢ φ \to A \in ℂ$
16		nfv	$⊢ Ⅎ x φ$
17		simpllr	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \land M \leq j) \to j \in ℤ$
18	6	ad4antr	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \land \neg M \leq j) \to M \in ℤ$
19	17 18	ifclda	$⊢ (((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \to if (M \leq j, j, M) \in ℤ$
20		nfv	$⊢ Ⅎ i ((φ \land x \in ℝ^{+}) \land j \in ℤ)$
21		nfra1	$⊢ Ⅎ i \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)$
22	20 21	nfan	$⊢ Ⅎ i (((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x))$
23		simp-4l	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to φ$
24		simpllr	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to j \in ℤ$
25	23 24	jca	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to (φ \land j \in ℤ)$
26		simpr	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to i \in ℤ_{\geq if (M \leq j, j, M)}$
27		simpr	$⊢ ((φ \land j \in ℤ) \land M \leq j) \to M \leq j$
28	6	anim1i	$⊢ (φ \land j \in ℤ) \to (M \in ℤ \land j \in ℤ)$
29	28	adantr	$⊢ ((φ \land j \in ℤ) \land M \leq j) \to (M \in ℤ \land j \in ℤ)$
30		eluz	$⊢ (M \in ℤ \land j \in ℤ) \to (j \in ℤ_{\geq M} \leftrightarrow M \leq j)$
31	29 30	syl	$⊢ ((φ \land j \in ℤ) \land M \leq j) \to (j \in ℤ_{\geq M} \leftrightarrow M \leq j)$
32	27 31	mpbird	$⊢ ((φ \land j \in ℤ) \land M \leq j) \to j \in ℤ_{\geq M}$
33		simpll	$⊢ ((φ \land j \in ℤ) \land \neg M \leq j) \to φ$
34		uzid	$⊢ M \in ℤ \to M \in ℤ_{\geq M}$
35	33 6 34	3syl	$⊢ ((φ \land j \in ℤ) \land \neg M \leq j) \to M \in ℤ_{\geq M}$
36	32 35	ifclda	$⊢ (φ \land j \in ℤ) \to if (M \leq j, j, M) \in ℤ_{\geq M}$
37		uzss	$⊢ if (M \leq j, j, M) \in ℤ_{\geq M} \to ℤ_{\geq if (M \leq j, j, M)} \subseteq ℤ_{\geq M}$
38	36 37	syl	$⊢ (φ \land j \in ℤ) \to ℤ_{\geq if (M \leq j, j, M)} \subseteq ℤ_{\geq M}$
39	38 5	sseqtrrdi	$⊢ (φ \land j \in ℤ) \to ℤ_{\geq if (M \leq j, j, M)} \subseteq Z$
40	39	sseld	$⊢ (φ \land j \in ℤ) \to (i \in ℤ_{\geq if (M \leq j, j, M)} \to i \in Z)$
41	25 26 40	sylc	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to i \in Z$
42		nfv	$⊢ Ⅎ k i \in Z$
43	1 42	nfan	$⊢ Ⅎ k (φ \land i \in Z)$
44		nfcv	$⊢ \underline{Ⅎ} k i$
45	3 44	nffv	$⊢ \underline{Ⅎ} k G (i)$
46	4 44	nffv	$⊢ \underline{Ⅎ} k I (i)$
47	2 46	nffv	$⊢ \underline{Ⅎ} k F (I (i))$
48	45 47	nfeq	$⊢ Ⅎ k G (i) = F (I (i))$
49	43 48	nfim	$⊢ Ⅎ k ((φ \land i \in Z) \to G (i) = F (I (i)))$
50		eleq1	$⊢ k = i \to (k \in Z \leftrightarrow i \in Z)$
51	50	anbi2d	$⊢ k = i \to ((φ \land k \in Z) \leftrightarrow (φ \land i \in Z))$
52		fveq2	$⊢ k = i \to G (k) = G (i)$
53		2fveq3	$⊢ k = i \to F (I (k)) = F (I (i))$
54	52 53	eqeq12d	$⊢ k = i \to (G (k) = F (I (k)) \leftrightarrow G (i) = F (I (i)))$
55	51 54	imbi12d	$⊢ k = i \to (((φ \land k \in Z) \to G (k) = F (I (k))) \leftrightarrow ((φ \land i \in Z) \to G (i) = F (I (i))))$
56	49 55 13	chvarfv	$⊢ (φ \land i \in Z) \to G (i) = F (I (i))$
57	5	eleq2i	$⊢ i \in Z \leftrightarrow i \in ℤ_{\geq M}$
58	57	bilani	$⊢ (φ \land i \in Z) \to i \in ℤ_{\geq M}$
59		uzss	$⊢ i \in ℤ_{\geq M} \to ℤ_{\geq i} \subseteq ℤ_{\geq M}$
60	58 59	syl	$⊢ (φ \land i \in Z) \to ℤ_{\geq i} \subseteq ℤ_{\geq M}$
61		nfcv	$⊢ \underline{Ⅎ} k (i + 1)$
62	4 61	nffv	$⊢ \underline{Ⅎ} k I (i + 1)$
63		nfcv	$⊢ \underline{Ⅎ} k ℤ_{\geq}$
64		nfcv	$⊢ \underline{Ⅎ} k +$
65		nfcv	$⊢ \underline{Ⅎ} k 1$
66	46 64 65	nfov	$⊢ \underline{Ⅎ} k (I (i) + 1)$
67	63 66	nffv	$⊢ \underline{Ⅎ} k ℤ_{\geq (I (i) + 1)}$
68	62 67	nfel	$⊢ Ⅎ k I (i + 1) \in ℤ_{\geq (I (i) + 1)}$
69	43 68	nfim	$⊢ Ⅎ k ((φ \land i \in Z) \to I (i + 1) \in ℤ_{\geq (I (i) + 1)})$
70		fvoveq1	$⊢ k = i \to I (k + 1) = I (i + 1)$
71		fveq2	$⊢ k = i \to I (k) = I (i)$
72	71	fvoveq1d	$⊢ k = i \to ℤ_{\geq (I (k) + 1)} = ℤ_{\geq (I (i) + 1)}$
73	70 72	eleq12d	$⊢ k = i \to (I (k + 1) \in ℤ_{\geq (I (k) + 1)} \leftrightarrow I (i + 1) \in ℤ_{\geq (I (i) + 1)})$
74	51 73	imbi12d	$⊢ k = i \to (((φ \land k \in Z) \to I (k + 1) \in ℤ_{\geq (I (k) + 1)}) \leftrightarrow ((φ \land i \in Z) \to I (i + 1) \in ℤ_{\geq (I (i) + 1)}))$
75	69 74 11	chvarfv	$⊢ (φ \land i \in Z) \to I (i + 1) \in ℤ_{\geq (I (i) + 1)}$
76	5 6 10 75	climsuselem1	$⊢ (φ \land i \in Z) \to I (i) \in ℤ_{\geq i}$
77	60 76	sseldd	$⊢ (φ \land i \in Z) \to I (i) \in ℤ_{\geq M}$
78	77 5	eleqtrrdi	$⊢ (φ \land i \in Z) \to I (i) \in Z$
79	78	ex	$⊢ φ \to (i \in Z \to I (i) \in Z)$
80	79	imdistani	$⊢ (φ \land i \in Z) \to (φ \land I (i) \in Z)$
81	42	nfci	$⊢ \underline{Ⅎ} k Z$
82	46 81	nfel	$⊢ Ⅎ k I (i) \in Z$
83	1 82	nfan	$⊢ Ⅎ k (φ \land I (i) \in Z)$
84	47	nfel1	$⊢ Ⅎ k F (I (i)) \in ℂ$
85	83 84	nfim	$⊢ Ⅎ k ((φ \land I (i) \in Z) \to F (I (i)) \in ℂ)$
86		eleq1	$⊢ k = I (i) \to (k \in Z \leftrightarrow I (i) \in Z)$
87	86	anbi2d	$⊢ k = I (i) \to ((φ \land k \in Z) \leftrightarrow (φ \land I (i) \in Z))$
88		fveq2	$⊢ k = I (i) \to F (k) = F (I (i))$
89	88	eleq1d	$⊢ k = I (i) \to (F (k) \in ℂ \leftrightarrow F (I (i)) \in ℂ)$
90	87 89	imbi12d	$⊢ k = I (i) \to (((φ \land k \in Z) \to F (k) \in ℂ) \leftrightarrow ((φ \land I (i) \in Z) \to F (I (i)) \in ℂ))$
91	46 85 90 8	vtoclgf	$⊢ I (i) \in Z \to ((φ \land I (i) \in Z) \to F (I (i)) \in ℂ)$
92	78 80 91	sylc	$⊢ (φ \land i \in Z) \to F (I (i)) \in ℂ$
93	56 92	eqeltrd	$⊢ (φ \land i \in Z) \to G (i) \in ℂ$
94	23 41 93	syl2anc	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to G (i) \in ℂ$
95	23 41 56	syl2anc	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to G (i) = F (I (i))$
96	95	fvoveq1d	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to \|G (i) - A\| = \|F (I (i)) - A\|$
97		fveq2	$⊢ i = h \to F (i) = F (h)$
98	97	eleq1d	$⊢ i = h \to (F (i) \in ℂ \leftrightarrow F (h) \in ℂ)$
99	97	fvoveq1d	$⊢ i = h \to \|F (i) - A\| = \|F (h) - A\|$
100	99	breq1d	$⊢ i = h \to (\|F (i) - A\| < x \leftrightarrow \|F (h) - A\| < x)$
101	98 100	anbi12d	$⊢ i = h \to ((F (i) \in ℂ \land \|F (i) - A\| < x) \leftrightarrow (F (h) \in ℂ \land \|F (h) - A\| < x))$
102	101	cbvralvw	$⊢ \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x) \leftrightarrow \forall h \in ℤ_{\geq j} (F (h) \in ℂ \land \|F (h) - A\| < x)$
103	102	biimpi	$⊢ \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x) \to \forall h \in ℤ_{\geq j} (F (h) \in ℂ \land \|F (h) - A\| < x)$
104	103	ad2antlr	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to \forall h \in ℤ_{\geq j} (F (h) \in ℂ \land \|F (h) - A\| < x)$
105		zre	$⊢ j \in ℤ \to j \in ℝ$
106	105	3ad2ant2	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to j \in ℝ$
107		simp3	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to i \in ℤ_{\geq if (M \leq j, j, M)}$
108		eluzelz	$⊢ i \in ℤ_{\geq if (M \leq j, j, M)} \to i \in ℤ$
109		zre	$⊢ i \in ℤ \to i \in ℝ$
110	107 108 109	3syl	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to i \in ℝ$
111		simp1	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to φ$
112	6	zred	$⊢ φ \to M \in ℝ$
113	111 112	syl	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to M \in ℝ$
114		simpl2	$⊢ ((φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \land M \leq j) \to j \in ℤ$
115	114	zred	$⊢ ((φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \land M \leq j) \to j \in ℝ$
116	113	adantr	$⊢ ((φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \land \neg M \leq j) \to M \in ℝ$
117	115 116	ifclda	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to if (M \leq j, j, M) \in ℝ$
118		max1	$⊢ (M \in ℝ \land j \in ℝ) \to M \leq if (M \leq j, j, M)$
119	113 106 118	syl2anc	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to M \leq if (M \leq j, j, M)$
120		eluzle	$⊢ i \in ℤ_{\geq if (M \leq j, j, M)} \to if (M \leq j, j, M) \leq i$
121	120	3ad2ant3	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to if (M \leq j, j, M) \leq i$
122	113 117 110 119 121	letrd	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to M \leq i$
123	111 6	syl	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to M \in ℤ$
124	108	3ad2ant3	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to i \in ℤ$
125		eluz	$⊢ (M \in ℤ \land i \in ℤ) \to (i \in ℤ_{\geq M} \leftrightarrow M \leq i)$
126	123 124 125	syl2anc	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to (i \in ℤ_{\geq M} \leftrightarrow M \leq i)$
127	122 126	mpbird	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to i \in ℤ_{\geq M}$
128	127 5	eleqtrrdi	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to i \in Z$
129	111 128	jca	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to (φ \land i \in Z)$
130		eluzelre	$⊢ I (i) \in ℤ_{\geq M} \to I (i) \in ℝ$
131	129 77 130	3syl	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to I (i) \in ℝ$
132		max2	$⊢ (M \in ℝ \land j \in ℝ) \to j \leq if (M \leq j, j, M)$
133	113 106 132	syl2anc	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to j \leq if (M \leq j, j, M)$
134	106 117 110 133 121	letrd	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to j \leq i$
135		eluzle	$⊢ I (i) \in ℤ_{\geq i} \to i \leq I (i)$
136	129 76 135	3syl	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to i \leq I (i)$
137	106 110 131 134 136	letrd	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to j \leq I (i)$
138		simp2	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to j \in ℤ$
139		eluzelz	$⊢ I (i) \in ℤ_{\geq i} \to I (i) \in ℤ$
140	129 76 139	3syl	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to I (i) \in ℤ$
141		eluz	$⊢ (j \in ℤ \land I (i) \in ℤ) \to (I (i) \in ℤ_{\geq j} \leftrightarrow j \leq I (i))$
142	138 140 141	syl2anc	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to (I (i) \in ℤ_{\geq j} \leftrightarrow j \leq I (i))$
143	137 142	mpbird	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to I (i) \in ℤ_{\geq j}$
144	23 24 26 143	syl3anc	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to I (i) \in ℤ_{\geq j}$
145		fveq2	$⊢ h = I (i) \to F (h) = F (I (i))$
146	145	eleq1d	$⊢ h = I (i) \to (F (h) \in ℂ \leftrightarrow F (I (i)) \in ℂ)$
147	145	fvoveq1d	$⊢ h = I (i) \to \|F (h) - A\| = \|F (I (i)) - A\|$
148	147	breq1d	$⊢ h = I (i) \to (\|F (h) - A\| < x \leftrightarrow \|F (I (i)) - A\| < x)$
149	146 148	anbi12d	$⊢ h = I (i) \to ((F (h) \in ℂ \land \|F (h) - A\| < x) \leftrightarrow (F (I (i)) \in ℂ \land \|F (I (i)) - A\| < x))$
150	149	rspccva	$⊢ (\forall h \in ℤ_{\geq j} (F (h) \in ℂ \land \|F (h) - A\| < x) \land I (i) \in ℤ_{\geq j}) \to (F (I (i)) \in ℂ \land \|F (I (i)) - A\| < x)$
151	150	simprd	$⊢ (\forall h \in ℤ_{\geq j} (F (h) \in ℂ \land \|F (h) - A\| < x) \land I (i) \in ℤ_{\geq j}) \to \|F (I (i)) - A\| < x$
152	104 144 151	syl2anc	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to \|F (I (i)) - A\| < x$
153	96 152	eqbrtrd	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to \|G (i) - A\| < x$
154	94 153	jca	$⊢ ((((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to (G (i) \in ℂ \land \|G (i) - A\| < x)$
155	154	ex	$⊢ (((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \to (i \in ℤ_{\geq if (M \leq j, j, M)} \to (G (i) \in ℂ \land \|G (i) - A\| < x))$
156	22 155	ralrimi	$⊢ (((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \to \forall i \in ℤ_{\geq if (M \leq j, j, M)} (G (i) \in ℂ \land \|G (i) - A\| < x)$
157		fveq2	$⊢ l = if (M \leq j, j, M) \to ℤ_{\geq l} = ℤ_{\geq if (M \leq j, j, M)}$
158	157	raleqdv	$⊢ l = if (M \leq j, j, M) \to (\forall i \in ℤ_{\geq l} (G (i) \in ℂ \land \|G (i) - A\| < x) \leftrightarrow \forall i \in ℤ_{\geq if (M \leq j, j, M)} (G (i) \in ℂ \land \|G (i) - A\| < x))$
159	158	rspcev	$⊢ (if (M \leq j, j, M) \in ℤ \land \forall i \in ℤ_{\geq if (M \leq j, j, M)} (G (i) \in ℂ \land \|G (i) - A\| < x)) \to \exists l \in ℤ \forall i \in ℤ_{\geq l} (G (i) \in ℂ \land \|G (i) - A\| < x)$
160	19 156 159	syl2anc	$⊢ (((φ \land x \in ℝ^{+}) \land j \in ℤ) \land \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)) \to \exists l \in ℤ \forall i \in ℤ_{\geq l} (G (i) \in ℂ \land \|G (i) - A\| < x)$
161		eqidd	$⊢ (φ \land i \in ℤ) \to F (i) = F (i)$
162	7 161	clim	$⊢ φ \to (F ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)))$
163	9 162	mpbid	$⊢ φ \to (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x))$
164	163	simprd	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in ℤ \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)$
165	164	r19.21bi	$⊢ (φ \land x \in ℝ^{+}) \to \exists j \in ℤ \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)$
166	160 165	r19.29a	$⊢ (φ \land x \in ℝ^{+}) \to \exists l \in ℤ \forall i \in ℤ_{\geq l} (G (i) \in ℂ \land \|G (i) - A\| < x)$
167	166	ex	$⊢ φ \to (x \in ℝ^{+} \to \exists l \in ℤ \forall i \in ℤ_{\geq l} (G (i) \in ℂ \land \|G (i) - A\| < x))$
168	16 167	ralrimi	$⊢ φ \to \forall x \in ℝ^{+} \exists l \in ℤ \forall i \in ℤ_{\geq l} (G (i) \in ℂ \land \|G (i) - A\| < x)$
169		eqidd	$⊢ (φ \land i \in ℤ) \to G (i) = G (i)$
170	12 169	clim	$⊢ φ \to (G ⇝ A \leftrightarrow (A \in ℂ \land \forall x \in ℝ^{+} \exists l \in ℤ \forall i \in ℤ_{\geq l} (G (i) \in ℂ \land \|G (i) - A\| < x)))$
171	15 168 170	mpbir2and	$⊢ φ \to G ⇝ A$

Metamath Proof Explorer

Theorem climsuse

Proof