Metamath Proof Explorer


Theorem dvexp3

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

Ref Expression
Assertion dvexp3 ( 𝑁 ∈ ℤ → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥𝑁 ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 elznn0nn ( 𝑁 ∈ ℤ ↔ ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) )
2 cnelprrecn ℂ ∈ { ℝ , ℂ }
3 2 a1i ( 𝑁 ∈ ℕ0 → ℂ ∈ { ℝ , ℂ } )
4 expcl ( ( 𝑥 ∈ ℂ ∧ 𝑁 ∈ ℕ0 ) → ( 𝑥𝑁 ) ∈ ℂ )
5 4 ancoms ( ( 𝑁 ∈ ℕ0𝑥 ∈ ℂ ) → ( 𝑥𝑁 ) ∈ ℂ )
6 c0ex 0 ∈ V
7 ovex ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ∈ V
8 6 7 ifex if ( 𝑁 = 0 , 0 , ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) ∈ V
9 8 a1i ( ( 𝑁 ∈ ℕ0𝑥 ∈ ℂ ) → if ( 𝑁 = 0 , 0 , ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) ∈ V )
10 dvexp2 ( 𝑁 ∈ ℕ0 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥𝑁 ) ) ) = ( 𝑥 ∈ ℂ ↦ if ( 𝑁 = 0 , 0 , ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) ) )
11 difssd ( 𝑁 ∈ ℕ0 → ( ℂ ∖ { 0 } ) ⊆ ℂ )
12 eqid ( TopOpen ‘ ℂfld ) = ( TopOpen ‘ ℂfld )
13 12 cnfldtopon ( TopOpen ‘ ℂfld ) ∈ ( TopOn ‘ ℂ )
14 13 toponrestid ( TopOpen ‘ ℂfld ) = ( ( TopOpen ‘ ℂfld ) ↾t ℂ )
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 ( 𝑁 ∈ ℕ0 → ( ℂ ∖ { 0 } ) ∈ ( TopOpen ‘ ℂfld ) )
23 3 5 9 10 11 14 12 22 dvmptres ( 𝑁 ∈ ℕ0 → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥𝑁 ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ if ( 𝑁 = 0 , 0 , ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) ) )
24 ifid if ( 𝑁 = 0 , ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) , ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) = ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) )
25 id ( 𝑁 = 0 → 𝑁 = 0 )
26 oveq1 ( 𝑁 = 0 → ( 𝑁 − 1 ) = ( 0 − 1 ) )
27 26 oveq2d ( 𝑁 = 0 → ( 𝑥 ↑ ( 𝑁 − 1 ) ) = ( 𝑥 ↑ ( 0 − 1 ) ) )
28 25 27 oveq12d ( 𝑁 = 0 → ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) = ( 0 · ( 𝑥 ↑ ( 0 − 1 ) ) ) )
29 eldifsn ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
30 0z 0 ∈ ℤ
31 peano2zm ( 0 ∈ ℤ → ( 0 − 1 ) ∈ ℤ )
32 30 31 ax-mp ( 0 − 1 ) ∈ ℤ
33 expclz ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ∧ ( 0 − 1 ) ∈ ℤ ) → ( 𝑥 ↑ ( 0 − 1 ) ) ∈ ℂ )
34 32 33 mp3an3 ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) → ( 𝑥 ↑ ( 0 − 1 ) ) ∈ ℂ )
35 29 34 sylbi ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → ( 𝑥 ↑ ( 0 − 1 ) ) ∈ ℂ )
36 35 adantl ( ( 𝑁 ∈ ℕ0𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ↑ ( 0 − 1 ) ) ∈ ℂ )
37 36 mul02d ( ( 𝑁 ∈ ℕ0𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 0 · ( 𝑥 ↑ ( 0 − 1 ) ) ) = 0 )
38 28 37 sylan9eqr ( ( ( 𝑁 ∈ ℕ0𝑥 ∈ ( ℂ ∖ { 0 } ) ) ∧ 𝑁 = 0 ) → ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) = 0 )
39 38 ifeq1da ( ( 𝑁 ∈ ℕ0𝑥 ∈ ( ℂ ∖ { 0 } ) ) → if ( 𝑁 = 0 , ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) , ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) = if ( 𝑁 = 0 , 0 , ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) )
40 24 39 eqtr3id ( ( 𝑁 ∈ ℕ0𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) = if ( 𝑁 = 0 , 0 , ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) )
41 40 mpteq2dva ( 𝑁 ∈ ℕ0 → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ if ( 𝑁 = 0 , 0 , ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) ) )
42 23 41 eqtr4d ( 𝑁 ∈ ℕ0 → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥𝑁 ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) )
43 eldifi ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → 𝑥 ∈ ℂ )
44 43 adantl ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → 𝑥 ∈ ℂ )
45 simpll ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → 𝑁 ∈ ℝ )
46 45 recnd ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → 𝑁 ∈ ℂ )
47 nnnn0 ( - 𝑁 ∈ ℕ → - 𝑁 ∈ ℕ0 )
48 47 ad2antlr ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → - 𝑁 ∈ ℕ0 )
49 expneg2 ( ( 𝑥 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ - 𝑁 ∈ ℕ0 ) → ( 𝑥𝑁 ) = ( 1 / ( 𝑥 ↑ - 𝑁 ) ) )
50 44 46 48 49 syl3anc ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥𝑁 ) = ( 1 / ( 𝑥 ↑ - 𝑁 ) ) )
51 50 mpteq2dva ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥𝑁 ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / ( 𝑥 ↑ - 𝑁 ) ) ) )
52 51 oveq2d ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥𝑁 ) ) ) = ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / ( 𝑥 ↑ - 𝑁 ) ) ) ) )
53 2 a1i ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ℂ ∈ { ℝ , ℂ } )
54 eldifsni ( 𝑥 ∈ ( ℂ ∖ { 0 } ) → 𝑥 ≠ 0 )
55 54 adantl ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → 𝑥 ≠ 0 )
56 nnz ( - 𝑁 ∈ ℕ → - 𝑁 ∈ ℤ )
57 56 ad2antlr ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → - 𝑁 ∈ ℤ )
58 44 55 57 expclzd ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ↑ - 𝑁 ) ∈ ℂ )
59 44 55 57 expne0d ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ↑ - 𝑁 ) ≠ 0 )
60 eldifsn ( ( 𝑥 ↑ - 𝑁 ) ∈ ( ℂ ∖ { 0 } ) ↔ ( ( 𝑥 ↑ - 𝑁 ) ∈ ℂ ∧ ( 𝑥 ↑ - 𝑁 ) ≠ 0 ) )
61 58 59 60 sylanbrc ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ↑ - 𝑁 ) ∈ ( ℂ ∖ { 0 } ) )
62 ovex ( - 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ∈ V
63 62 a1i ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( - 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ∈ V )
64 simpr ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → 𝑦 ∈ ( ℂ ∖ { 0 } ) )
65 eldifsn ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↔ ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
66 64 65 sylib ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) )
67 reccl ( ( 𝑦 ∈ ℂ ∧ 𝑦 ≠ 0 ) → ( 1 / 𝑦 ) ∈ ℂ )
68 66 67 syl ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → ( 1 / 𝑦 ) ∈ ℂ )
69 negex - ( 1 / ( 𝑦 ↑ 2 ) ) ∈ V
70 69 a1i ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑦 ∈ ( ℂ ∖ { 0 } ) ) → - ( 1 / ( 𝑦 ↑ 2 ) ) ∈ V )
71 simpr ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℂ ) → 𝑥 ∈ ℂ )
72 47 ad2antlr ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℂ ) → - 𝑁 ∈ ℕ0 )
73 71 72 expcld ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℂ ) → ( 𝑥 ↑ - 𝑁 ) ∈ ℂ )
74 62 a1i ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ℂ ) → ( - 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ∈ V )
75 dvexp ( - 𝑁 ∈ ℕ → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ - 𝑁 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( - 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ) )
76 75 adantl ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( 𝑥 ↑ - 𝑁 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( - 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ) )
77 difssd ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( ℂ ∖ { 0 } ) ⊆ ℂ )
78 21 a1i ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( ℂ ∖ { 0 } ) ∈ ( TopOpen ‘ ℂfld ) )
79 53 73 74 76 77 14 12 78 dvmptres ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥 ↑ - 𝑁 ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( - 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ) )
80 ax-1cn 1 ∈ ℂ
81 dvrec ( 1 ∈ ℂ → ( ℂ D ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ - ( 1 / ( 𝑦 ↑ 2 ) ) ) )
82 80 81 mp1i ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( ℂ D ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / 𝑦 ) ) ) = ( 𝑦 ∈ ( ℂ ∖ { 0 } ) ↦ - ( 1 / ( 𝑦 ↑ 2 ) ) ) )
83 oveq2 ( 𝑦 = ( 𝑥 ↑ - 𝑁 ) → ( 1 / 𝑦 ) = ( 1 / ( 𝑥 ↑ - 𝑁 ) ) )
84 oveq1 ( 𝑦 = ( 𝑥 ↑ - 𝑁 ) → ( 𝑦 ↑ 2 ) = ( ( 𝑥 ↑ - 𝑁 ) ↑ 2 ) )
85 84 oveq2d ( 𝑦 = ( 𝑥 ↑ - 𝑁 ) → ( 1 / ( 𝑦 ↑ 2 ) ) = ( 1 / ( ( 𝑥 ↑ - 𝑁 ) ↑ 2 ) ) )
86 85 negeqd ( 𝑦 = ( 𝑥 ↑ - 𝑁 ) → - ( 1 / ( 𝑦 ↑ 2 ) ) = - ( 1 / ( ( 𝑥 ↑ - 𝑁 ) ↑ 2 ) ) )
87 53 53 61 63 68 70 79 82 83 86 dvmptco ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 1 / ( 𝑥 ↑ - 𝑁 ) ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 1 / ( ( 𝑥 ↑ - 𝑁 ) ↑ 2 ) ) · ( - 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ) ) )
88 2z 2 ∈ ℤ
89 88 a1i ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → 2 ∈ ℤ )
90 expmulz ( ( ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ∧ ( - 𝑁 ∈ ℤ ∧ 2 ∈ ℤ ) ) → ( 𝑥 ↑ ( - 𝑁 · 2 ) ) = ( ( 𝑥 ↑ - 𝑁 ) ↑ 2 ) )
91 44 55 57 89 90 syl22anc ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ↑ ( - 𝑁 · 2 ) ) = ( ( 𝑥 ↑ - 𝑁 ) ↑ 2 ) )
92 91 eqcomd ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑥 ↑ - 𝑁 ) ↑ 2 ) = ( 𝑥 ↑ ( - 𝑁 · 2 ) ) )
93 92 oveq2d ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 1 / ( ( 𝑥 ↑ - 𝑁 ) ↑ 2 ) ) = ( 1 / ( 𝑥 ↑ ( - 𝑁 · 2 ) ) ) )
94 93 negeqd ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → - ( 1 / ( ( 𝑥 ↑ - 𝑁 ) ↑ 2 ) ) = - ( 1 / ( 𝑥 ↑ ( - 𝑁 · 2 ) ) ) )
95 peano2zm ( - 𝑁 ∈ ℤ → ( - 𝑁 − 1 ) ∈ ℤ )
96 57 95 syl ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( - 𝑁 − 1 ) ∈ ℤ )
97 44 55 96 expclzd ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ∈ ℂ )
98 46 97 mulneg1d ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( - 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) = - ( 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) )
99 94 98 oveq12d ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( - ( 1 / ( ( 𝑥 ↑ - 𝑁 ) ↑ 2 ) ) · ( - 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ) = ( - ( 1 / ( 𝑥 ↑ ( - 𝑁 · 2 ) ) ) · - ( 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ) )
100 zmulcl ( ( - 𝑁 ∈ ℤ ∧ 2 ∈ ℤ ) → ( - 𝑁 · 2 ) ∈ ℤ )
101 57 88 100 sylancl ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( - 𝑁 · 2 ) ∈ ℤ )
102 44 55 101 expclzd ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ↑ ( - 𝑁 · 2 ) ) ∈ ℂ )
103 44 55 101 expne0d ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ↑ ( - 𝑁 · 2 ) ) ≠ 0 )
104 102 103 reccld ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 1 / ( 𝑥 ↑ ( - 𝑁 · 2 ) ) ) ∈ ℂ )
105 46 97 mulcld ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ∈ ℂ )
106 104 105 mul2negd ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( - ( 1 / ( 𝑥 ↑ ( - 𝑁 · 2 ) ) ) · - ( 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ) = ( ( 1 / ( 𝑥 ↑ ( - 𝑁 · 2 ) ) ) · ( 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ) )
107 104 46 97 mul12d ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 1 / ( 𝑥 ↑ ( - 𝑁 · 2 ) ) ) · ( 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ) = ( 𝑁 · ( ( 1 / ( 𝑥 ↑ ( - 𝑁 · 2 ) ) ) · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ) )
108 44 55 101 96 expsubd ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ↑ ( ( - 𝑁 − 1 ) − ( - 𝑁 · 2 ) ) ) = ( ( 𝑥 ↑ ( - 𝑁 − 1 ) ) / ( 𝑥 ↑ ( - 𝑁 · 2 ) ) ) )
109 nncn ( - 𝑁 ∈ ℕ → - 𝑁 ∈ ℂ )
110 109 ad2antlr ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → - 𝑁 ∈ ℂ )
111 80 a1i ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → 1 ∈ ℂ )
112 101 zcnd ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( - 𝑁 · 2 ) ∈ ℂ )
113 110 111 112 sub32d ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( - 𝑁 − 1 ) − ( - 𝑁 · 2 ) ) = ( ( - 𝑁 − ( - 𝑁 · 2 ) ) − 1 ) )
114 110 times2d ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( - 𝑁 · 2 ) = ( - 𝑁 + - 𝑁 ) )
115 110 46 negsubd ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( - 𝑁 + - 𝑁 ) = ( - 𝑁𝑁 ) )
116 114 115 eqtrd ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( - 𝑁 · 2 ) = ( - 𝑁𝑁 ) )
117 116 oveq2d ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( - 𝑁 − ( - 𝑁 · 2 ) ) = ( - 𝑁 − ( - 𝑁𝑁 ) ) )
118 110 46 nncand ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( - 𝑁 − ( - 𝑁𝑁 ) ) = 𝑁 )
119 117 118 eqtrd ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( - 𝑁 − ( - 𝑁 · 2 ) ) = 𝑁 )
120 119 oveq1d ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( - 𝑁 − ( - 𝑁 · 2 ) ) − 1 ) = ( 𝑁 − 1 ) )
121 113 120 eqtrd ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( - 𝑁 − 1 ) − ( - 𝑁 · 2 ) ) = ( 𝑁 − 1 ) )
122 121 oveq2d ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑥 ↑ ( ( - 𝑁 − 1 ) − ( - 𝑁 · 2 ) ) ) = ( 𝑥 ↑ ( 𝑁 − 1 ) ) )
123 97 102 103 divrec2d ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 𝑥 ↑ ( - 𝑁 − 1 ) ) / ( 𝑥 ↑ ( - 𝑁 · 2 ) ) ) = ( ( 1 / ( 𝑥 ↑ ( - 𝑁 · 2 ) ) ) · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) )
124 108 122 123 3eqtr3rd ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 1 / ( 𝑥 ↑ ( - 𝑁 · 2 ) ) ) · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) = ( 𝑥 ↑ ( 𝑁 − 1 ) ) )
125 124 oveq2d ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( 𝑁 · ( ( 1 / ( 𝑥 ↑ ( - 𝑁 · 2 ) ) ) · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ) = ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) )
126 107 125 eqtrd ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( ( 1 / ( 𝑥 ↑ ( - 𝑁 · 2 ) ) ) · ( 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ) = ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) )
127 99 106 126 3eqtrd ( ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ∧ 𝑥 ∈ ( ℂ ∖ { 0 } ) ) → ( - ( 1 / ( ( 𝑥 ↑ - 𝑁 ) ↑ 2 ) ) · ( - 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ) = ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) )
128 127 mpteq2dva ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( - ( 1 / ( ( 𝑥 ↑ - 𝑁 ) ↑ 2 ) ) · ( - 𝑁 · ( 𝑥 ↑ ( - 𝑁 − 1 ) ) ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) )
129 52 87 128 3eqtrd ( ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥𝑁 ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) )
130 42 129 jaoi ( ( 𝑁 ∈ ℕ0 ∨ ( 𝑁 ∈ ℝ ∧ - 𝑁 ∈ ℕ ) ) → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥𝑁 ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) )
131 1 130 sylbi ( 𝑁 ∈ ℤ → ( ℂ D ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑥𝑁 ) ) ) = ( 𝑥 ∈ ( ℂ ∖ { 0 } ) ↦ ( 𝑁 · ( 𝑥 ↑ ( 𝑁 − 1 ) ) ) ) )