Metamath Proof Explorer

Theorem abscncf

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

Ref Expression
Assertion abscncf 
|- abs e. ( CC -cn-> RR )

Proof

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