Theorem climxlim2

Description: A sequence of extended reals, converging w.r.t. the standard topology on the complex numbers is a converging sequence w.r.t. the standard topology on the extended reals. This is non-trivial, because +oo and -oo could, in principle, be complex numbers. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	climxlim2.m	$$⊢\phi \to M\in \mathbb{Z}$$
	climxlim2.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climxlim2.f	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
	climxlim2.a	$$⊢\phi \to F⇝A$$
Assertion	climxlim2	$$⊢\phi \to F\underset{*}{⇝}A$$

Proof

Step	Hyp	Ref	Expression
1		climxlim2.m	$$⊢\phi \to M\in \mathbb{Z}$$
2		climxlim2.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		climxlim2.f	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
4		climxlim2.a	$$⊢\phi \to F⇝A$$
5	2	eluzelz2	$$⊢j\in Z\to j\in \mathbb{Z}$$
6	5	ad2antlr	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℂ\right)\to j\in \mathbb{Z}$$
7		eqid	$$⊢{\mathbb{Z}}_{\ge j}={\mathbb{Z}}_{\ge j}$$
8	3	adantr	$$⊢\left(\phi \wedge j\in Z\right)\to F:Z⟶{ℝ}^{*}$$
9	2	uzssd3	$$⊢j\in Z\to {\mathbb{Z}}_{\ge j}\subseteq Z$$
10	9	adantl	$$⊢\left(\phi \wedge j\in Z\right)\to {\mathbb{Z}}_{\ge j}\subseteq Z$$
11	8 10	fssresd	$$⊢\left(\phi \wedge j\in Z\right)\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶{ℝ}^{*}$$
12	11	adantr	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℂ\right)\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶{ℝ}^{*}$$
13		simpr	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℂ\right)\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℂ$$
14	4	adantr	$$⊢\left(\phi \wedge j\in Z\right)\to F⇝A$$
15	2	fvexi	$$⊢Z\in \mathrm{V}$$
16	15	a1i	$$⊢\phi \to Z\in \mathrm{V}$$
17	3 16	fexd	$$⊢\phi \to F\in \mathrm{V}$$
18		climres	$$⊢\left(j\in \mathbb{Z}\wedge F\in \mathrm{V}\right)\to \left(\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right)⇝A\leftrightarrow F⇝A\right)$$
19	5 17 18	syl2anr	$$⊢\left(\phi \wedge j\in Z\right)\to \left(\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right)⇝A\leftrightarrow F⇝A\right)$$
20	14 19	mpbird	$$⊢\left(\phi \wedge j\in Z\right)\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right)⇝A$$
21	20	adantr	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℂ\right)\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right)⇝A$$
22	6 7 12 13 21	climxlim2lem	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℂ\right)\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right)\underset{*}{⇝}A$$
23	2 3	fuzxrpmcn	$$⊢\phi \to F\in \left({ℝ}^{*}{\uparrow }_{𝑝𝑚}ℂ\right)$$
24	23	adantr	$$⊢\left(\phi \wedge j\in Z\right)\to F\in \left({ℝ}^{*}{\uparrow }_{𝑝𝑚}ℂ\right)$$
25	5	adantl	$$⊢\left(\phi \wedge j\in Z\right)\to j\in \mathbb{Z}$$
26	24 25	xlimres	$$⊢\left(\phi \wedge j\in Z\right)\to \left(F\underset{*}{⇝}A\leftrightarrow \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right)\underset{*}{⇝}A\right)$$
27	26	adantr	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℂ\right)\to \left(F\underset{*}{⇝}A\leftrightarrow \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right)\underset{*}{⇝}A\right)$$
28	22 27	mpbird	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℂ\right)\to F\underset{*}{⇝}A$$
29	3	ffnd	$$⊢\phi \to FFnZ$$
30		climcl	$$⊢F⇝A\to A\in ℂ$$
31	4 30	syl	$$⊢\phi \to A\in ℂ$$
32		breldmg	$$⊢\left(F\in \mathrm{V}\wedge A\in ℂ\wedge F⇝A\right)\to F\in \mathrm{dom}⇝$$
33	17 31 4 32	syl3anc	$$⊢\phi \to F\in \mathrm{dom}⇝$$
34	1 2 29 33	climrescn	$$⊢\phi \to \exists j\in Z\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℂ$$
35	28 34	r19.29a	$$⊢\phi \to F\underset{*}{⇝}A$$