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		c0ex	$$⊢0\in \mathrm{V}$$
34	33	snid	$$⊢0\in \left\{0\right\}$$
35		opelxpi	$$⊢\left(x\in ℂ\wedge 0\in \left\{0\right\}\right)\to ⟨x,0⟩\in \left(ℂ\times \left\{0\right\}\right)$$
36	34 35	mpan2	$$⊢x\in ℂ\to ⟨x,0⟩\in \left(ℂ\times \left\{0\right\}\right)$$
37		dvconst	$$⊢{\mathrm{e}}^x\in ℂ\to ℂ\mathrm{D}\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)=ℂ\times \left\{0\right\}$$
38	24 37	syl	$$⊢x\in ℂ\to ℂ\mathrm{D}\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)=ℂ\times \left\{0\right\}$$
39	36 38	eleqtrrd	$$⊢x\in ℂ\to ⟨x,0⟩\in {\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)}_{ℂ}^{\prime }$$
40		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 }$$
41	39 40	sylibr	$$⊢x\in ℂ\to x{\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)}_{ℂ}^{\prime }0$$
42	20 4	cofmpt	$$⊢x\in ℂ\to \exp \circ \left(z\in ℂ⟼z-x\right)=\left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)$$
43	42	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}$$
44	4	fmpttd	$$⊢x\in ℂ\to \left(z\in ℂ⟼z-x\right):ℂ⟶ℂ$$
45		oveq1	$$⊢z=x\to z-x=x-x$$
46		eqid	$$⊢\left(z\in ℂ⟼z-x\right)=\left(z\in ℂ⟼z-x\right)$$
47		ovex	$$⊢x-x\in \mathrm{V}$$
48	45 46 47	fvmpt	$$⊢x\in ℂ\to \left(z\in ℂ⟼z-x\right)\left(x\right)=x-x$$
49		subid	$$⊢x\in ℂ\to x-x=0$$
50	48 49	eqtrd	$$⊢x\in ℂ\to \left(z\in ℂ⟼z-x\right)\left(x\right)=0$$
51		dveflem	$$⊢0{\exp }_{ℂ}^{\prime }1$$
52	50 51	eqbrtrdi	$$⊢x\in ℂ\to \left(z\in ℂ⟼z-x\right)\left(x\right){\exp }_{ℂ}^{\prime }1$$
53		1ex	$$⊢1\in \mathrm{V}$$
54	53	snid	$$⊢1\in \left\{1\right\}$$
55		opelxpi	$$⊢\left(x\in ℂ\wedge 1\in \left\{1\right\}\right)\to ⟨x,1⟩\in \left(ℂ\times \left\{1\right\}\right)$$
56	54 55	mpan2	$$⊢x\in ℂ\to ⟨x,1⟩\in \left(ℂ\times \left\{1\right\}\right)$$
57		cnelprrecn	$$⊢ℂ\in \left\{ℝ,ℂ\right\}$$
58	57	a1i	$$⊢x\in ℂ\to ℂ\in \left\{ℝ,ℂ\right\}$$
59		simpr	$$⊢\left(x\in ℂ\wedge z\in ℂ\right)\to z\in ℂ$$
60		1cnd	$$⊢\left(x\in ℂ\wedge z\in ℂ\right)\to 1\in ℂ$$
61	58	dvmptid	$$⊢x\in ℂ\to \frac{d\left(z\in ℂ⟼z\right)}{d_{ℂ}z}=\left(z\in ℂ⟼1\right)$$
62		simpl	$$⊢\left(x\in ℂ\wedge z\in ℂ\right)\to x\in ℂ$$
63		0cnd	$$⊢\left(x\in ℂ\wedge z\in ℂ\right)\to 0\in ℂ$$
64		id	$$⊢x\in ℂ\to x\in ℂ$$
65	58 64	dvmptc	$$⊢x\in ℂ\to \frac{d\left(z\in ℂ⟼x\right)}{d_{ℂ}z}=\left(z\in ℂ⟼0\right)$$
66	58 59 60 61 62 63 65	dvmptsub	$$⊢x\in ℂ\to \frac{d\left(z\in ℂ⟼z-x\right)}{d_{ℂ}z}=\left(z\in ℂ⟼1-0\right)$$
67		1m0e1	$$⊢1-0=1$$
68	67	mpteq2i	$$⊢\left(z\in ℂ⟼1-0\right)=\left(z\in ℂ⟼1\right)$$
69		fconstmpt	$$⊢ℂ\times \left\{1\right\}=\left(z\in ℂ⟼1\right)$$
70	68 69	eqtr4i	$$⊢\left(z\in ℂ⟼1-0\right)=ℂ\times \left\{1\right\}$$
71	66 70	eqtrdi	$$⊢x\in ℂ\to \frac{d\left(z\in ℂ⟼z-x\right)}{d_{ℂ}z}=ℂ\times \left\{1\right\}$$
72	56 71	eleqtrrd	$$⊢x\in ℂ\to ⟨x,1⟩\in \frac{d\left(z\in ℂ⟼z-x\right)}{d_{ℂ}z}$$
73		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}$$
74	72 73	sylibr	$$⊢x\in ℂ\to x\frac{d\left(z\in ℂ⟼z-x\right)}{d_{ℂ}z}1$$
75		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
76	20 29 44 29 29 29 52 74 75	dvcobr	$$⊢x\in ℂ\to x{\left(\exp \circ \left(z\in ℂ⟼z-x\right)\right)}_{ℂ}^{\prime }1\cdot 1$$
77		1t1e1	$$⊢1\cdot 1=1$$
78	76 77	breqtrdi	$$⊢x\in ℂ\to x{\left(\exp \circ \left(z\in ℂ⟼z-x\right)\right)}_{ℂ}^{\prime }1$$
79	43 78	breqdi	$$⊢x\in ℂ\to x\frac{d\left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)}{d_{ℂ}z}1$$
80	28 29 32 29 29 41 79 75	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)$$
81	32 64	ffvelcdmd	$$⊢x\in ℂ\to \left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)\left(x\right)\in ℂ$$
82	81	mul02d	$$⊢x\in ℂ\to 0\cdot \left(z\in ℂ⟼{\mathrm{e}}^{z-x}\right)\left(x\right)=0$$
83		fvex	$$⊢{\mathrm{e}}^x\in \mathrm{V}$$
84	83	fvconst2	$$⊢x\in ℂ\to \left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)\left(x\right)={\mathrm{e}}^x$$
85	84	oveq2d	$$⊢x\in ℂ\to 1\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)\left(x\right)=1{\mathrm{e}}^x$$
86	24	mullidd	$$⊢x\in ℂ\to 1{\mathrm{e}}^x={\mathrm{e}}^x$$
87	85 86	eqtrd	$$⊢x\in ℂ\to 1\left(ℂ\times \left\{{\mathrm{e}}^x\right\}\right)\left(x\right)={\mathrm{e}}^x$$
88	82 87	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$$
89	24	addlidd	$$⊢x\in ℂ\to 0+{\mathrm{e}}^x={\mathrm{e}}^x$$
90	88 89	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$$
91	80 90	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$$
92	23 91	breqdi	$$⊢x\in ℂ\to x{\exp }_{ℂ}^{\prime }{\mathrm{e}}^x$$
93		vex	$$⊢x\in \mathrm{V}$$
94	93 83	breldm	$$⊢x{\exp }_{ℂ}^{\prime }{\mathrm{e}}^x\to x\in \mathrm{dom}{\exp }_{ℂ}^{\prime }$$
95	92 94	syl	$$⊢x\in ℂ\to x\in \mathrm{dom}{\exp }_{ℂ}^{\prime }$$
96	95	ssriv	$$⊢ℂ\subseteq \mathrm{dom}{\exp }_{ℂ}^{\prime }$$
97	2 96	eqssi	$$⊢\mathrm{dom}{\exp }_{ℂ}^{\prime }=ℂ$$
98	97	feq2i	$$⊢{\exp }_{ℂ}^{\prime }:\mathrm{dom}{\exp }_{ℂ}^{\prime }⟶ℂ\leftrightarrow {\exp }_{ℂ}^{\prime }:ℂ⟶ℂ$$
99	1 98	mpbi	$$⊢{\exp }_{ℂ}^{\prime }:ℂ⟶ℂ$$
100	99	a1i	$$⊢\top \to {\exp }_{ℂ}^{\prime }:ℂ⟶ℂ$$
101	100	feqmptd	$$⊢\top \to ℂ\mathrm{D}\exp =\left(x\in ℂ⟼{\exp }_{ℂ}^{\prime }\left(x\right)\right)$$
102		ffun	$$⊢{\exp }_{ℂ}^{\prime }:\mathrm{dom}{\exp }_{ℂ}^{\prime }⟶ℂ\to \mathrm{Fun}{\exp }_{ℂ}^{\prime }$$
103	1 102	ax-mp	$$⊢\mathrm{Fun}{\exp }_{ℂ}^{\prime }$$
104		funbrfv	$$⊢\mathrm{Fun}{\exp }_{ℂ}^{\prime }\to \left(x{\exp }_{ℂ}^{\prime }{\mathrm{e}}^x\to {\exp }_{ℂ}^{\prime }\left(x\right)={\mathrm{e}}^x\right)$$
105	103 92 104	mpsyl	$$⊢x\in ℂ\to {\exp }_{ℂ}^{\prime }\left(x\right)={\mathrm{e}}^x$$
106	105	mpteq2ia	$$⊢\left(x\in ℂ⟼{\exp }_{ℂ}^{\prime }\left(x\right)\right)=\left(x\in ℂ⟼{\mathrm{e}}^x\right)$$
107	101 106	eqtrdi	$$⊢\top \to ℂ\mathrm{D}\exp =\left(x\in ℂ⟼{\mathrm{e}}^x\right)$$
108	19	a1i	$$⊢\top \to \exp :ℂ⟶ℂ$$
109	108	feqmptd	$$⊢\top \to \exp =\left(x\in ℂ⟼{\mathrm{e}}^x\right)$$
110	107 109	eqtr4d	$$⊢\top \to ℂ\mathrm{D}\exp =\exp$$
111	110	mptru	$$⊢ℂ\mathrm{D}\exp =\exp$$