Metamath Proof Explorer


Theorem dvexp3

Description: Derivative of an exponential of integer exponent. (Contributed by Mario Carneiro, 26-Feb-2015)

Ref Expression
Assertion dvexp3 N dx 0 x N d x = x 0 N x N 1

Proof

Step Hyp Ref Expression
1 elznn0nn N N 0 N N
2 cnelprrecn
3 2 a1i N 0
4 expcl x N 0 x N
5 4 ancoms N 0 x x N
6 c0ex 0 V
7 ovex N x N 1 V
8 6 7 ifex if N = 0 0 N x N 1 V
9 8 a1i N 0 x if N = 0 0 N x N 1 V
10 dvexp2 N 0 dx x N d x = x if N = 0 0 N x N 1
11 difssd N 0 0
12 eqid TopOpen fld = TopOpen fld
13 12 cnfldtopon TopOpen fld TopOn
14 13 toponrestid TopOpen fld = TopOpen fld 𝑡
15 cnn0opn 0 TopOpen fld
16 15 a1i N 0 0 TopOpen fld
17 3 5 9 10 11 14 12 16 dvmptres N 0 dx 0 x N d x = x 0 if N = 0 0 N x N 1
18 ifid if N = 0 N x N 1 N x N 1 = N x N 1
19 id N = 0 N = 0
20 oveq1 N = 0 N 1 = 0 1
21 20 oveq2d N = 0 x N 1 = x 0 1
22 19 21 oveq12d N = 0 N x N 1 = 0 x 0 1
23 eldifsn x 0 x x 0
24 0z 0
25 peano2zm 0 0 1
26 24 25 ax-mp 0 1
27 expclz x x 0 0 1 x 0 1
28 26 27 mp3an3 x x 0 x 0 1
29 23 28 sylbi x 0 x 0 1
30 29 adantl N 0 x 0 x 0 1
31 30 mul02d N 0 x 0 0 x 0 1 = 0
32 22 31 sylan9eqr N 0 x 0 N = 0 N x N 1 = 0
33 32 ifeq1da N 0 x 0 if N = 0 N x N 1 N x N 1 = if N = 0 0 N x N 1
34 18 33 eqtr3id N 0 x 0 N x N 1 = if N = 0 0 N x N 1
35 34 mpteq2dva N 0 x 0 N x N 1 = x 0 if N = 0 0 N x N 1
36 17 35 eqtr4d N 0 dx 0 x N d x = x 0 N x N 1
37 eldifi x 0 x
38 37 adantl N N x 0 x
39 simpll N N x 0 N
40 39 recnd N N x 0 N
41 nnnn0 N N 0
42 41 ad2antlr N N x 0 N 0
43 expneg2 x N N 0 x N = 1 x N
44 38 40 42 43 syl3anc N N x 0 x N = 1 x N
45 44 mpteq2dva N N x 0 x N = x 0 1 x N
46 45 oveq2d N N dx 0 x N d x = dx 0 1 x N d x
47 2 a1i N N
48 eldifsni x 0 x 0
49 48 adantl N N x 0 x 0
50 nnz N N
51 50 ad2antlr N N x 0 N
52 38 49 51 expclzd N N x 0 x N
53 38 49 51 expne0d N N x 0 x N 0
54 eldifsn x N 0 x N x N 0
55 52 53 54 sylanbrc N N x 0 x N 0
56 ovex -N x - N - 1 V
57 56 a1i N N x 0 -N x - N - 1 V
58 simpr N N y 0 y 0
59 eldifsn y 0 y y 0
60 58 59 sylib N N y 0 y y 0
61 reccl y y 0 1 y
62 60 61 syl N N y 0 1 y
63 negex 1 y 2 V
64 63 a1i N N y 0 1 y 2 V
65 simpr N N x x
66 41 ad2antlr N N x N 0
67 65 66 expcld N N x x N
68 56 a1i N N x -N x - N - 1 V
69 dvexp N dx x N d x = x -N x - N - 1
70 69 adantl N N dx x N d x = x -N x - N - 1
71 difssd N N 0
72 15 a1i N N 0 TopOpen fld
73 47 67 68 70 71 14 12 72 dvmptres N N dx 0 x N d x = x 0 -N x - N - 1
74 ax-1cn 1
75 dvrec 1 dy 0 1 y d y = y 0 1 y 2
76 74 75 mp1i N N dy 0 1 y d y = y 0 1 y 2
77 oveq2 y = x N 1 y = 1 x N
78 oveq1 y = x N y 2 = x N 2
79 78 oveq2d y = x N 1 y 2 = 1 x N 2
80 79 negeqd y = x N 1 y 2 = 1 x N 2
81 47 47 55 57 62 64 73 76 77 80 dvmptco N N dx 0 1 x N d x = x 0 1 x N 2 -N x - N - 1
82 2z 2
83 82 a1i N N x 0 2
84 expmulz x x 0 N 2 x -N 2 = x N 2
85 38 49 51 83 84 syl22anc N N x 0 x -N 2 = x N 2
86 85 eqcomd N N x 0 x N 2 = x -N 2
87 86 oveq2d N N x 0 1 x N 2 = 1 x -N 2
88 87 negeqd N N x 0 1 x N 2 = 1 x -N 2
89 peano2zm N - N - 1
90 51 89 syl N N x 0 - N - 1
91 38 49 90 expclzd N N x 0 x - N - 1
92 40 91 mulneg1d N N x 0 -N x - N - 1 = N x - N - 1
93 88 92 oveq12d N N x 0 1 x N 2 -N x - N - 1 = 1 x -N 2 N x - N - 1
94 zmulcl N 2 -N 2
95 51 82 94 sylancl N N x 0 -N 2
96 38 49 95 expclzd N N x 0 x -N 2
97 38 49 95 expne0d N N x 0 x -N 2 0
98 96 97 reccld N N x 0 1 x -N 2
99 40 91 mulcld N N x 0 N x - N - 1
100 98 99 mul2negd N N x 0 1 x -N 2 N x - N - 1 = 1 x -N 2 N x - N - 1
101 98 40 91 mul12d N N x 0 1 x -N 2 N x - N - 1 = N 1 x -N 2 x - N - 1
102 38 49 95 90 expsubd N N x 0 x -N - 1 - -N 2 = x - N - 1 x -N 2
103 nncn N N
104 103 ad2antlr N N x 0 N
105 74 a1i N N x 0 1
106 95 zcnd N N x 0 -N 2
107 104 105 106 sub32d N N x 0 -N - 1 - -N 2 = -N - -N 2 - 1
108 104 times2d N N x 0 -N 2 = - N + -N
109 104 40 negsubd N N x 0 - N + -N = - N - N
110 108 109 eqtrd N N x 0 -N 2 = - N - N
111 110 oveq2d N N x 0 - N - -N 2 = - N - - N - N
112 104 40 nncand N N x 0 - N - - N - N = N
113 111 112 eqtrd N N x 0 - N - -N 2 = N
114 113 oveq1d N N x 0 -N - -N 2 - 1 = N 1
115 107 114 eqtrd N N x 0 -N - 1 - -N 2 = N 1
116 115 oveq2d N N x 0 x -N - 1 - -N 2 = x N 1
117 91 96 97 divrec2d N N x 0 x - N - 1 x -N 2 = 1 x -N 2 x - N - 1
118 102 116 117 3eqtr3rd N N x 0 1 x -N 2 x - N - 1 = x N 1
119 118 oveq2d N N x 0 N 1 x -N 2 x - N - 1 = N x N 1
120 101 119 eqtrd N N x 0 1 x -N 2 N x - N - 1 = N x N 1
121 93 100 120 3eqtrd N N x 0 1 x N 2 -N x - N - 1 = N x N 1
122 121 mpteq2dva N N x 0 1 x N 2 -N x - N - 1 = x 0 N x N 1
123 46 81 122 3eqtrd N N dx 0 x N d x = x 0 N x N 1
124 36 123 jaoi N 0 N N dx 0 x N d x = x 0 N x N 1
125 1 124 sylbi N dx 0 x N d x = x 0 N x N 1