Theorem dvsef

Description: Derivative of the exponential function on the real or complex numbers. (Contributed by Steve Rodriguez, 12-Nov-2015)

	Ref	Expression
Assertion	dvsef	$$⊢S\in \left\{ℝ,ℂ\right\}\to S\mathrm{D}\left({\exp \upharpoonright }_S\right)={\exp \upharpoonright }_S$$

Proof

Step	Hyp	Ref	Expression
1		eff	$$⊢\exp :ℂ⟶ℂ$$
2	1	jctr	$$⊢S\in \left\{ℝ,ℂ\right\}\to \left(S\in \left\{ℝ,ℂ\right\}\wedge \exp :ℂ⟶ℂ\right)$$
3		recnprss	$$⊢S\in \left\{ℝ,ℂ\right\}\to S\subseteq ℂ$$
4		dvef	$$⊢ℂ\mathrm{D}\exp =\exp$$
5	4	dmeqi	$$⊢\mathrm{dom}{\exp }_{ℂ}^{\prime }=\mathrm{dom}\exp$$
6	1	fdmi	$$⊢\mathrm{dom}\exp =ℂ$$
7	5 6	eqtri	$$⊢\mathrm{dom}{\exp }_{ℂ}^{\prime }=ℂ$$
8	3 7	sseqtrrdi	$$⊢S\in \left\{ℝ,ℂ\right\}\to S\subseteq \mathrm{dom}{\exp }_{ℂ}^{\prime }$$
9		ssid	$$⊢ℂ\subseteq ℂ$$
10	8 9	jctil	$$⊢S\in \left\{ℝ,ℂ\right\}\to \left(ℂ\subseteq ℂ\wedge S\subseteq \mathrm{dom}{\exp }_{ℂ}^{\prime }\right)$$
11		dvres3	$$⊢\left(\left(S\in \left\{ℝ,ℂ\right\}\wedge \exp :ℂ⟶ℂ\right)\wedge \left(ℂ\subseteq ℂ\wedge S\subseteq \mathrm{dom}{\exp }_{ℂ}^{\prime }\right)\right)\to S\mathrm{D}\left({\exp \upharpoonright }_S\right)={{\exp }_{ℂ}^{\prime }\upharpoonright }_S$$
12	2 10 11	syl2anc	$$⊢S\in \left\{ℝ,ℂ\right\}\to S\mathrm{D}\left({\exp \upharpoonright }_S\right)={{\exp }_{ℂ}^{\prime }\upharpoonright }_S$$
13	4	reseq1i	$$⊢{{\exp }_{ℂ}^{\prime }\upharpoonright }_S={\exp \upharpoonright }_S$$
14	12 13	eqtrdi	$$⊢S\in \left\{ℝ,ℂ\right\}\to S\mathrm{D}\left({\exp \upharpoonright }_S\right)={\exp \upharpoonright }_S$$