Theorem xlimclimdm

Description: A sequence of extended reals that converges to a real w.r.t. the standard topology on the extended reals, also converges w.r.t. to the standard topology on the complex numbers. (Contributed by Glauco Siliprandi, 23-Apr-2023)

	Ref	Expression
Hypotheses	xlimclimdm.1	$$⊢\phi \to M\in \mathbb{Z}$$
	xlimclimdm.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	xlimclimdm.3	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
	xlimclimdm.4	$$⊢\phi \to F\underset{*}{⇝}A$$
	xlimclimdm.5	$$⊢\phi \to A\in ℝ$$
Assertion	xlimclimdm	$$⊢\phi \to F\in \mathrm{dom}⇝$$

Proof

Step	Hyp	Ref	Expression
1		xlimclimdm.1	$$⊢\phi \to M\in \mathbb{Z}$$
2		xlimclimdm.2	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		xlimclimdm.3	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
4		xlimclimdm.4	$$⊢\phi \to F\underset{*}{⇝}A$$
5		xlimclimdm.5	$$⊢\phi \to A\in ℝ$$
6		climrel	$$⊢\mathrm{Rel}⇝$$
7	1 2 3 5	xlimclim2	$$⊢\phi \to \left(F\underset{*}{⇝}A\leftrightarrow F⇝A\right)$$
8	4 7	mpbid	$$⊢\phi \to F⇝A$$
9		releldm	$$⊢\left(\mathrm{Rel}⇝\wedge F⇝A\right)\to F\in \mathrm{dom}⇝$$
10	6 8 9	sylancr	$$⊢\phi \to F\in \mathrm{dom}⇝$$