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

Proof

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