Theorem dvef

Description: Derivative of the exponential function. (Contributed by Mario Carneiro, 9-Aug-2014) (Proof shortened by Mario Carneiro, 10-Feb-2015)

	Ref	Expression
Assertion	dvef	$$⊢ℂ\mathrm{D}\exp =\exp$$

Proof

Step	Hyp	Ref	Expression
1		dvfcn	$$⊢{\exp }_{ℂ}^{\prime }:\mathrm{dom}{\exp }_{ℂ}^{\prime }⟶ℂ$$
2		dvbsss	$$⊢\mathrm{dom}{\exp }_{ℂ}^{\prime }\subseteq ℂ$$
3		subcl	$$⊢\left(z\in ℂ\wedge x\in ℂ\right)\to z-x\in ℂ$$
4	3	ancoms	$$⊢\left(x\in ℂ\wedge z\in ℂ\right)\to z-x\in ℂ$$
5		efadd	$$⊢\left(x\in ℂ\wedge z-x\in ℂ\right)\to {\mathrm{e}}^{x+z-x}={\mathrm{e}}^x{\mathrm{e}}^{z-x}$$
6	4 5	syldan	$$⊢\left(x\in ℂ\wedge z\in ℂ\right)\to {\mathrm{e}}^{x+z-x}={\mathrm{e}}^x{\mathrm{e}}^{z-x}$$
7		pncan3	$$⊢\left(x\in ℂ\wedge z\in ℂ\right)\to x+z-x=z$$
8	7	fveq2d	$$⊢\left(x\in ℂ\wedge z\in ℂ\right)\to {\mathrm{e}}^{x+z-x}={\mathrm{e}}^z$$
9	6 8	eqtr3d	$$⊢\left(x\in ℂ\wedge z\in ℂ\right)\to {\mathrm{e}}^x{\mathrm{e}}^{z-x}={\mathrm{e}}^z$$
10	9	mpteq2dva	$$⊢x\in ℂ\to \left(z\in ℂ⟼{\mathrm{e}}^x{\mathrm{e}}^{z-x}\right)=\left(z\in ℂ⟼{\mathrm{e}}^z\right)$$
11		cnex	$$⊢ℂ\in \mathrm{V}$$
12	11	a1i	$$⊢x\in ℂ\to ℂ\in \mathrm{V}$$
13		fvexd	$$⊢\left(x\in ℂ\wedge z\in ℂ\right)\to {\mathrm{e}}^x\in \mathrm{V}$$
14		fvexd	$$⊢\left(x\in ℂ\wedge z\in ℂ\right)\to {\mathrm{e}}^{z-x}\in \mathrm{V}$$
15		fconstmpt	$$⊢ℂ\times \left\{{\mathrm{e}}^x\right\}=\left(z\in ℂ⟼{\mathrm{e}}^x\right)$$
16	15	a1i	$$⊢x\in ℂ\to ℂ\times \left\{{\mathrm{e}}^x\right\}=\left(z\in ℂ⟼{\mathrm{e}}^x\right)$$
17		eqidd	$$⊢x\in ℂ\to \left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)=\left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)$$
18	12 13 14 16 17	offval2	$$⊢x\in ℂ\to \left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right){\times }_f\left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)=\left(z\in ℂ⟼{\mathrm{e}}^x{\mathrm{e}}^{z-x}\right)$$
19		eff	$$⊢\exp :ℂ⟶ℂ$$
20	19	a1i	$$⊢x\in ℂ\to \exp :ℂ⟶ℂ$$
21	20	feqmptd	$$⊢x\in ℂ\to \exp =\left(z\in ℂ⟼{\mathrm{e}}^z\right)$$
22	10 18 21	3eqtr4d	$$⊢x\in ℂ\to \left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right){\times }_f\left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)=\exp$$
23	22	oveq2d	$$⊢x\in ℂ\to ℂ\mathrm{D}\left(\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right){\times }_f\left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)\right)=ℂ\mathrm{D}\exp$$
24		efcl	$$⊢x\in ℂ\to {\mathrm{e}}^x\in ℂ$$
25		fconstg	$$⊢{\mathrm{e}}^x\in ℂ\to \left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right):ℂ⟶\left\{{\mathrm{e}}^x\right\}$$
26	24 25	syl	$$⊢x\in ℂ\to \left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right):ℂ⟶\left\{{\mathrm{e}}^x\right\}$$
27	24	snssd	$$⊢x\in ℂ\to \left\{{\mathrm{e}}^x\right\}\subseteq ℂ$$
28	26 27	fssd	$$⊢x\in ℂ\to \left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right):ℂ⟶ℂ$$
29		ssidd	$$⊢x\in ℂ\to ℂ\subseteq ℂ$$
30		efcl	$$⊢z-x\in ℂ\to {\mathrm{e}}^{z-x}\in ℂ$$
31	4 30	syl	$$⊢\left(x\in ℂ\wedge z\in ℂ\right)\to {\mathrm{e}}^{z-x}\in ℂ$$
32	31	fmpttd	$$⊢x\in ℂ\to \left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right):ℂ⟶ℂ$$
33		0cnd	$$⊢x\in ℂ\to 0\in ℂ$$
34		1cnd	$$⊢x\in ℂ\to 1\in ℂ$$
35		c0ex	$$⊢0\in \mathrm{V}$$
36	35	snid	$$⊢0\in \left\{0\right\}$$
37		opelxpi	$$⊢\left(x\in ℂ\wedge 0\in \left\{0\right\}\right)\to ⟨x,0⟩\in \left(ℂ\times \left\{0\right\}\right)$$
38	36 37	mpan2	$$⊢x\in ℂ\to ⟨x,0⟩\in \left(ℂ\times \left\{0\right\}\right)$$
39		dvconst	$$⊢{\mathrm{e}}^x\in ℂ\to ℂ\mathrm{D}\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)=ℂ\times \left\{0\right\}$$
40	24 39	syl	$$⊢x\in ℂ\to ℂ\mathrm{D}\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)=ℂ\times \left\{0\right\}$$
41	38 40	eleqtrrd	$$⊢x\in ℂ\to ⟨x,0⟩\in {\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)}_{ℂ}^{\prime }$$
42		df-br	$$⊢x{\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)}_{ℂ}^{\prime }0\leftrightarrow ⟨x,0⟩\in {\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)}_{ℂ}^{\prime }$$
43	41 42	sylibr	$$⊢x\in ℂ\to x{\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)}_{ℂ}^{\prime }0$$
44	20 4	cofmpt	$$⊢x\in ℂ\to \exp \circ \left(z\in ℂ⟼z-x\right)=\left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)$$
45	44	oveq2d	$$⊢x\in ℂ\to ℂ\mathrm{D}\left(\exp \circ \left(z\in ℂ⟼z-x\right)\right)=\frac{d\left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)}{d_{ℂ}z}$$
46	4	fmpttd	$$⊢x\in ℂ\to \left(z\in ℂ⟼z-x\right):ℂ⟶ℂ$$
47		oveq1	$$⊢z=x\to z-x=x-x$$
48		eqid	$$⊢\left(z\in ℂ⟼z-x\right)=\left(z\in ℂ⟼z-x\right)$$
49		ovex	$$⊢x-x\in \mathrm{V}$$
50	47 48 49	fvmpt	$$⊢x\in ℂ\to \left(z\in ℂ⟼z-x\right)\left(x\right)=x-x$$
51		subid	$$⊢x\in ℂ\to x-x=0$$
52	50 51	eqtrd	$$⊢x\in ℂ\to \left(z\in ℂ⟼z-x\right)\left(x\right)=0$$
53		dveflem	$$⊢0{\exp }_{ℂ}^{\prime }1$$
54	52 53	eqbrtrdi	$$⊢x\in ℂ\to \left(z\in ℂ⟼z-x\right)\left(x\right){\exp }_{ℂ}^{\prime }1$$
55		1ex	$$⊢1\in \mathrm{V}$$
56	55	snid	$$⊢1\in \left\{1\right\}$$
57		opelxpi	$$⊢\left(x\in ℂ\wedge 1\in \left\{1\right\}\right)\to ⟨x,1⟩\in \left(ℂ\times \left\{1\right\}\right)$$
58	56 57	mpan2	$$⊢x\in ℂ\to ⟨x,1⟩\in \left(ℂ\times \left\{1\right\}\right)$$
59		cnelprrecn	$$⊢ℂ\in \left\{ℝ,ℂ\right\}$$
60	59	a1i	$$⊢x\in ℂ\to ℂ\in \left\{ℝ,ℂ\right\}$$
61		simpr	$$⊢\left(x\in ℂ\wedge z\in ℂ\right)\to z\in ℂ$$
62		1cnd	$$⊢\left(x\in ℂ\wedge z\in ℂ\right)\to 1\in ℂ$$
63	60	dvmptid	$$⊢x\in ℂ\to \frac{d\left(z\in ℂ⟼z\right)}{d_{ℂ}z}=\left(z\in ℂ⟼1\right)$$
64		simpl	$$⊢\left(x\in ℂ\wedge z\in ℂ\right)\to x\in ℂ$$
65		0cnd	$$⊢\left(x\in ℂ\wedge z\in ℂ\right)\to 0\in ℂ$$
66		id	$$⊢x\in ℂ\to x\in ℂ$$
67	60 66	dvmptc	$$⊢x\in ℂ\to \frac{d\left(z\in ℂ⟼x\right)}{d_{ℂ}z}=\left(z\in ℂ⟼0\right)$$
68	60 61 62 63 64 65 67	dvmptsub	$$⊢x\in ℂ\to \frac{d\left(z\in ℂ⟼z-x\right)}{d_{ℂ}z}=\left(z\in ℂ⟼1-0\right)$$
69		1m0e1	$$⊢1-0=1$$
70	69	mpteq2i	$$⊢\left(z\in ℂ⟼1-0\right)=\left(z\in ℂ⟼1\right)$$
71		fconstmpt	$$⊢ℂ\times \left\{1\right\}=\left(z\in ℂ⟼1\right)$$
72	70 71	eqtr4i	$$⊢\left(z\in ℂ⟼1-0\right)=ℂ\times \left\{1\right\}$$
73	68 72	eqtrdi	$$⊢x\in ℂ\to \frac{d\left(z\in ℂ⟼z-x\right)}{d_{ℂ}z}=ℂ\times \left\{1\right\}$$
74	58 73	eleqtrrd	$$⊢x\in ℂ\to ⟨x,1⟩\in \frac{d\left(z\in ℂ⟼z-x\right)}{d_{ℂ}z}$$
75		df-br	$$⊢x\frac{d\left(z\in ℂ⟼z-x\right)}{d_{ℂ}z}1\leftrightarrow ⟨x,1⟩\in \frac{d\left(z\in ℂ⟼z-x\right)}{d_{ℂ}z}$$
76	74 75	sylibr	$$⊢x\in ℂ\to x\frac{d\left(z\in ℂ⟼z-x\right)}{d_{ℂ}z}1$$
77		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
78	20 29 46 29 29 29 34 34 54 76 77	dvcobr	$$⊢x\in ℂ\to x{\left(\exp \circ \left(z\in ℂ⟼z-x\right)\right)}_{ℂ}^{\prime }1\cdot 1$$
79		1t1e1	$$⊢1\cdot 1=1$$
80	78 79	breqtrdi	$$⊢x\in ℂ\to x{\left(\exp \circ \left(z\in ℂ⟼z-x\right)\right)}_{ℂ}^{\prime }1$$
81	45 80	breqdi	$$⊢x\in ℂ\to x\frac{d\left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)}{d_{ℂ}z}1$$
82	28 29 32 29 29 33 34 43 81 77	dvmulbr	$$⊢x\in ℂ\to x{\left(\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right){\times }_f\left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)\right)}_{ℂ}^{\prime }\left(0\cdot \left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)\left(x\right)+1\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)\left(x\right)\right)$$
83	32 66	ffvelrnd	$$⊢x\in ℂ\to \left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)\left(x\right)\in ℂ$$
84	83	mul02d	$$⊢x\in ℂ\to 0\cdot \left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)\left(x\right)=0$$
85		fvex	$$⊢{\mathrm{e}}^x\in \mathrm{V}$$
86	85	fvconst2	$$⊢x\in ℂ\to \left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)\left(x\right)={\mathrm{e}}^x$$
87	86	oveq2d	$$⊢x\in ℂ\to 1\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)\left(x\right)=1{\mathrm{e}}^x$$
88	24	mulid2d	$$⊢x\in ℂ\to 1{\mathrm{e}}^x={\mathrm{e}}^x$$
89	87 88	eqtrd	$$⊢x\in ℂ\to 1\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)\left(x\right)={\mathrm{e}}^x$$
90	84 89	oveq12d	$$⊢x\in ℂ\to 0\cdot \left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)\left(x\right)+1\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)\left(x\right)=0+{\mathrm{e}}^x$$
91	24	addid2d	$$⊢x\in ℂ\to 0+{\mathrm{e}}^x={\mathrm{e}}^x$$
92	90 91	eqtrd	$$⊢x\in ℂ\to 0\cdot \left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)\left(x\right)+1\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)\left(x\right)={\mathrm{e}}^x$$
93	82 92	breqtrd	$$⊢x\in ℂ\to x{\left(\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right){\times }_f\left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)\right)}_{ℂ}^{\prime }{\mathrm{e}}^x$$
94	23 93	breqdi	$$⊢x\in ℂ\to x{\exp }_{ℂ}^{\prime }{\mathrm{e}}^x$$
95		vex	$$⊢x\in \mathrm{V}$$
96	95 85	breldm	$$⊢x{\exp }_{ℂ}^{\prime }{\mathrm{e}}^x\to x\in \mathrm{dom}{\exp }_{ℂ}^{\prime }$$
97	94 96	syl	$$⊢x\in ℂ\to x\in \mathrm{dom}{\exp }_{ℂ}^{\prime }$$
98	97	ssriv	$$⊢ℂ\subseteq \mathrm{dom}{\exp }_{ℂ}^{\prime }$$
99	2 98	eqssi	$$⊢\mathrm{dom}{\exp }_{ℂ}^{\prime }=ℂ$$
100	99	feq2i	$$⊢{\exp }_{ℂ}^{\prime }:\mathrm{dom}{\exp }_{ℂ}^{\prime }⟶ℂ\leftrightarrow {\exp }_{ℂ}^{\prime }:ℂ⟶ℂ$$
101	1 100	mpbi	$$⊢{\exp }_{ℂ}^{\prime }:ℂ⟶ℂ$$
102	101	a1i	$$⊢\top \to {\exp }_{ℂ}^{\prime }:ℂ⟶ℂ$$
103	102	feqmptd	$$⊢\top \to ℂ\mathrm{D}\exp =\left(x\in ℂ⟼{\exp }_{ℂ}^{\prime }\left(x\right)\right)$$
104		ffun	$$⊢{\exp }_{ℂ}^{\prime }:\mathrm{dom}{\exp }_{ℂ}^{\prime }⟶ℂ\to \mathrm{Fun}{\exp }_{ℂ}^{\prime }$$
105	1 104	ax-mp	$$⊢\mathrm{Fun}{\exp }_{ℂ}^{\prime }$$
106		funbrfv	$$⊢\mathrm{Fun}{\exp }_{ℂ}^{\prime }\to \left(x{\exp }_{ℂ}^{\prime }{\mathrm{e}}^x\to {\exp }_{ℂ}^{\prime }\left(x\right)={\mathrm{e}}^x\right)$$
107	105 94 106	mpsyl	$$⊢x\in ℂ\to {\exp }_{ℂ}^{\prime }\left(x\right)={\mathrm{e}}^x$$
108	107	mpteq2ia	$$⊢\left(x\in ℂ⟼{\exp }_{ℂ}^{\prime }\left(x\right)\right)=\left(x\in ℂ⟼{\mathrm{e}}^x\right)$$
109	103 108	eqtrdi	$$⊢\top \to ℂ\mathrm{D}\exp =\left(x\in ℂ⟼{\mathrm{e}}^x\right)$$
110	19	a1i	$$⊢\top \to \exp :ℂ⟶ℂ$$
111	110	feqmptd	$$⊢\top \to \exp =\left(x\in ℂ⟼{\mathrm{e}}^x\right)$$
112	109 111	eqtr4d	$$⊢\top \to ℂ\mathrm{D}\exp =\exp$$
113	112	mptru	$$⊢ℂ\mathrm{D}\exp =\exp$$