Metamath Proof Explorer

Theorem rlimss

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

Ref Expression
Assertion rlimss 
|- ( F ~~>r A -> dom F C_ RR )

Proof

Step Hyp Ref Expression
1 rlimpm 
 |-  ( F ~~>r A -> F e. ( CC ^pm RR ) )
2 cnex 
 |-  CC e. _V
3 reex 
 |-  RR e. _V
4 2 3 elpm2 
 |-  ( F e. ( CC ^pm RR ) <-> ( F : dom F --> CC /\ dom F C_ RR ) )
5 4 simprbi 
 |-  ( F e. ( CC ^pm RR ) -> dom F C_ RR )
6 1 5 syl 
 |-  ( F ~~>r A -> dom F C_ RR )