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	ffvelrni	|- ( 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 ) )