Description: Closure of a function with a limit in the complex numbers. (Contributed by Mario Carneiro, 16-Sep-2014)
Ref | Expression | ||
---|---|---|---|
Assertion | rlimf | ⊢ ( 𝐹 ⇝𝑟 𝐴 → 𝐹 : dom 𝐹 ⟶ ℂ ) |
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 𝐹 ⟶ ℂ ) |