Metamath Proof Explorer

Theorem recn2

Description: The real part function is continuous. (Contributed by Mario Carneiro, 9-Feb-2014)

Ref Expression
Assertion recn2 
|- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( Re ` z ) - ( Re ` A ) ) ) < x ) )

Proof

Step Hyp Ref Expression
1 ref 
 |-  Re : CC --> RR
2 ax-resscn 
 |-  RR C_ CC
3 fss 
 |-  ( ( Re : CC --> RR /\ RR C_ CC ) -> Re : CC --> CC )
4 1 2 3 mp2an 
 |-  Re : CC --> CC
5 resub 
 |-  ( ( z e. CC /\ A e. CC ) -> ( Re ` ( z - A ) ) = ( ( Re ` z ) - ( Re ` A ) ) )
6 5 fveq2d 
 |-  ( ( z e. CC /\ A e. CC ) -> ( abs ` ( Re ` ( z - A ) ) ) = ( abs ` ( ( Re ` z ) - ( Re ` A ) ) ) )
7 subcl 
 |-  ( ( z e. CC /\ A e. CC ) -> ( z - A ) e. CC )
8 absrele 
 |-  ( ( z - A ) e. CC -> ( abs ` ( Re ` ( z - A ) ) ) <_ ( abs ` ( z - A ) ) )
9 7 8 syl 
 |-  ( ( z e. CC /\ A e. CC ) -> ( abs ` ( Re ` ( z - A ) ) ) <_ ( abs ` ( z - A ) ) )
10 6 9 eqbrtrrd 
 |-  ( ( z e. CC /\ A e. CC ) -> ( abs ` ( ( Re ` z ) - ( Re ` A ) ) ) <_ ( abs ` ( z - A ) ) )
11 4 10 cn1lem 
 |-  ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( Re ` z ) - ( Re ` A ) ) ) < x ) )