Metamath Proof Explorer

Theorem recncf

Description: Real part is continuous. (Contributed by Paul Chapman, 21-Oct-2007) (Revised by Mario Carneiro, 28-Apr-2014)

Ref Expression
Assertion recncf 
|- Re e. ( CC -cn-> RR )

Proof

Step Hyp Ref Expression
1 ref 
 |-  Re : CC --> RR
2 recn2 
 |-  ( ( x e. CC /\ y e. RR+ ) -> E. z e. RR+ A. w e. CC ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( Re ` w ) - ( Re ` x ) ) ) < y ) )
3 2 rgen2 
 |-  A. x e. CC A. y e. RR+ E. z e. RR+ A. w e. CC ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( Re ` w ) - ( Re ` x ) ) ) < y )
4 ssid 
 |-  CC C_ CC
5 ax-resscn 
 |-  RR C_ CC
6 elcncf2 
 |-  ( ( CC C_ CC /\ RR C_ CC ) -> ( Re e. ( CC -cn-> RR ) <-> ( Re : CC --> RR /\ A. x e. CC A. y e. RR+ E. z e. RR+ A. w e. CC ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( Re ` w ) - ( Re ` x ) ) ) < y ) ) ) )
7 4 5 6 mp2an 
 |-  ( Re e. ( CC -cn-> RR ) <-> ( Re : CC --> RR /\ A. x e. CC A. y e. RR+ E. z e. RR+ A. w e. CC ( ( abs ` ( w - x ) ) < z -> ( abs ` ( ( Re ` w ) - ( Re ` x ) ) ) < y ) ) )
8 1 3 7 mpbir2an 
 |-  Re e. ( CC -cn-> RR )