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	$$⊢\phi \to S\subseteq ℂ$$
	dvcl.f	$$⊢\phi \to F:A⟶ℂ$$
	dvcl.a	$$⊢\phi \to A\subseteq S$$
Assertion	dvcl	$$⊢\left(\phi \wedge B{F}_S^{\prime }C\right)\to C\in ℂ$$

Proof

Step	Hyp	Ref	Expression
1		dvcl.s	$$⊢\phi \to S\subseteq ℂ$$
2		dvcl.f	$$⊢\phi \to F:A⟶ℂ$$
3		dvcl.a	$$⊢\phi \to A\subseteq S$$
4		limccl	$$⊢\left(z\in \left(A\setminus \left\{B\right\}\right)⟼\frac{F\left(z\right)-F\left(B\right)}{z-B}\right){lim}_{ℂ}B\subseteq ℂ$$
5		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S$$
6		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
7		eqid	$$⊢\left(z\in \left(A\setminus \left\{B\right\}\right)⟼\frac{F\left(z\right)-F\left(B\right)}{z-B}\right)=\left(z\in \left(A\setminus \left\{B\right\}\right)⟼\frac{F\left(z\right)-F\left(B\right)}{z-B}\right)$$
8	5 6 7 1 2 3	eldv	$$⊢\phi \to \left(B{F}_S^{\prime }C\leftrightarrow \left(B\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}S\right)\left(A\right)\wedge C\in \left(\left(z\in \left(A\setminus \left\{B\right\}\right)⟼\frac{F\left(z\right)-F\left(B\right)}{z-B}\right){lim}_{ℂ}B\right)\right)\right)$$
9	8	simplbda	$$⊢\left(\phi \wedge B{F}_S^{\prime }C\right)\to C\in \left(\left(z\in \left(A\setminus \left\{B\right\}\right)⟼\frac{F\left(z\right)-F\left(B\right)}{z-B}\right){lim}_{ℂ}B\right)$$
10	4 9	sselid	$$⊢\left(\phi \wedge B{F}_S^{\prime }C\right)\to C\in ℂ$$