Theorem abscn2

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

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

Proof

Step	Hyp	Ref	Expression
1		absf	|- abs : CC --> RR
2		ax-resscn	|- RR C_ CC
3		fss	|- ( ( abs : CC --> RR /\ RR C_ CC ) -> abs : CC --> CC )
4	1 2 3	mp2an	|- abs : CC --> CC
5		abs2difabs	|- ( ( z e. CC /\ A e. CC ) -> ( abs ` ( ( abs ` z ) - ( abs ` A ) ) ) <_ ( abs ` ( z - A ) ) )
6	4 5	cn1lem	|- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( abs ` z ) - ( abs ` A ) ) ) < x ) )