Theorem dvcl

Description: The derivative function takes values in the complex numbers. (Contributed by Mario Carneiro, 7-Aug-2014) (Revised by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Hypotheses	dvcl.s	|- ( ph -> S C_ CC )
	dvcl.f	|- ( ph -> F : A --> CC )
	dvcl.a	|- ( ph -> A C_ S )
Assertion	dvcl	|- ( ( ph /\ B ( S _D F ) C ) -> C e. CC )

Proof

Step	Hyp	Ref	Expression
1		dvcl.s	|- ( ph -> S C_ CC )
2		dvcl.f	|- ( ph -> F : A --> CC )
3		dvcl.a	|- ( ph -> A C_ S )
4		limccl	|- ( ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) limCC B ) C_ CC
5		eqid	|- ( ( TopOpen ` CCfld ) |`t S ) = ( ( TopOpen ` CCfld ) |`t S )
6		eqid	|- ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
7		eqid	|- ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) = ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) )
8	5 6 7 1 2 3	eldv	|- ( ph -> ( B ( S _D F ) C <-> ( B e. ( ( int ` ( ( TopOpen ` CCfld ) |`t S ) ) ` A ) /\ C e. ( ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) limCC B ) ) ) )
9	8	simplbda	|- ( ( ph /\ B ( S _D F ) C ) -> C e. ( ( z e. ( A \ { B } ) |-> ( ( ( F ` z ) - ( F ` B ) ) / ( z - B ) ) ) limCC B ) )
10	4 9	sseldi	|- ( ( ph /\ B ( S _D F ) C ) -> C e. CC )