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 0cnd 
 |-  ( x e. CC -> 0 e. CC )
34 1cnd 
 |-  ( x e. CC -> 1 e. CC )
35 c0ex 
 |-  0 e. _V
36 35 snid 
 |-  0 e. { 0 }
37 opelxpi 
 |-  ( ( x e. CC /\ 0 e. { 0 } ) -> <. x , 0 >. e. ( CC X. { 0 } ) )
38 36 37 mpan2 
 |-  ( x e. CC -> <. x , 0 >. e. ( CC X. { 0 } ) )
39 dvconst 
 |-  ( ( exp ` x ) e. CC -> ( CC _D ( CC X. { ( exp ` x ) } ) ) = ( CC X. { 0 } ) )
40 24 39 syl 
 |-  ( x e. CC -> ( CC _D ( CC X. { ( exp ` x ) } ) ) = ( CC X. { 0 } ) )
41 38 40 eleqtrrd 
 |-  ( x e. CC -> <. x , 0 >. e. ( CC _D ( CC X. { ( exp ` x ) } ) ) )
42 df-br 
 |-  ( x ( CC _D ( CC X. { ( exp ` x ) } ) ) 0 <-> <. x , 0 >. e. ( CC _D ( CC X. { ( exp ` x ) } ) ) )
43 41 42 sylibr 
 |-  ( x e. CC -> x ( CC _D ( CC X. { ( exp ` x ) } ) ) 0 )
44 20 4 cofmpt 
 |-  ( x e. CC -> ( exp o. ( z e. CC |-> ( z - x ) ) ) = ( z e. CC |-> ( exp ` ( z - x ) ) ) )
45 44 oveq2d 
 |-  ( x e. CC -> ( CC _D ( exp o. ( z e. CC |-> ( z - x ) ) ) ) = ( CC _D ( z e. CC |-> ( exp ` ( z - x ) ) ) ) )
46 4 fmpttd 
 |-  ( x e. CC -> ( z e. CC |-> ( z - x ) ) : CC --> CC )
47 oveq1 
 |-  ( z = x -> ( z - x ) = ( x - x ) )
48 eqid 
 |-  ( z e. CC |-> ( z - x ) ) = ( z e. CC |-> ( z - x ) )
49 ovex 
 |-  ( x - x ) e. _V
50 47 48 49 fvmpt 
 |-  ( x e. CC -> ( ( z e. CC |-> ( z - x ) ) ` x ) = ( x - x ) )
51 subid 
 |-  ( x e. CC -> ( x - x ) = 0 )
52 50 51 eqtrd 
 |-  ( x e. CC -> ( ( z e. CC |-> ( z - x ) ) ` x ) = 0 )
53 dveflem 
 |-  0 ( CC _D exp ) 1
54 52 53 eqbrtrdi 
 |-  ( x e. CC -> ( ( z e. CC |-> ( z - x ) ) ` x ) ( CC _D exp ) 1 )
55 1ex 
 |-  1 e. _V
56 55 snid 
 |-  1 e. { 1 }
57 opelxpi 
 |-  ( ( x e. CC /\ 1 e. { 1 } ) -> <. x , 1 >. e. ( CC X. { 1 } ) )
58 56 57 mpan2 
 |-  ( x e. CC -> <. x , 1 >. e. ( CC X. { 1 } ) )
59 cnelprrecn 
 |-  CC e. { RR , CC }
60 59 a1i 
 |-  ( x e. CC -> CC e. { RR , CC } )
61 simpr 
 |-  ( ( x e. CC /\ z e. CC ) -> z e. CC )
62 1cnd 
 |-  ( ( x e. CC /\ z e. CC ) -> 1 e. CC )
63 60 dvmptid 
 |-  ( x e. CC -> ( CC _D ( z e. CC |-> z ) ) = ( z e. CC |-> 1 ) )
64 simpl 
 |-  ( ( x e. CC /\ z e. CC ) -> x e. CC )
65 0cnd 
 |-  ( ( x e. CC /\ z e. CC ) -> 0 e. CC )
66 id 
 |-  ( x e. CC -> x e. CC )
67 60 66 dvmptc 
 |-  ( x e. CC -> ( CC _D ( z e. CC |-> x ) ) = ( z e. CC |-> 0 ) )
68 60 61 62 63 64 65 67 dvmptsub 
 |-  ( x e. CC -> ( CC _D ( z e. CC |-> ( z - x ) ) ) = ( z e. CC |-> ( 1 - 0 ) ) )
69 1m0e1 
 |-  ( 1 - 0 ) = 1
70 69 mpteq2i 
 |-  ( z e. CC |-> ( 1 - 0 ) ) = ( z e. CC |-> 1 )
71 fconstmpt 
 |-  ( CC X. { 1 } ) = ( z e. CC |-> 1 )
72 70 71 eqtr4i 
 |-  ( z e. CC |-> ( 1 - 0 ) ) = ( CC X. { 1 } )
73 68 72 eqtrdi 
 |-  ( x e. CC -> ( CC _D ( z e. CC |-> ( z - x ) ) ) = ( CC X. { 1 } ) )
74 58 73 eleqtrrd 
 |-  ( x e. CC -> <. x , 1 >. e. ( CC _D ( z e. CC |-> ( z - x ) ) ) )
75 df-br 
 |-  ( x ( CC _D ( z e. CC |-> ( z - x ) ) ) 1 <-> <. x , 1 >. e. ( CC _D ( z e. CC |-> ( z - x ) ) ) )
76 74 75 sylibr 
 |-  ( x e. CC -> x ( CC _D ( z e. CC |-> ( z - x ) ) ) 1 )
77 eqid 
 |-  ( TopOpen ` CCfld ) = ( TopOpen ` CCfld )
78 20 29 46 29 29 29 34 34 54 76 77 dvcobr 
 |-  ( x e. CC -> x ( CC _D ( exp o. ( z e. CC |-> ( z - x ) ) ) ) ( 1 x. 1 ) )
79 1t1e1 
 |-  ( 1 x. 1 ) = 1
80 78 79 breqtrdi 
 |-  ( x e. CC -> x ( CC _D ( exp o. ( z e. CC |-> ( z - x ) ) ) ) 1 )
81 45 80 breqdi 
 |-  ( x e. CC -> x ( CC _D ( z e. CC |-> ( exp ` ( z - x ) ) ) ) 1 )
82 28 29 32 29 29 33 34 43 81 77 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 ) ) ) )
83 32 66 ffvelrnd 
 |-  ( x e. CC -> ( ( z e. CC |-> ( exp ` ( z - x ) ) ) ` x ) e. CC )
84 83 mul02d 
 |-  ( x e. CC -> ( 0 x. ( ( z e. CC |-> ( exp ` ( z - x ) ) ) ` x ) ) = 0 )
85 fvex 
 |-  ( exp ` x ) e. _V
86 85 fvconst2 
 |-  ( x e. CC -> ( ( CC X. { ( exp ` x ) } ) ` x ) = ( exp ` x ) )
87 86 oveq2d 
 |-  ( x e. CC -> ( 1 x. ( ( CC X. { ( exp ` x ) } ) ` x ) ) = ( 1 x. ( exp ` x ) ) )
88 24 mulid2d 
 |-  ( x e. CC -> ( 1 x. ( exp ` x ) ) = ( exp ` x ) )
89 87 88 eqtrd 
 |-  ( x e. CC -> ( 1 x. ( ( CC X. { ( exp ` x ) } ) ` x ) ) = ( exp ` x ) )
90 84 89 oveq12d 
 |-  ( x e. CC -> ( ( 0 x. ( ( z e. CC |-> ( exp ` ( z - x ) ) ) ` x ) ) + ( 1 x. ( ( CC X. { ( exp ` x ) } ) ` x ) ) ) = ( 0 + ( exp ` x ) ) )
91 24 addid2d 
 |-  ( x e. CC -> ( 0 + ( exp ` x ) ) = ( exp ` x ) )
92 90 91 eqtrd 
 |-  ( x e. CC -> ( ( 0 x. ( ( z e. CC |-> ( exp ` ( z - x ) ) ) ` x ) ) + ( 1 x. ( ( CC X. { ( exp ` x ) } ) ` x ) ) ) = ( exp ` x ) )
93 82 92 breqtrd 
 |-  ( x e. CC -> x ( CC _D ( ( CC X. { ( exp ` x ) } ) oF x. ( z e. CC |-> ( exp ` ( z - x ) ) ) ) ) ( exp ` x ) )
94 23 93 breqdi 
 |-  ( x e. CC -> x ( CC _D exp ) ( exp ` x ) )
95 vex 
 |-  x e. _V
96 95 85 breldm 
 |-  ( x ( CC _D exp ) ( exp ` x ) -> x e. dom ( CC _D exp ) )
97 94 96 syl 
 |-  ( x e. CC -> x e. dom ( CC _D exp ) )
98 97 ssriv 
 |-  CC C_ dom ( CC _D exp )
99 2 98 eqssi 
 |-  dom ( CC _D exp ) = CC
100 99 feq2i 
 |-  ( ( CC _D exp ) : dom ( CC _D exp ) --> CC <-> ( CC _D exp ) : CC --> CC )
101 1 100 mpbi 
 |-  ( CC _D exp ) : CC --> CC
102 101 a1i 
 |-  ( T. -> ( CC _D exp ) : CC --> CC )
103 102 feqmptd 
 |-  ( T. -> ( CC _D exp ) = ( x e. CC |-> ( ( CC _D exp ) ` x ) ) )
104 ffun 
 |-  ( ( CC _D exp ) : dom ( CC _D exp ) --> CC -> Fun ( CC _D exp ) )
105 1 104 ax-mp 
 |-  Fun ( CC _D exp )
106 funbrfv 
 |-  ( Fun ( CC _D exp ) -> ( x ( CC _D exp ) ( exp ` x ) -> ( ( CC _D exp ) ` x ) = ( exp ` x ) ) )
107 105 94 106 mpsyl 
 |-  ( x e. CC -> ( ( CC _D exp ) ` x ) = ( exp ` x ) )
108 107 mpteq2ia 
 |-  ( x e. CC |-> ( ( CC _D exp ) ` x ) ) = ( x e. CC |-> ( exp ` x ) )
109 103 108 eqtrdi 
 |-  ( T. -> ( CC _D exp ) = ( x e. CC |-> ( exp ` x ) ) )
110 19 a1i 
 |-  ( T. -> exp : CC --> CC )
111 110 feqmptd 
 |-  ( T. -> exp = ( x e. CC |-> ( exp ` x ) ) )
112 109 111 eqtr4d 
 |-  ( T. -> ( CC _D exp ) = exp )
113 112 mptru 
 |-  ( CC _D exp ) = exp