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 D exp = exp

Proof

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