Metamath Proof Explorer


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 𝐹 ⟶ ℂ )