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	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
	dvcl.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	dvcl.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
Assertion	dvcl	⊢ ( ( 𝜑 ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝐶 ) → 𝐶 ∈ ℂ )

Proof

Step	Hyp	Ref	Expression
1		dvcl.s	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
2		dvcl.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
3		dvcl.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
4		limccl	⊢ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) ⊆ ℂ
5		eqid	⊢ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) = ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 )
6		eqid	⊢ ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
7		eqid	⊢ ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) )
8	5 6 7 1 2 3	eldv	⊢ ( 𝜑 → ( 𝐵 ( 𝑆 D 𝐹 ) 𝐶 ↔ ( 𝐵 ∈ ( ( int ‘ ( ( TopOpen ‘ ℂfld ) ↾t 𝑆 ) ) ‘ 𝐴 ) ∧ 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) ) ) )
9	8	simplbda	⊢ ( ( 𝜑 ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝐶 ) → 𝐶 ∈ ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) limℂ 𝐵 ) )
10	4 9	sselid	⊢ ( ( 𝜑 ∧ 𝐵 ( 𝑆 D 𝐹 ) 𝐶 ) → 𝐶 ∈ ℂ )