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

Metamath Proof Explorer

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ℂ 𝐵 ) ) ) )