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	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D ( exp ↾ 𝑆 ) ) = ( exp ↾ 𝑆 ) )

Proof

Step	Hyp	Ref	Expression
1		eff	⊢ exp : ℂ ⟶ ℂ
2	1	jctr	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 ∈ { ℝ , ℂ } ∧ exp : ℂ ⟶ ℂ ) )
3		recnprss	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ ℂ )
4		dvef	⊢ ( ℂ D exp ) = exp
5	4	dmeqi	⊢ dom ( ℂ D exp ) = dom exp
6	1	fdmi	⊢ dom exp = ℂ
7	5 6	eqtri	⊢ dom ( ℂ D exp ) = ℂ
8	3 7	sseqtrrdi	⊢ ( 𝑆 ∈ { ℝ , ℂ } → 𝑆 ⊆ dom ( ℂ D exp ) )
9		ssid	⊢ ℂ ⊆ ℂ
10	8 9	jctil	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( ℂ ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D exp ) ) )
11		dvres3	⊢ ( ( ( 𝑆 ∈ { ℝ , ℂ } ∧ exp : ℂ ⟶ ℂ ) ∧ ( ℂ ⊆ ℂ ∧ 𝑆 ⊆ dom ( ℂ D exp ) ) ) → ( 𝑆 D ( exp ↾ 𝑆 ) ) = ( ( ℂ D exp ) ↾ 𝑆 ) )
12	2 10 11	syl2anc	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D ( exp ↾ 𝑆 ) ) = ( ( ℂ D exp ) ↾ 𝑆 ) )
13	4	reseq1i	⊢ ( ( ℂ D exp ) ↾ 𝑆 ) = ( exp ↾ 𝑆 )
14	12 13	eqtrdi	⊢ ( 𝑆 ∈ { ℝ , ℂ } → ( 𝑆 D ( exp ↾ 𝑆 ) ) = ( exp ↾ 𝑆 ) )