dvcnp

Description: The difference quotient is continuous at B when the original function is differentiable at B . (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 28-Dec-2016)

	Ref	Expression
Hypotheses	dvcnp.j	$⊢ J = K ↾_{𝑡} A$
	dvcnp.k	$⊢ K = TopOpen (ℂ_{fld})$
	dvcnp.g	$⊢ G = (z \in A ⟼ if (z = B, F_{S}^{'} (B), \frac{F (z) - F (B)}{z - B}))$
Assertion	dvcnp	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \land B \in dom F_{S}^{'}) \to G \in (J CnP K) (B)$

Proof

Step	Hyp	Ref	Expression
1		dvcnp.j	$⊢ J = K ↾_{𝑡} A$
2		dvcnp.k	$⊢ K = TopOpen (ℂ_{fld})$
3		dvcnp.g	$⊢ G = (z \in A ⟼ if (z = B, F_{S}^{'} (B), \frac{F (z) - F (B)}{z - B}))$
4		dvfg	$⊢ S \in \{ℝ, ℂ\} \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
5	4	3ad2ant1	$⊢ (S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \to F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ$
6		ffun	$⊢ F_{S}^{'} : dom F_{S}^{'} ⟶ ℂ \to Fun F_{S}^{'}$
7		funfvbrb	$⊢ Fun F_{S}^{'} \to (B \in dom F_{S}^{'} \leftrightarrow B F_{S}^{'} F_{S}^{'} (B))$
8	5 6 7	3syl	$⊢ (S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \to (B \in dom F_{S}^{'} \leftrightarrow B F_{S}^{'} F_{S}^{'} (B))$
9		eqid	$⊢ K ↾_{𝑡} S = K ↾_{𝑡} S$
10		eqid	$⊢ (z \in (A ∖ \{B\}) ⟼ \frac{F (z) - F (B)}{z - B}) = (z \in (A ∖ \{B\}) ⟼ \frac{F (z) - F (B)}{z - B})$
11		recnprss	$⊢ S \in \{ℝ, ℂ\} \to S \subseteq ℂ$
12	11	3ad2ant1	$⊢ (S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \to S \subseteq ℂ$
13		simp2	$⊢ (S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \to F : A ⟶ ℂ$
14		simp3	$⊢ (S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \to A \subseteq S$
15	9 2 10 12 13 14	eldv	$⊢ (S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \to (B F_{S}^{'} F_{S}^{'} (B) \leftrightarrow (B \in int (K ↾_{𝑡} S) (A) \land F_{S}^{'} (B) \in ((z \in (A ∖ \{B\}) ⟼ \frac{F (z) - F (B)}{z - B}) {lim}_{ℂ} B)))$
16	8 15	bitrd	$⊢ (S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \to (B \in dom F_{S}^{'} \leftrightarrow (B \in int (K ↾_{𝑡} S) (A) \land F_{S}^{'} (B) \in ((z \in (A ∖ \{B\}) ⟼ \frac{F (z) - F (B)}{z - B}) {lim}_{ℂ} B)))$
17	16	simplbda	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \land B \in dom F_{S}^{'}) \to F_{S}^{'} (B) \in ((z \in (A ∖ \{B\}) ⟼ \frac{F (z) - F (B)}{z - B}) {lim}_{ℂ} B)$
18	14 12	sstrd	$⊢ (S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \to A \subseteq ℂ$
19	18	adantr	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \land B \in dom F_{S}^{'}) \to A \subseteq ℂ$
20	12 13 14	dvbss	$⊢ (S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \to dom F_{S}^{'} \subseteq A$
21	20	sselda	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \land B \in dom F_{S}^{'}) \to B \in A$
22		eldifsn	$⊢ z \in (A ∖ \{B\}) \leftrightarrow (z \in A \land z \neq B)$
23	13	adantr	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \land B \in dom F_{S}^{'}) \to F : A ⟶ ℂ$
24	23 19 21	dvlem	$⊢ (((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \land B \in dom F_{S}^{'}) \land z \in (A ∖ \{B\})) \to \frac{F (z) - F (B)}{z - B} \in ℂ$
25	22 24	sylan2br	$⊢ (((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \land B \in dom F_{S}^{'}) \land (z \in A \land z \neq B)) \to \frac{F (z) - F (B)}{z - B} \in ℂ$
26	19 21 25 1 2	limcmpt2	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \land B \in dom F_{S}^{'}) \to (F_{S}^{'} (B) \in ((z \in (A ∖ \{B\}) ⟼ \frac{F (z) - F (B)}{z - B}) {lim}_{ℂ} B) \leftrightarrow (z \in A ⟼ if (z = B, F_{S}^{'} (B), \frac{F (z) - F (B)}{z - B})) \in (J CnP K) (B))$
27	17 26	mpbid	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \land B \in dom F_{S}^{'}) \to (z \in A ⟼ if (z = B, F_{S}^{'} (B), \frac{F (z) - F (B)}{z - B})) \in (J CnP K) (B)$
28	3 27	eqeltrid	$⊢ ((S \in \{ℝ, ℂ\} \land F : A ⟶ ℂ \land A \subseteq S) \land B \in dom F_{S}^{'}) \to G \in (J CnP K) (B)$

Metamath Proof Explorer

Theorem dvcnp

Proof