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