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∈ℂ∖0xNdℂx=x∈ℂ∖0⟼N⁢xN−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→xN∈ℂ
5 4 ancoms ⊢N∈ℕ0∧x∈ℂ→xN∈ℂ
6 c0ex ⊢0∈V
7 ovex ⊢N⁢xN−1∈V
8 6 7 ifex ⊢ifN=00N⁢xN−1∈V
9 8 a1i ⊢N∈ℕ0∧x∈ℂ→ifN=00N⁢xN−1∈V
10 dvexp2 ⊢N∈ℕ0→dx∈ℂxNdℂx=x∈ℂ⟼ifN=00N⁢xN−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∈ℂ∖0xNdℂx=x∈ℂ∖0⟼ifN=00N⁢xN−1
24 ifid ⊢ifN=0N⁢xN−1N⁢xN−1=N⁢xN−1
25 id ⊢N=0→N=0
26 oveq1 ⊢N=0→N−1=0−1
27 26 oveq2d ⊢N=0→xN−1=x0−1
28 25 27 oveq12d ⊢N=0→N⁢xN−1=0⋅x0−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∈ℤ→x0−1∈ℂ
34 32 33 mp3an3 ⊢x∈ℂ∧x≠0→x0−1∈ℂ
35 29 34 sylbi ⊢x∈ℂ∖0→x0−1∈ℂ
36 35 adantl ⊢N∈ℕ0∧x∈ℂ∖0→x0−1∈ℂ
37 36 mul02d ⊢N∈ℕ0∧x∈ℂ∖0→0⋅x0−1=0
38 28 37 sylan9eqr ⊢N∈ℕ0∧x∈ℂ∖0∧N=0→N⁢xN−1=0
39 38 ifeq1da ⊢N∈ℕ0∧x∈ℂ∖0→ifN=0N⁢xN−1N⁢xN−1=ifN=00N⁢xN−1
40 24 39 eqtr3id ⊢N∈ℕ0∧x∈ℂ∖0→N⁢xN−1=ifN=00N⁢xN−1
41 40 mpteq2dva ⊢N∈ℕ0→x∈ℂ∖0⟼N⁢xN−1=x∈ℂ∖0⟼ifN=00N⁢xN−1
42 23 41 eqtr4d ⊢N∈ℕ0→dx∈ℂ∖0xNdℂx=x∈ℂ∖0⟼N⁢xN−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→xN=1x−N
50 44 46 48 49 syl3anc ⊢N∈ℝ∧−N∈ℕ∧x∈ℂ∖0→xN=1x−N
51 50 mpteq2dva ⊢N∈ℝ∧−N∈ℕ→x∈ℂ∖0⟼xN=x∈ℂ∖0⟼1x−N
52 51 oveq2d ⊢N∈ℝ∧−N∈ℕ→dx∈ℂ∖0xNdℂx=dx∈ℂ∖01x−Ndℂ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→1y∈ℂ
68 66 67 syl ⊢N∈ℝ∧−N∈ℕ∧y∈ℂ∖0→1y∈ℂ
69 negex ⊢−1y2∈V
70 69 a1i ⊢N∈ℝ∧−N∈ℕ∧y∈ℂ∖0→−1y2∈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−Ndℂx=x∈ℂ⟼- N⁢x-N-1
76 75 adantl ⊢N∈ℝ∧−N∈ℕ→dx∈ℂx−Ndℂ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∈ℂ∖0x−Ndℂx=x∈ℂ∖0⟼- N⁢x-N-1
80 ax-1cn ⊢1∈ℂ
81 dvrec ⊢1∈ℂ→dy∈ℂ∖01ydℂy=y∈ℂ∖0⟼−1y2
82 80 81 mp1i ⊢N∈ℝ∧−N∈ℕ→dy∈ℂ∖01ydℂy=y∈ℂ∖0⟼−1y2
83 oveq2 ⊢y=x−N→1y=1x−N
84 oveq1 ⊢y=x−N→y2=x−N2
85 84 oveq2d ⊢y=x−N→1y2=1x−N2
86 85 negeqd ⊢y=x−N→−1y2=−1x−N2
87 53 53 61 63 68 70 79 82 83 86 dvmptco ⊢N∈ℝ∧−N∈ℕ→dx∈ℂ∖01x−Ndℂx=x∈ℂ∖0⟼−1x−N2⁢- 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−N2
91 44 55 57 89 90 syl22anc ⊢N∈ℝ∧−N∈ℕ∧x∈ℂ∖0→x- N⋅2=x−N2
92 91 eqcomd ⊢N∈ℝ∧−N∈ℕ∧x∈ℂ∖0→x−N2=x- N⋅2
93 92 oveq2d ⊢N∈ℝ∧−N∈ℕ∧x∈ℂ∖0→1x−N2=1x- N⋅2
94 93 negeqd ⊢N∈ℝ∧−N∈ℕ∧x∈ℂ∖0→−1x−N2=−1x- 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→−1x−N2⁢- N⁢x-N-1=−1x- 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→1x- N⋅2∈ℂ
105 46 97 mulcld ⊢N∈ℝ∧−N∈ℕ∧x∈ℂ∖0→N⁢x-N-1∈ℂ
106 104 105 mul2negd ⊢N∈ℝ∧−N∈ℕ∧x∈ℂ∖0→−1x- N⋅2⁢−N⁢x-N-1=1x- N⋅2⁢N⁢x-N-1
107 104 46 97 mul12d ⊢N∈ℝ∧−N∈ℕ∧x∈ℂ∖0→1x- N⋅2⁢N⁢x-N-1=N⁢1x- N⋅2⁢x-N-1
108 44 55 101 96 expsubd ⊢N∈ℝ∧−N∈ℕ∧x∈ℂ∖0→x- N-1-- N⋅2=x-N-1x- 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=xN−1
123 97 102 103 divrec2d ⊢N∈ℝ∧−N∈ℕ∧x∈ℂ∖0→x-N-1x- N⋅2=1x- N⋅2⁢x-N-1
124 108 122 123 3eqtr3rd ⊢N∈ℝ∧−N∈ℕ∧x∈ℂ∖0→1x- N⋅2⁢x-N-1=xN−1
125 124 oveq2d ⊢N∈ℝ∧−N∈ℕ∧x∈ℂ∖0→N⁢1x- N⋅2⁢x-N-1=N⁢xN−1
126 107 125 eqtrd ⊢N∈ℝ∧−N∈ℕ∧x∈ℂ∖0→1x- N⋅2⁢N⁢x-N-1=N⁢xN−1
127 99 106 126 3eqtrd ⊢N∈ℝ∧−N∈ℕ∧x∈ℂ∖0→−1x−N2⁢- N⁢x-N-1=N⁢xN−1
128 127 mpteq2dva ⊢N∈ℝ∧−N∈ℕ→x∈ℂ∖0⟼−1x−N2⁢- N⁢x-N-1=x∈ℂ∖0⟼N⁢xN−1
129 52 87 128 3eqtrd ⊢N∈ℝ∧−N∈ℕ→dx∈ℂ∖0xNdℂx=x∈ℂ∖0⟼N⁢xN−1
130 42 129 jaoi ⊢N∈ℕ0∨N∈ℝ∧−N∈ℕ→dx∈ℂ∖0xNdℂx=x∈ℂ∖0⟼N⁢xN−1
131 1 130 sylbi ⊢N∈ℤ→dx∈ℂ∖0xNdℂx=x∈ℂ∖0⟼N⁢xN−1