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 = K ↾ 𝑡 S
dvval.k ⊢ K = TopOpen ⁡ ℂ fld
eldv.g ⊢ G = z ∈ A ∖ B ⟼ F ⁡ z − F ⁡ B z − B
eldv.s ⊢ φ → S ⊆ ℂ
eldv.f ⊢ φ → F : A ⟶ ℂ
eldv.a ⊢ φ → A ⊆ S
Assertion eldv ⊢ φ → B F S ′ C ↔ B ∈ int ⁡ T ⁡ A ∧ C ∈ G lim ℂ B

Proof

Step Hyp Ref Expression
1 dvval.t ⊢ T = K ↾ 𝑡 S
2 dvval.k ⊢ K = TopOpen ⁡ ℂ fld
3 eldv.g ⊢ G = z ∈ A ∖ B ⟼ F ⁡ z − F ⁡ B z − B
4 eldv.s ⊢ φ → S ⊆ ℂ
5 eldv.f ⊢ φ → F : A ⟶ ℂ
6 eldv.a ⊢ φ → A ⊆ S
7 1 2 dvfval ⊢ S ⊆ ℂ ∧ F : A ⟶ ℂ ∧ A ⊆ S → S D F = ⋃ x ∈ int ⁡ T ⁡ A x × z ∈ A ∖ x ⟼ F ⁡ z − F ⁡ x z − x lim ℂ x ∧ S D F ⊆ int ⁡ T ⁡ A × ℂ
8 4 5 6 7 syl3anc ⊢ φ → S D F = ⋃ x ∈ int ⁡ T ⁡ A x × z ∈ A ∖ x ⟼ F ⁡ z − F ⁡ x z − x lim ℂ x ∧ S D F ⊆ int ⁡ T ⁡ A × ℂ
9 8 simpld ⊢ φ → S D F = ⋃ x ∈ int ⁡ T ⁡ A x × z ∈ A ∖ x ⟼ F ⁡ z − F ⁡ x z − x lim ℂ x
10 9 eleq2d ⊢ φ → B C ∈ F S ′ ↔ B C ∈ ⋃ x ∈ int ⁡ T ⁡ A x × z ∈ A ∖ x ⟼ F ⁡ z − F ⁡ x z − x lim ℂ x
11 df-br ⊢ B F S ′ C ↔ B C ∈ F S ′
12 11 bicomi ⊢ B C ∈ F S ′ ↔ B F S ′ C
13 sneq ⊢ x = B → x = B
14 13 difeq2d ⊢ x = B → A ∖ x = A ∖ B
15 fveq2 ⊢ x = B → F ⁡ x = F ⁡ B
16 15 oveq2d ⊢ x = B → F ⁡ z − F ⁡ x = F ⁡ z − F ⁡ B
17 oveq2 ⊢ x = B → z − x = z − B
18 16 17 oveq12d ⊢ x = B → F ⁡ z − F ⁡ x z − x = F ⁡ z − F ⁡ B z − B
19 14 18 mpteq12dv ⊢ x = B → z ∈ A ∖ x ⟼ F ⁡ z − F ⁡ x z − x = z ∈ A ∖ B ⟼ F ⁡ z − F ⁡ B z − B
20 19 3 eqtr4di ⊢ x = B → z ∈ A ∖ x ⟼ F ⁡ z − F ⁡ x z − x = G
21 id ⊢ x = B → x = B
22 20 21 oveq12d ⊢ x = B → z ∈ A ∖ x ⟼ F ⁡ z − F ⁡ x z − x lim ℂ x = G lim ℂ B
23 22 opeliunxp2 ⊢ B C ∈ ⋃ x ∈ int ⁡ T ⁡ A x × z ∈ A ∖ x ⟼ F ⁡ z − F ⁡ x z − x lim ℂ x ↔ B ∈ int ⁡ T ⁡ A ∧ C ∈ G lim ℂ B
24 10 12 23 3bitr3g ⊢ φ → B F S ′ C ↔ B ∈ int ⁡ T ⁡ A ∧ C ∈ G lim ℂ B