Theorem eldv

Description: The differentiable predicate. A function F is differentiable at B with derivative C iff F is defined in a neighborhood of B and the difference quotient has limit C at B . (Contributed by Mario Carneiro, 7-Aug-2014) (Revised by Mario Carneiro, 25-Dec-2016)

	Ref	Expression
Hypotheses	dvval.t	⊢ 𝑇 = ( 𝐾 ↾t 𝑆 )
	dvval.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
	eldv.g	⊢ 𝐺 = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) )
	eldv.s	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
	eldv.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
	eldv.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
Assertion	eldv	⊢ ( 𝜑 → ( 𝐵 ( 𝑆 D 𝐹 ) 𝐶 ↔ ( 𝐵 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∧ 𝐶 ∈ ( 𝐺 limℂ 𝐵 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvval.t	⊢ 𝑇 = ( 𝐾 ↾t 𝑆 )
2		dvval.k	⊢ 𝐾 = ( TopOpen ‘ ℂfld )
3		eldv.g	⊢ 𝐺 = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) )
4		eldv.s	⊢ ( 𝜑 → 𝑆 ⊆ ℂ )
5		eldv.f	⊢ ( 𝜑 → 𝐹 : 𝐴 ⟶ ℂ )
6		eldv.a	⊢ ( 𝜑 → 𝐴 ⊆ 𝑆 )
7	1 2	dvfval	⊢ ( ( 𝑆 ⊆ ℂ ∧ 𝐹 : 𝐴 ⟶ ℂ ∧ 𝐴 ⊆ 𝑆 ) → ( ( 𝑆 D 𝐹 ) = ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ∧ ( 𝑆 D 𝐹 ) ⊆ ( ( ( int ‘ 𝑇 ) ‘ 𝐴 ) × ℂ ) ) )
8	4 5 6 7	syl3anc	⊢ ( 𝜑 → ( ( 𝑆 D 𝐹 ) = ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ∧ ( 𝑆 D 𝐹 ) ⊆ ( ( ( int ‘ 𝑇 ) ‘ 𝐴 ) × ℂ ) ) )
9	8	simpld	⊢ ( 𝜑 → ( 𝑆 D 𝐹 ) = ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) )
10	9	eleq2d	⊢ ( 𝜑 → ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑆 D 𝐹 ) ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ) )
11		df-br	⊢ ( 𝐵 ( 𝑆 D 𝐹 ) 𝐶 ↔ ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑆 D 𝐹 ) )
12	11	bicomi	⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ( 𝑆 D 𝐹 ) ↔ 𝐵 ( 𝑆 D 𝐹 ) 𝐶 )
13		sneq	⊢ ( 𝑥 = 𝐵 → { 𝑥 } = { 𝐵 } )
14	13	difeq2d	⊢ ( 𝑥 = 𝐵 → ( 𝐴 ∖ { 𝑥 } ) = ( 𝐴 ∖ { 𝐵 } ) )
15		fveq2	⊢ ( 𝑥 = 𝐵 → ( 𝐹 ‘ 𝑥 ) = ( 𝐹 ‘ 𝐵 ) )
16	15	oveq2d	⊢ ( 𝑥 = 𝐵 → ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) = ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) )
17		oveq2	⊢ ( 𝑥 = 𝐵 → ( 𝑧 − 𝑥 ) = ( 𝑧 − 𝐵 ) )
18	16 17	oveq12d	⊢ ( 𝑥 = 𝐵 → ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) = ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) )
19	14 18	mpteq12dv	⊢ ( 𝑥 = 𝐵 → ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) = ( 𝑧 ∈ ( 𝐴 ∖ { 𝐵 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝐵 ) ) / ( 𝑧 − 𝐵 ) ) ) )
20	19 3	eqtr4di	⊢ ( 𝑥 = 𝐵 → ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) = 𝐺 )
21		id	⊢ ( 𝑥 = 𝐵 → 𝑥 = 𝐵 )
22	20 21	oveq12d	⊢ ( 𝑥 = 𝐵 → ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) = ( 𝐺 limℂ 𝐵 ) )
23	22	opeliunxp2	⊢ ( ⟨ 𝐵 , 𝐶 ⟩ ∈ ∪ 𝑥 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ( { 𝑥 } × ( ( 𝑧 ∈ ( 𝐴 ∖ { 𝑥 } ) ↦ ( ( ( 𝐹 ‘ 𝑧 ) − ( 𝐹 ‘ 𝑥 ) ) / ( 𝑧 − 𝑥 ) ) ) limℂ 𝑥 ) ) ↔ ( 𝐵 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∧ 𝐶 ∈ ( 𝐺 limℂ 𝐵 ) ) )
24	10 12 23	3bitr3g	⊢ ( 𝜑 → ( 𝐵 ( 𝑆 D 𝐹 ) 𝐶 ↔ ( 𝐵 ∈ ( ( int ‘ 𝑇 ) ‘ 𝐴 ) ∧ 𝐶 ∈ ( 𝐺 limℂ 𝐵 ) ) ) )