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
|
syl5eqr |
⊢ ( ( 𝑁 ∈ ℕ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 ) ) ) ) ) |