Metamath Proof Explorer

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 e. { RR , CC } -> ( S _D ( exp |` S ) ) = ( exp |` S ) )

Proof

Step Hyp Ref Expression
1 eff 
 |-  exp : CC --> CC
2 1 jctr 
 |-  ( S e. { RR , CC } -> ( S e. { RR , CC } /\ exp : CC --> CC ) )
3 recnprss 
 |-  ( S e. { RR , CC } -> S C_ CC )
4 dvef 
 |-  ( CC _D exp ) = exp
5 4 dmeqi 
 |-  dom ( CC _D exp ) = dom exp
6 1 fdmi 
 |-  dom exp = CC
7 5 6 eqtri 
 |-  dom ( CC _D exp ) = CC
8 3 7 sseqtrrdi 
 |-  ( S e. { RR , CC } -> S C_ dom ( CC _D exp ) )
9 ssid 
 |-  CC C_ CC
10 8 9 jctil 
 |-  ( S e. { RR , CC } -> ( CC C_ CC /\ S C_ dom ( CC _D exp ) ) )
11 dvres3 
 |-  ( ( ( S e. { RR , CC } /\ exp : CC --> CC ) /\ ( CC C_ CC /\ S C_ dom ( CC _D exp ) ) ) -> ( S _D ( exp |` S ) ) = ( ( CC _D exp ) |` S ) )
12 2 10 11 syl2anc 
 |-  ( S e. { RR , CC } -> ( S _D ( exp |` S ) ) = ( ( CC _D exp ) |` S ) )
13 4 reseq1i 
 |-  ( ( CC _D exp ) |` S ) = ( exp |` S )
14 12 13 eqtrdi 
 |-  ( S e. { RR , CC } -> ( S _D ( exp |` S ) ) = ( exp |` S ) )