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

Metamath Proof Explorer

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 sselid 
 |-  ( ( ph /\ B ( S _D F ) C ) -> C e. CC )