This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem climcn1lem

Description: The limit of a continuous function, theorem form. (Contributed by Mario Carneiro, 9-Feb-2014)

Ref Expression
Hypotheses climcn1lem.1 
|- Z = ( ZZ>= ` M )
climcn1lem.2 
|- ( ph -> F ~~> A )
climcn1lem.4 
|- ( ph -> G e. W )
climcn1lem.5 
|- ( ph -> M e. ZZ )
climcn1lem.6 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
climcn1lem.7 
|- H : CC --> CC
climcn1lem.8 
|- ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( H ` z ) - ( H ` A ) ) ) < x ) )
climcn1lem.9 
|- ( ( ph /\ k e. Z ) -> ( G ` k ) = ( H ` ( F ` k ) ) )
Assertion climcn1lem 
|- ( ph -> G ~~> ( H ` A ) )

Proof

Step Hyp Ref Expression
1 climcn1lem.1 
 |-  Z = ( ZZ>= ` M )
2 climcn1lem.2 
 |-  ( ph -> F ~~> A )
3 climcn1lem.4 
 |-  ( ph -> G e. W )
4 climcn1lem.5 
 |-  ( ph -> M e. ZZ )
5 climcn1lem.6 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
6 climcn1lem.7 
 |-  H : CC --> CC
7 climcn1lem.8 
 |-  ( ( A e. CC /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( H ` z ) - ( H ` A ) ) ) < x ) )
8 climcn1lem.9 
 |-  ( ( ph /\ k e. Z ) -> ( G ` k ) = ( H ` ( F ` k ) ) )
9 climcl 
 |-  ( F ~~> A -> A e. CC )
10 2 9 syl 
 |-  ( ph -> A e. CC )
11 6 ffvelcdmi 
 |-  ( z e. CC -> ( H ` z ) e. CC )
12 11 adantl 
 |-  ( ( ph /\ z e. CC ) -> ( H ` z ) e. CC )
13 10 7 sylan 
 |-  ( ( ph /\ x e. RR+ ) -> E. y e. RR+ A. z e. CC ( ( abs ` ( z - A ) ) < y -> ( abs ` ( ( H ` z ) - ( H ` A ) ) ) < x ) )
14 1 4 10 12 2 3 13 5 8 climcn1 
 |-  ( ph -> G ~~> ( H ` A ) )