Theorem dmclimxlim

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

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

Proof

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