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	biimpi	$⊢ i \in Z \to i \in ℤ_{\geq M}$
59	58	adantl	$⊢ (φ \land i \in Z) \to i \in ℤ_{\geq M}$
60		uzss	$⊢ i \in ℤ_{\geq M} \to ℤ_{\geq i} \subseteq ℤ_{\geq M}$
61	59 60	syl	$⊢ (φ \land i \in Z) \to ℤ_{\geq i} \subseteq ℤ_{\geq M}$
62		nfcv	$⊢ \underline{Ⅎ} k (i + 1)$
63	4 62	nffv	$⊢ \underline{Ⅎ} k I (i + 1)$
64		nfcv	$⊢ \underline{Ⅎ} k ℤ_{\geq}$
65		nfcv	$⊢ \underline{Ⅎ} k +$
66		nfcv	$⊢ \underline{Ⅎ} k 1$
67	46 65 66	nfov	$⊢ \underline{Ⅎ} k (I (i) + 1)$
68	64 67	nffv	$⊢ \underline{Ⅎ} k ℤ_{\geq (I (i) + 1)}$
69	63 68	nfel	$⊢ Ⅎ k I (i + 1) \in ℤ_{\geq (I (i) + 1)}$
70	43 69	nfim	$⊢ Ⅎ k ((φ \land i \in Z) \to I (i + 1) \in ℤ_{\geq (I (i) + 1)})$
71		fvoveq1	$⊢ k = i \to I (k + 1) = I (i + 1)$
72		fveq2	$⊢ k = i \to I (k) = I (i)$
73	72	fvoveq1d	$⊢ k = i \to ℤ_{\geq (I (k) + 1)} = ℤ_{\geq (I (i) + 1)}$
74	71 73	eleq12d	$⊢ k = i \to (I (k + 1) \in ℤ_{\geq (I (k) + 1)} \leftrightarrow I (i + 1) \in ℤ_{\geq (I (i) + 1)})$
75	51 74	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)}))$
76	70 75 11	chvarfv	$⊢ (φ \land i \in Z) \to I (i + 1) \in ℤ_{\geq (I (i) + 1)}$
77	5 6 10 76	climsuselem1	$⊢ (φ \land i \in Z) \to I (i) \in ℤ_{\geq i}$
78	61 77	sseldd	$⊢ (φ \land i \in Z) \to I (i) \in ℤ_{\geq M}$
79	78 5	eleqtrrdi	$⊢ (φ \land i \in Z) \to I (i) \in Z$
80	79	ex	$⊢ φ \to (i \in Z \to I (i) \in Z)$
81	80	imdistani	$⊢ (φ \land i \in Z) \to (φ \land I (i) \in Z)$
82	42	nfci	$⊢ \underline{Ⅎ} k Z$
83	46 82	nfel	$⊢ Ⅎ k I (i) \in Z$
84	1 83	nfan	$⊢ Ⅎ k (φ \land I (i) \in Z)$
85	47	nfel1	$⊢ Ⅎ k F (I (i)) \in ℂ$
86	84 85	nfim	$⊢ Ⅎ k ((φ \land I (i) \in Z) \to F (I (i)) \in ℂ)$
87		eleq1	$⊢ k = I (i) \to (k \in Z \leftrightarrow I (i) \in Z)$
88	87	anbi2d	$⊢ k = I (i) \to ((φ \land k \in Z) \leftrightarrow (φ \land I (i) \in Z))$
89		fveq2	$⊢ k = I (i) \to F (k) = F (I (i))$
90	89	eleq1d	$⊢ k = I (i) \to (F (k) \in ℂ \leftrightarrow F (I (i)) \in ℂ)$
91	88 90	imbi12d	$⊢ k = I (i) \to (((φ \land k \in Z) \to F (k) \in ℂ) \leftrightarrow ((φ \land I (i) \in Z) \to F (I (i)) \in ℂ))$
92	46 86 91 8	vtoclgf	$⊢ I (i) \in Z \to ((φ \land I (i) \in Z) \to F (I (i)) \in ℂ)$
93	79 81 92	sylc	$⊢ (φ \land i \in Z) \to F (I (i)) \in ℂ$
94	56 93	eqeltrd	$⊢ (φ \land i \in Z) \to G (i) \in ℂ$
95	23 41 94	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 ℂ$
96	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))$
97	96	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\|$
98		fveq2	$⊢ i = h \to F (i) = F (h)$
99	98	eleq1d	$⊢ i = h \to (F (i) \in ℂ \leftrightarrow F (h) \in ℂ)$
100	98	fvoveq1d	$⊢ i = h \to \|F (i) - A\| = \|F (h) - A\|$
101	100	breq1d	$⊢ i = h \to (\|F (i) - A\| < x \leftrightarrow \|F (h) - A\| < x)$
102	99 101	anbi12d	$⊢ i = h \to ((F (i) \in ℂ \land \|F (i) - A\| < x) \leftrightarrow (F (h) \in ℂ \land \|F (h) - A\| < x))$
103	102	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)$
104	103	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)$
105	104	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)$
106		zre	$⊢ j \in ℤ \to j \in ℝ$
107	106	3ad2ant2	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to j \in ℝ$
108		simp3	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to i \in ℤ_{\geq if (M \leq j, j, M)}$
109		eluzelz	$⊢ i \in ℤ_{\geq if (M \leq j, j, M)} \to i \in ℤ$
110		zre	$⊢ i \in ℤ \to i \in ℝ$
111	108 109 110	3syl	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to i \in ℝ$
112		simp1	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to φ$
113	6	zred	$⊢ φ \to M \in ℝ$
114	112 113	syl	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to M \in ℝ$
115		simpl2	$⊢ ((φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \land M \leq j) \to j \in ℤ$
116	115	zred	$⊢ ((φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \land M \leq j) \to j \in ℝ$
117	114	adantr	$⊢ ((φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \land \neg M \leq j) \to M \in ℝ$
118	116 117	ifclda	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to if (M \leq j, j, M) \in ℝ$
119		max1	$⊢ (M \in ℝ \land j \in ℝ) \to M \leq if (M \leq j, j, M)$
120	114 107 119	syl2anc	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to M \leq if (M \leq j, j, M)$
121		eluzle	$⊢ i \in ℤ_{\geq if (M \leq j, j, M)} \to if (M \leq j, j, M) \leq i$
122	121	3ad2ant3	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to if (M \leq j, j, M) \leq i$
123	114 118 111 120 122	letrd	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to M \leq i$
124	112 6	syl	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to M \in ℤ$
125	109	3ad2ant3	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to i \in ℤ$
126		eluz	$⊢ (M \in ℤ \land i \in ℤ) \to (i \in ℤ_{\geq M} \leftrightarrow M \leq i)$
127	124 125 126	syl2anc	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to (i \in ℤ_{\geq M} \leftrightarrow M \leq i)$
128	123 127	mpbird	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to i \in ℤ_{\geq M}$
129	128 5	eleqtrrdi	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to i \in Z$
130	112 129	jca	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to (φ \land i \in Z)$
131		eluzelre	$⊢ I (i) \in ℤ_{\geq M} \to I (i) \in ℝ$
132	130 78 131	3syl	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to I (i) \in ℝ$
133		max2	$⊢ (M \in ℝ \land j \in ℝ) \to j \leq if (M \leq j, j, M)$
134	114 107 133	syl2anc	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to j \leq if (M \leq j, j, M)$
135	107 118 111 134 122	letrd	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to j \leq i$
136		eluzle	$⊢ I (i) \in ℤ_{\geq i} \to i \leq I (i)$
137	130 77 136	3syl	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to i \leq I (i)$
138	107 111 132 135 137	letrd	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to j \leq I (i)$
139		simp2	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to j \in ℤ$
140		eluzelz	$⊢ I (i) \in ℤ_{\geq i} \to I (i) \in ℤ$
141	130 77 140	3syl	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to I (i) \in ℤ$
142		eluz	$⊢ (j \in ℤ \land I (i) \in ℤ) \to (I (i) \in ℤ_{\geq j} \leftrightarrow j \leq I (i))$
143	139 141 142	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))$
144	138 143	mpbird	$⊢ (φ \land j \in ℤ \land i \in ℤ_{\geq if (M \leq j, j, M)}) \to I (i) \in ℤ_{\geq j}$
145	23 24 26 144	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}$
146		fveq2	$⊢ h = I (i) \to F (h) = F (I (i))$
147	146	eleq1d	$⊢ h = I (i) \to (F (h) \in ℂ \leftrightarrow F (I (i)) \in ℂ)$
148	146	fvoveq1d	$⊢ h = I (i) \to \|F (h) - A\| = \|F (I (i)) - A\|$
149	148	breq1d	$⊢ h = I (i) \to (\|F (h) - A\| < x \leftrightarrow \|F (I (i)) - A\| < x)$
150	147 149	anbi12d	$⊢ h = I (i) \to ((F (h) \in ℂ \land \|F (h) - A\| < x) \leftrightarrow (F (I (i)) \in ℂ \land \|F (I (i)) - A\| < x))$
151	150	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)$
152	151	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$
153	105 145 152	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$
154	97 153	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$
155	95 154	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)$
156	155	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))$
157	22 156	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)$
158		fveq2	$⊢ l = if (M \leq j, j, M) \to ℤ_{\geq l} = ℤ_{\geq if (M \leq j, j, M)}$
159	158	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))$
160	159	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)$
161	19 157 160	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)$
162		eqidd	$⊢ (φ \land i \in ℤ) \to F (i) = F (i)$
163	7 162	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)))$
164	9 163	mpbid	$⊢ φ \to (A \in ℂ \land \forall x \in ℝ^{+} \exists j \in ℤ \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x))$
165	164	simprd	$⊢ φ \to \forall x \in ℝ^{+} \exists j \in ℤ \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)$
166	165	r19.21bi	$⊢ (φ \land x \in ℝ^{+}) \to \exists j \in ℤ \forall i \in ℤ_{\geq j} (F (i) \in ℂ \land \|F (i) - A\| < x)$
167	161 166	r19.29a	$⊢ (φ \land x \in ℝ^{+}) \to \exists l \in ℤ \forall i \in ℤ_{\geq l} (G (i) \in ℂ \land \|G (i) - A\| < x)$
168	167	ex	$⊢ φ \to (x \in ℝ^{+} \to \exists l \in ℤ \forall i \in ℤ_{\geq l} (G (i) \in ℂ \land \|G (i) - A\| < x))$
169	16 168	ralrimi	$⊢ φ \to \forall x \in ℝ^{+} \exists l \in ℤ \forall i \in ℤ_{\geq l} (G (i) \in ℂ \land \|G (i) - A\| < x)$
170		eqidd	$⊢ (φ \land i \in ℤ) \to G (i) = G (i)$
171	12 170	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)))$
172	15 169 171	mpbir2and	$⊢ φ \to G ⇝ A$

Metamath Proof Explorer

Theorem climsuse

Proof