Metamath Proof Explorer

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 
|- ( CC _D exp ) = exp

Proof

Step Hyp Ref Expression
1 dvfcn 
 |-  ( CC _D exp ) : dom ( CC _D exp ) --> CC
2 dvbsss 
 |-  dom ( CC _D exp ) C_ CC
3 subcl 
 |-  ( ( z e. CC /\ x e. CC ) -> ( z - x ) e. CC )
4 3 ancoms 
 |-  ( ( x e. CC /\ z e. CC ) -> ( z - x ) e. CC )
5 efadd 
 |-  ( ( x e. CC /\ ( z - x ) e. CC ) -> ( exp ` ( x + ( z - x ) ) ) = ( ( exp ` x ) x. ( exp ` ( z - x ) ) ) )
6 4 5 syldan 
 |-  ( ( x e. CC /\ z e. CC ) -> ( exp ` ( x + ( z - x ) ) ) = ( ( exp ` x ) x. ( exp ` ( z - x ) ) ) )
7 pncan3 
 |-  ( ( x e. CC /\ z e. CC ) -> ( x + ( z - x ) ) = z )
8 7 fveq2d 
 |-  ( ( x e. CC /\ z e. CC ) -> ( exp ` ( x + ( z - x ) ) ) = ( exp ` z ) )
9 6 8 eqtr3d 
 |-  ( ( x e. CC /\ z e. CC ) -> ( ( exp ` x ) x. ( exp ` ( z - x ) ) ) = ( exp ` z ) )
10 9 mpteq2dva 
 |-  ( x e. CC -> ( z e. CC |-> ( ( exp ` x ) x. ( exp ` ( z - x ) ) ) ) = ( z e. CC |-> ( exp ` z ) ) )
11 cnex 
 |-  CC e. _V
12 11 a1i 
 |-  ( x e. CC -> CC e. _V )
13 fvexd 
 |-  ( ( x e. CC /\ z e. CC ) -> ( exp ` x ) e. _V )
14 fvexd 
 |-  ( ( x e. CC /\ z e. CC ) -> ( exp ` ( z - x ) ) e. _V )
15 fconstmpt 
 |-  ( CC X. { ( exp ` x ) } ) = ( z e. CC |-> ( exp ` x ) )
16 15 a1i 
 |-  ( x e. CC -> ( CC X. { ( exp ` x ) } ) = ( z e. CC |-> ( exp ` x ) ) )
17 eqidd 
 |-  ( x e. CC -> ( z e. CC |-> ( exp ` ( z - x ) ) ) = ( z e. CC |-> ( exp ` ( z - x ) ) ) )
18 12 13 14 16 17 offval2 
 |-  ( x e. CC -> ( ( CC X. { ( exp ` x ) } ) oF x. ( z e. CC |-> ( exp ` ( z - x ) ) ) ) = ( z e. CC |-> ( ( exp ` x ) x. ( exp ` ( z - x ) ) ) ) )
19 eff 
 |-  exp : CC --> CC
20 19 a1i 
 |-  ( x e. CC -> exp : CC --> CC )
21 20 feqmptd 
 |-  ( x e. CC -> exp = ( z e. CC |-> ( exp ` z ) ) )
22 10 18 21 3eqtr4d 
 |-  ( x e. CC -> ( ( CC X. { ( exp ` x ) } ) oF x. ( z e. CC |-> ( exp ` ( z - x ) ) ) ) = exp )
23 22 oveq2d 
 |-  ( x e. CC -> ( CC _D ( ( CC X. { ( exp ` x ) } ) oF x. ( z e. CC |-> ( exp ` ( z - x ) ) ) ) ) = ( CC _D exp ) )
24 efcl 
 |-  ( x e. CC -> ( exp ` x ) e. CC )
25 fconstg 
 |-  ( ( exp ` x ) e. CC -> ( CC X. { ( exp ` x ) } ) : CC --> { ( exp ` x ) } )
26 24 25 syl 
 |-  ( x e. CC -> ( CC X. { ( exp ` x ) } ) : CC --> { ( exp ` x ) } )
27 24 snssd 
 |-  ( x e. CC -> { ( exp ` x ) } C_ CC )
28 26 27 fssd 
 |-  ( x e. CC -> ( CC X. { ( exp ` x ) } ) : CC --> CC )
29 ssidd 
 |-  ( x e. CC -> CC C_ CC )
30 efcl 
 |-  ( ( z - x ) e. CC -> ( exp ` ( z - x ) ) e. CC )
31 4 30 syl 
 |-  ( ( x e. CC /\ z e. CC ) -> ( exp ` ( z - x ) ) e. CC )
32 31 fmpttd 
 |-  ( x e. CC -> ( z e. CC |-> ( exp ` ( z - x ) ) ) : CC --> CC )
33 c0ex 
 |-  0 e. _V
34 33 snid 
 |-  0 e. { 0 }
35 opelxpi 
 |-  ( ( x e. CC /\ 0 e. { 0 } ) -> <. x , 0 >. e. ( CC X. { 0 } ) )
36 34 35 mpan2 
 |-  ( x e. CC -> <. x , 0 >. e. ( CC X. { 0 } ) )
37 dvconst 
 |-  ( ( exp ` x ) e. CC -> ( CC _D ( CC X. { ( exp ` x ) } ) ) = ( CC X. { 0 } ) )
38 24 37 syl 
 |-  ( x e. CC -> ( CC _D ( CC X. { ( exp ` x ) } ) ) = ( CC X. { 0 } ) )
39 36 38 eleqtrrd 
 |-  ( x e. CC -> <. x , 0 >. e. ( CC _D ( CC X. { ( exp ` x ) } ) ) )
40 df-br 
 |-  ( x ( CC _D ( CC X. { ( exp ` x ) } ) ) 0 <-> <. x , 0 >. e. ( CC _D ( CC X. { ( exp ` x ) } ) ) )
41 39 40 sylibr 
 |-  ( x e. CC -> x ( CC _D ( CC X. { ( exp ` x ) } ) ) 0 )
42 20 4 cofmpt 
 |-  ( x e. CC -> ( exp o. ( z e. CC |-> ( z - x ) ) ) = ( z e. CC |-> ( exp ` ( z - x ) ) ) )
43 42 oveq2d 
 |-  ( x e. CC -> ( CC _D ( exp o. ( z e. CC |-> ( z - x ) ) ) ) = ( CC _D ( z e. CC |-> ( exp ` ( z - x ) ) ) ) )
44 4 fmpttd 
 |-  ( x e. CC -> ( z e. CC |-> ( z - x ) ) : CC --> CC )
45 oveq1 
 |-  ( z = x -> ( z - x ) = ( x - x ) )
46 eqid 
 |-  ( z e. CC |-> ( z - x ) ) = ( z e. CC |-> ( z - x ) )
47 ovex 
 |-  ( x - x ) e. _V
48 45 46 47 fvmpt 
 |-  ( x e. CC -> ( ( z e. CC |-> ( z - x ) ) ` x ) = ( x - x ) )
49 subid 
 |-  ( x e. CC -> ( x - x ) = 0 )
50 48 49 eqtrd 
 |-  ( x e. CC -> ( ( z e. CC |-> ( z - x ) ) ` x ) = 0 )
51 dveflem 
 |-  0 ( CC _D exp ) 1
52 50 51 eqbrtrdi 
 |-  ( x e. CC -> ( ( z e. CC |-> ( z - x ) ) ` x ) ( CC _D exp ) 1 )
53 1ex 
 |-  1 e. _V
54 53 snid 
 |-  1 e. { 1 }
55 opelxpi 
 |-  ( ( x e. CC /\ 1 e. { 1 } ) -> <. x , 1 >. e. ( CC X. { 1 } ) )
56 54 55 mpan2 
 |-  ( x e. CC -> <. x , 1 >. e. ( CC X. { 1 } ) )
57 cnelprrecn 
 |-  CC e. { RR , CC }
58 57 a1i 
 |-  ( x e. CC -> CC e. { RR , CC } )
59 simpr 
 |-  ( ( x e. CC /\ z e. CC ) -> z e. CC )
60 1cnd 
 |-  ( ( x e. CC /\ z e. CC ) -> 1 e. CC )
61 58 dvmptid 
 |-  ( x e. CC -> ( CC _D ( z e. CC |-> z ) ) = ( z e. CC |-> 1 ) )
62 simpl 
 |-  ( ( x e. CC /\ z e. CC ) -> x e. CC )
63 0cnd 
 |-  ( ( x e. CC /\ z e. CC ) -> 0 e. CC )
64 id 
 |-  ( x e. CC -> x e. CC )
65 58 64 dvmptc 
 |-  ( x e. CC -> ( CC _D ( z e. CC |-> x ) ) = ( z e. CC |-> 0 ) )
66 58 59 60 61 62 63 65 dvmptsub 
 |-  ( x e. CC -> ( CC _D ( z e. CC |-> ( z - x ) ) ) = ( z e. CC |-> ( 1 - 0 ) ) )
67 1m0e1 
 |-  ( 1 - 0 ) = 1
68 67 mpteq2i 
 |-  ( z e. CC |-> ( 1 - 0 ) ) = ( z e. CC |-> 1 )
69 fconstmpt 
 |-  ( CC X. { 1 } ) = ( z e. CC |-> 1 )
70 68 69 eqtr4i 
 |-  ( z e. CC |-> ( 1 - 0 ) ) = ( CC X. { 1 } )
71 66 70 eqtrdi 
 |-  ( x e. CC -> ( CC _D ( z e. CC |-> ( z - x ) ) ) = ( CC X. { 1 } ) )
72 56 71 eleqtrrd 
 |-  ( x e. CC -> <. x , 1 >. e. ( CC _D ( z e. CC |-> ( z - x ) ) ) )
73 df-br 
 |-  ( x ( CC _D ( z e. CC |-> ( z - x ) ) ) 1 <-> <. x , 1 >. e. ( CC _D ( z e. CC |-> ( z - x ) ) ) )
74 72 73 sylibr 
 |-  ( x e. CC -> x ( CC _D ( z e. CC |-> ( z - x ) ) ) 1 )
75 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
76 20 29 44 29 29 29 52 74 75 dvcobr 
 |-  ( x e. CC -> x ( CC _D ( exp o. ( z e. CC |-> ( z - x ) ) ) ) ( 1 x. 1 ) )
77 1t1e1 
 |-  ( 1 x. 1 ) = 1
78 76 77 breqtrdi 
 |-  ( x e. CC -> x ( CC _D ( exp o. ( z e. CC |-> ( z - x ) ) ) ) 1 )
79 43 78 breqdi 
 |-  ( x e. CC -> x ( CC _D ( z e. CC |-> ( exp ` ( z - x ) ) ) ) 1 )
80 28 29 32 29 29 41 79 75 dvmulbr 
 |-  ( x e. CC -> x ( CC _D ( ( CC X. { ( exp ` x ) } ) oF x. ( z e. CC |-> ( exp ` ( z - x ) ) ) ) ) ( ( 0 x. ( ( z e. CC |-> ( exp ` ( z - x ) ) ) ` x ) ) + ( 1 x. ( ( CC X. { ( exp ` x ) } ) ` x ) ) ) )
81 32 64 ffvelcdmd 
 |-  ( x e. CC -> ( ( z e. CC |-> ( exp ` ( z - x ) ) ) ` x ) e. CC )
82 81 mul02d 
 |-  ( x e. CC -> ( 0 x. ( ( z e. CC |-> ( exp ` ( z - x ) ) ) ` x ) ) = 0 )
83 fvex 
 |-  ( exp ` x ) e. _V
84 83 fvconst2 
 |-  ( x e. CC -> ( ( CC X. { ( exp ` x ) } ) ` x ) = ( exp ` x ) )
85 84 oveq2d 
 |-  ( x e. CC -> ( 1 x. ( ( CC X. { ( exp ` x ) } ) ` x ) ) = ( 1 x. ( exp ` x ) ) )
86 24 mullidd 
 |-  ( x e. CC -> ( 1 x. ( exp ` x ) ) = ( exp ` x ) )
87 85 86 eqtrd 
 |-  ( x e. CC -> ( 1 x. ( ( CC X. { ( exp ` x ) } ) ` x ) ) = ( exp ` x ) )
88 82 87 oveq12d 
 |-  ( x e. CC -> ( ( 0 x. ( ( z e. CC |-> ( exp ` ( z - x ) ) ) ` x ) ) + ( 1 x. ( ( CC X. { ( exp ` x ) } ) ` x ) ) ) = ( 0 + ( exp ` x ) ) )
89 24 addlidd 
 |-  ( x e. CC -> ( 0 + ( exp ` x ) ) = ( exp ` x ) )
90 88 89 eqtrd 
 |-  ( x e. CC -> ( ( 0 x. ( ( z e. CC |-> ( exp ` ( z - x ) ) ) ` x ) ) + ( 1 x. ( ( CC X. { ( exp ` x ) } ) ` x ) ) ) = ( exp ` x ) )
91 80 90 breqtrd 
 |-  ( x e. CC -> x ( CC _D ( ( CC X. { ( exp ` x ) } ) oF x. ( z e. CC |-> ( exp ` ( z - x ) ) ) ) ) ( exp ` x ) )
92 23 91 breqdi 
 |-  ( x e. CC -> x ( CC _D exp ) ( exp ` x ) )
93 vex 
 |-  x e. _V
94 93 83 breldm 
 |-  ( x ( CC _D exp ) ( exp ` x ) -> x e. dom ( CC _D exp ) )
95 92 94 syl 
 |-  ( x e. CC -> x e. dom ( CC _D exp ) )
96 95 ssriv 
 |-  CC C_ dom ( CC _D exp )
97 2 96 eqssi 
 |-  dom ( CC _D exp ) = CC
98 97 feq2i 
 |-  ( ( CC _D exp ) : dom ( CC _D exp ) --> CC <-> ( CC _D exp ) : CC --> CC )
99 1 98 mpbi 
 |-  ( CC _D exp ) : CC --> CC
100 99 a1i 
 |-  ( T. -> ( CC _D exp ) : CC --> CC )
101 100 feqmptd 
 |-  ( T. -> ( CC _D exp ) = ( x e. CC |-> ( ( CC _D exp ) ` x ) ) )
102 ffun 
 |-  ( ( CC _D exp ) : dom ( CC _D exp ) --> CC -> Fun ( CC _D exp ) )
103 1 102 ax-mp 
 |-  Fun ( CC _D exp )
104 funbrfv 
 |-  ( Fun ( CC _D exp ) -> ( x ( CC _D exp ) ( exp ` x ) -> ( ( CC _D exp ) ` x ) = ( exp ` x ) ) )
105 103 92 104 mpsyl 
 |-  ( x e. CC -> ( ( CC _D exp ) ` x ) = ( exp ` x ) )
106 105 mpteq2ia 
 |-  ( x e. CC |-> ( ( CC _D exp ) ` x ) ) = ( x e. CC |-> ( exp ` x ) )
107 101 106 eqtrdi 
 |-  ( T. -> ( CC _D exp ) = ( x e. CC |-> ( exp ` x ) ) )
108 19 a1i 
 |-  ( T. -> exp : CC --> CC )
109 108 feqmptd 
 |-  ( T. -> exp = ( x e. CC |-> ( exp ` x ) ) )
110 107 109 eqtr4d 
 |-  ( T. -> ( CC _D exp ) = exp )
111 110 mptru 
 |-  ( CC _D exp ) = exp