Theorem rlimf

Description: Closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014)

	Ref	Expression
Assertion	rlimf	⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 : dom 𝐹 ⟶ ℂ )

Proof

Step	Hyp	Ref	Expression
1		rlimpm	⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 ∈ ( ℂ ↑pm ℝ ) )
2		cnex	⊢ ℂ ∈ V
3		reex	⊢ ℝ ∈ V
4	2 3	elpm2	⊢ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) ↔ ( 𝐹 : dom 𝐹 ⟶ ℂ ∧ dom 𝐹 ⊆ ℝ ) )
5	4	simplbi	⊢ ( 𝐹 ∈ ( ℂ ↑pm ℝ ) → 𝐹 : dom 𝐹 ⟶ ℂ )
6	1 5	syl	⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 : dom 𝐹 ⟶ ℂ )