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	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	dmclimxlim.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	dmclimxlim.3	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
	dmclimxlim.4	⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )
Assertion	dmclimxlim	⊢ ( 𝜑 → 𝐹 ∈ dom ~~>* )

Proof

Step	Hyp	Ref	Expression
1		dmclimxlim.1	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2		dmclimxlim.2	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3		dmclimxlim.3	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ )
4		dmclimxlim.4	⊢ ( 𝜑 → 𝐹 ∈ dom ⇝ )
5		xlimrel	⊢ Rel ~~>*
6	1 2 3	climliminf	⊢ ( 𝜑 → ( 𝐹 ∈ dom ⇝ ↔ 𝐹 ⇝ ( lim inf ‘ 𝐹 ) ) )
7	4 6	mpbid	⊢ ( 𝜑 → 𝐹 ⇝ ( lim inf ‘ 𝐹 ) )
8	1 2 3 7	climxlim	⊢ ( 𝜑 → 𝐹 ~~>* ( lim inf ‘ 𝐹 ) )
9		releldm	⊢ ( ( Rel ~~>* ∧ 𝐹 ~~>* ( lim inf ‘ 𝐹 ) ) → 𝐹 ∈ dom ~~>* )
10	5 8 9	sylancr	⊢ ( 𝜑 → 𝐹 ∈ dom ~~>* )