Theorem dvidlem

Description: Lemma for dvid and dvconst . (Contributed by Mario Carneiro, 8-Aug-2014) (Revised by Mario Carneiro, 9-Feb-2015)

	Ref	Expression
Hypotheses	dvidlem.1	$$⊢\phi \to F:ℂ⟶ℂ$$
	dvidlem.2	$$⊢\left(\phi \wedge \left(x\in ℂ\wedge z\in ℂ\wedge z\ne x\right)\right)\to \frac{F\left(z\right)-F\left(x\right)}{z-x}=B$$
	dvidlem.3	$$⊢B\in ℂ$$
Assertion	dvidlem	$$⊢\phi \to ℂ\mathrm{D}F=ℂ\times \left\{B\right\}$$

Proof

Step	Hyp	Ref	Expression
1		dvidlem.1	$$⊢\phi \to F:ℂ⟶ℂ$$
2		dvidlem.2	$$⊢\left(\phi \wedge \left(x\in ℂ\wedge z\in ℂ\wedge z\ne x\right)\right)\to \frac{F\left(z\right)-F\left(x\right)}{z-x}=B$$
3		dvidlem.3	$$⊢B\in ℂ$$
4		dvfcn	$$⊢F_{ℂ}^{\prime }:\mathrm{dom}{F}_{ℂ}^{\prime }⟶ℂ$$
5		ssidd	$$⊢\phi \to ℂ\subseteq ℂ$$
6	5 1 5	dvbss	$$⊢\phi \to \mathrm{dom}{F}_{ℂ}^{\prime }\subseteq ℂ$$
7		reldv	$$⊢\mathrm{Rel}{F}_{ℂ}^{\prime }$$
8		simpr	$$⊢\left(\phi \wedge x\in ℂ\right)\to x\in ℂ$$
9		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
10	9	cnfldtop	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}$$
11		unicntop	$$⊢ℂ=\bigcup \mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
12	11	ntrtop	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{Top}\to \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(ℂ\right)=ℂ$$
13	10 12	ax-mp	$$⊢\mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(ℂ\right)=ℂ$$
14	8 13	eleqtrrdi	$$⊢\left(\phi \wedge x\in ℂ\right)\to x\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(ℂ\right)$$
15		limcresi	$$⊢\left(z\in ℂ⟼B\right){lim}_{ℂ}x\subseteq \left({\left(z\in ℂ⟼B\right)\upharpoonright }_{\left(ℂ\setminus \left\{x\right\}\right)}\right){lim}_{ℂ}x$$
16		ssidd	$$⊢\left(\phi \wedge x\in ℂ\right)\to ℂ\subseteq ℂ$$
17		cncfmptc	$$⊢\left(B\in ℂ\wedge ℂ\subseteq ℂ\wedge ℂ\subseteq ℂ\right)\to \left(z\in ℂ⟼B\right):ℂ\underset{cn}{⟶}ℂ$$
18	3 16 16 17	mp3an2i	$$⊢\left(\phi \wedge x\in ℂ\right)\to \left(z\in ℂ⟼B\right):ℂ\underset{cn}{⟶}ℂ$$
19		eqidd	$$⊢z=x\to B=B$$
20	18 8 19	cnmptlimc	$$⊢\left(\phi \wedge x\in ℂ\right)\to B\in \left(\left(z\in ℂ⟼B\right){lim}_{ℂ}x\right)$$
21	15 20	sselid	$$⊢\left(\phi \wedge x\in ℂ\right)\to B\in \left(\left({\left(z\in ℂ⟼B\right)\upharpoonright }_{\left(ℂ\setminus \left\{x\right\}\right)}\right){lim}_{ℂ}x\right)$$
22		eldifsn	$$⊢z\in \left(ℂ\setminus \left\{x\right\}\right)\leftrightarrow \left(z\in ℂ\wedge z\ne x\right)$$
23	2	3exp2	$$⊢\phi \to \left(x\in ℂ\to \left(z\in ℂ\to \left(z\ne x\to \frac{F\left(z\right)-F\left(x\right)}{z-x}=B\right)\right)\right)$$
24	23	imp43	$$⊢\left(\left(\phi \wedge x\in ℂ\right)\wedge \left(z\in ℂ\wedge z\ne x\right)\right)\to \frac{F\left(z\right)-F\left(x\right)}{z-x}=B$$
25	22 24	sylan2b	$$⊢\left(\left(\phi \wedge x\in ℂ\right)\wedge z\in \left(ℂ\setminus \left\{x\right\}\right)\right)\to \frac{F\left(z\right)-F\left(x\right)}{z-x}=B$$
26	25	mpteq2dva	$$⊢\left(\phi \wedge x\in ℂ\right)\to \left(z\in \left(ℂ\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right)=\left(z\in \left(ℂ\setminus \left\{x\right\}\right)⟼B\right)$$
27		difss	$$⊢ℂ\setminus \left\{x\right\}\subseteq ℂ$$
28		resmpt	$$⊢ℂ\setminus \left\{x\right\}\subseteq ℂ\to {\left(z\in ℂ⟼B\right)\upharpoonright }_{\left(ℂ\setminus \left\{x\right\}\right)}=\left(z\in \left(ℂ\setminus \left\{x\right\}\right)⟼B\right)$$
29	27 28	ax-mp	$$⊢{\left(z\in ℂ⟼B\right)\upharpoonright }_{\left(ℂ\setminus \left\{x\right\}\right)}=\left(z\in \left(ℂ\setminus \left\{x\right\}\right)⟼B\right)$$
30	26 29	eqtr4di	$$⊢\left(\phi \wedge x\in ℂ\right)\to \left(z\in \left(ℂ\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right)={\left(z\in ℂ⟼B\right)\upharpoonright }_{\left(ℂ\setminus \left\{x\right\}\right)}$$
31	30	oveq1d	$$⊢\left(\phi \wedge x\in ℂ\right)\to \left(z\in \left(ℂ\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right){lim}_{ℂ}x=\left({\left(z\in ℂ⟼B\right)\upharpoonright }_{\left(ℂ\setminus \left\{x\right\}\right)}\right){lim}_{ℂ}x$$
32	21 31	eleqtrrd	$$⊢\left(\phi \wedge x\in ℂ\right)\to B\in \left(\left(z\in \left(ℂ\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)$$
33	9	cnfldtopon	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\in \mathrm{TopOn}\left(ℂ\right)$$
34	33	toponrestid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℂ$$
35		eqid	$$⊢\left(z\in \left(ℂ\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right)=\left(z\in \left(ℂ\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right)$$
36	1	adantr	$$⊢\left(\phi \wedge x\in ℂ\right)\to F:ℂ⟶ℂ$$
37	34 9 35 16 36 16	eldv	$$⊢\left(\phi \wedge x\in ℂ\right)\to \left(x{F}_{ℂ}^{\prime }B\leftrightarrow \left(x\in \mathrm{int}\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\left(ℂ\right)\wedge B\in \left(\left(z\in \left(ℂ\setminus \left\{x\right\}\right)⟼\frac{F\left(z\right)-F\left(x\right)}{z-x}\right){lim}_{ℂ}x\right)\right)\right)$$
38	14 32 37	mpbir2and	$$⊢\left(\phi \wedge x\in ℂ\right)\to x{F}_{ℂ}^{\prime }B$$
39		releldm	$$⊢\left(\mathrm{Rel}{F}_{ℂ}^{\prime }\wedge x{F}_{ℂ}^{\prime }B\right)\to x\in \mathrm{dom}{F}_{ℂ}^{\prime }$$
40	7 38 39	sylancr	$$⊢\left(\phi \wedge x\in ℂ\right)\to x\in \mathrm{dom}{F}_{ℂ}^{\prime }$$
41	6 40	eqelssd	$$⊢\phi \to \mathrm{dom}{F}_{ℂ}^{\prime }=ℂ$$
42	41	feq2d	$$⊢\phi \to \left(F_{ℂ}^{\prime }:\mathrm{dom}{F}_{ℂ}^{\prime }⟶ℂ\leftrightarrow F_{ℂ}^{\prime }:ℂ⟶ℂ\right)$$
43	4 42	mpbii	$$⊢\phi \to F_{ℂ}^{\prime }:ℂ⟶ℂ$$
44	43	ffnd	$$⊢\phi \to F_{ℂ}^{\prime }Fnℂ$$
45		fnconstg	$$⊢B\in ℂ\to \left(ℂ\times \left\{B\right\}\right)Fnℂ$$
46	3 45	mp1i	$$⊢\phi \to \left(ℂ\times \left\{B\right\}\right)Fnℂ$$
47		ffun	$$⊢F_{ℂ}^{\prime }:\mathrm{dom}{F}_{ℂ}^{\prime }⟶ℂ\to \mathrm{Fun}{F}_{ℂ}^{\prime }$$
48	4 47	mp1i	$$⊢\left(\phi \wedge x\in ℂ\right)\to \mathrm{Fun}{F}_{ℂ}^{\prime }$$
49		funbrfvb	$$⊢\left(\mathrm{Fun}{F}_{ℂ}^{\prime }\wedge x\in \mathrm{dom}{F}_{ℂ}^{\prime }\right)\to \left(F_{ℂ}^{\prime }\left(x\right)=B\leftrightarrow x{F}_{ℂ}^{\prime }B\right)$$
50	48 40 49	syl2anc	$$⊢\left(\phi \wedge x\in ℂ\right)\to \left(F_{ℂ}^{\prime }\left(x\right)=B\leftrightarrow x{F}_{ℂ}^{\prime }B\right)$$
51	38 50	mpbird	$$⊢\left(\phi \wedge x\in ℂ\right)\to F_{ℂ}^{\prime }\left(x\right)=B$$
52	3	a1i	$$⊢\phi \to B\in ℂ$$
53		fvconst2g	$$⊢\left(B\in ℂ\wedge x\in ℂ\right)\to \left(ℂ\times \left\{B\right\}\right)\left(x\right)=B$$
54	52 53	sylan	$$⊢\left(\phi \wedge x\in ℂ\right)\to \left(ℂ\times \left\{B\right\}\right)\left(x\right)=B$$
55	51 54	eqtr4d	$$⊢\left(\phi \wedge x\in ℂ\right)\to F_{ℂ}^{\prime }\left(x\right)=\left(ℂ\times \left\{B\right\}\right)\left(x\right)$$
56	44 46 55	eqfnfvd	$$⊢\phi \to ℂ\mathrm{D}F=ℂ\times \left\{B\right\}$$