Metamath Proof Explorer

Theorem cn1lem

Description: A sufficient condition for a function to be continuous. (Contributed by Mario Carneiro, 9-Feb-2014)

Ref Expression
Hypotheses cn1lem.1 
|- F : CC --> CC
cn1lem.2 
|- ( ( z e. CC /\ A e. CC ) -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) <_ ( abs ` ( z - A ) ) )
Assertion cn1lem 
|- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) )

Proof

Step Hyp Ref Expression
1 cn1lem.1 
 |-  F : CC --> CC
2 cn1lem.2 
 |-  ( ( z e. CC /\ A e. CC ) -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) <_ ( abs ` ( z - A ) ) )
3 simpr 
 |-  ( ( A e. CC /\ x e. RR+ ) -> x e. RR+ )
4 simpr 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ z e. CC ) -> z e. CC )
5 simpll 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ z e. CC ) -> A e. CC )
6 4 5 2 syl2anc 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ z e. CC ) -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) <_ ( abs ` ( z - A ) ) )
7 1 ffvelrni 
 |-  ( z e. CC -> ( F ` z ) e. CC )
8 4 7 syl 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ z e. CC ) -> ( F ` z ) e. CC )
9 1 ffvelrni 
 |-  ( A e. CC -> ( F ` A ) e. CC )
10 5 9 syl 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ z e. CC ) -> ( F ` A ) e. CC )
11 8 10 subcld 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ z e. CC ) -> ( ( F ` z ) - ( F ` A ) ) e. CC )
12 11 abscld 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ z e. CC ) -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) e. RR )
13 4 5 subcld 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ z e. CC ) -> ( z - A ) e. CC )
14 13 abscld 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ z e. CC ) -> ( abs ` ( z - A ) ) e. RR )
15 rpre 
 |-  ( x e. RR+ -> x e. RR )
16 15 ad2antlr 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ z e. CC ) -> x e. RR )
17 lelttr 
 |-  ( ( ( abs ` ( ( F ` z ) - ( F ` A ) ) ) e. RR /\ ( abs ` ( z - A ) ) e. RR /\ x e. RR ) -> ( ( ( abs ` ( ( F ` z ) - ( F ` A ) ) ) <_ ( abs ` ( z - A ) ) /\ ( abs ` ( z - A ) ) < x ) -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) )
18 12 14 16 17 syl3anc 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ z e. CC ) -> ( ( ( abs ` ( ( F ` z ) - ( F ` A ) ) ) <_ ( abs ` ( z - A ) ) /\ ( abs ` ( z - A ) ) < x ) -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) )
19 6 18 mpand 
 |-  ( ( ( A e. CC /\ x e. RR+ ) /\ z e. CC ) -> ( ( abs ` ( z - A ) ) < x -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) )
20 19 ralrimiva 
 |-  ( ( A e. CC /\ x e. RR+ ) -> A. z e. CC ( ( abs ` ( z - A ) ) < x -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) )
21 breq2 
 |-  ( y = x -> ( ( abs ` ( z - A ) ) < y <-> ( abs ` ( z - A ) ) < x ) )
22 21 rspceaimv 
 |-  ( ( x e. RR+ /\ A. z e. CC ( ( abs ` ( z - A ) ) < x -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) )
23 3 20 22 syl2anc 
 |-  ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( F ` z ) - ( F ` A ) ) ) < x ) )