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