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 )