| Step | Hyp | Ref | Expression | 
|---|
| 1 |  | elznn0nn 12629 | . 2
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨
(𝑁 ∈ ℝ ∧
-𝑁 ∈
ℕ))) | 
| 2 |  | cnelprrecn 11249 | . . . . . 6
⊢ ℂ
∈ {ℝ, ℂ} | 
| 3 | 2 | a1i 11 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ ℂ ∈ {ℝ, ℂ}) | 
| 4 |  | expcl 14121 | . . . . . 6
⊢ ((𝑥 ∈ ℂ ∧ 𝑁 ∈ ℕ0)
→ (𝑥↑𝑁) ∈
ℂ) | 
| 5 | 4 | ancoms 458 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℂ)
→ (𝑥↑𝑁) ∈
ℂ) | 
| 6 |  | c0ex 11256 | . . . . . . 7
⊢ 0 ∈
V | 
| 7 |  | ovex 7465 | . . . . . . 7
⊢ (𝑁 · (𝑥↑(𝑁 − 1))) ∈ V | 
| 8 | 6, 7 | ifex 4575 | . . . . . 6
⊢ if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1)))) ∈ V | 
| 9 | 8 | a1i 11 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ ℂ)
→ if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1)))) ∈ V) | 
| 10 |  | dvexp2 25993 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ (ℂ D (𝑥 ∈
ℂ ↦ (𝑥↑𝑁))) = (𝑥 ∈ ℂ ↦ if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1)))))) | 
| 11 |  | difssd 4136 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ (ℂ ∖ {0}) ⊆ ℂ) | 
| 12 |  | eqid 2736 | . . . . . . 7
⊢
(TopOpen‘ℂfld) =
(TopOpen‘ℂfld) | 
| 13 | 12 | cnfldtopon 24804 | . . . . . 6
⊢
(TopOpen‘ℂfld) ∈
(TopOn‘ℂ) | 
| 14 | 13 | toponrestid 22928 | . . . . 5
⊢
(TopOpen‘ℂfld) =
((TopOpen‘ℂfld) ↾t
ℂ) | 
| 15 |  | cnn0opn 24809 | . . . . . 6
⊢ (ℂ
∖ {0}) ∈ (TopOpen‘ℂfld) | 
| 16 | 15 | a1i 11 | . . . . 5
⊢ (𝑁 ∈ ℕ0
→ (ℂ ∖ {0}) ∈
(TopOpen‘ℂfld)) | 
| 17 | 3, 5, 9, 10, 11, 14, 12, 16 | dvmptres 26002 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ (ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝑥↑𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦
if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1)))))) | 
| 18 |  | ifid 4565 | . . . . . 6
⊢ if(𝑁 = 0, (𝑁 · (𝑥↑(𝑁 − 1))), (𝑁 · (𝑥↑(𝑁 − 1)))) = (𝑁 · (𝑥↑(𝑁 − 1))) | 
| 19 |  | id 22 | . . . . . . . . 9
⊢ (𝑁 = 0 → 𝑁 = 0) | 
| 20 |  | oveq1 7439 | . . . . . . . . . 10
⊢ (𝑁 = 0 → (𝑁 − 1) = (0 −
1)) | 
| 21 | 20 | oveq2d 7448 | . . . . . . . . 9
⊢ (𝑁 = 0 → (𝑥↑(𝑁 − 1)) = (𝑥↑(0 − 1))) | 
| 22 | 19, 21 | oveq12d 7450 | . . . . . . . 8
⊢ (𝑁 = 0 → (𝑁 · (𝑥↑(𝑁 − 1))) = (0 · (𝑥↑(0 −
1)))) | 
| 23 |  | eldifsn 4785 | . . . . . . . . . . 11
⊢ (𝑥 ∈ (ℂ ∖ {0})
↔ (𝑥 ∈ ℂ
∧ 𝑥 ≠
0)) | 
| 24 |  | 0z 12626 | . . . . . . . . . . . . 13
⊢ 0 ∈
ℤ | 
| 25 |  | peano2zm 12662 | . . . . . . . . . . . . 13
⊢ (0 ∈
ℤ → (0 − 1) ∈ ℤ) | 
| 26 | 24, 25 | ax-mp 5 | . . . . . . . . . . . 12
⊢ (0
− 1) ∈ ℤ | 
| 27 |  | expclz 14126 | . . . . . . . . . . . 12
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ∧ (0 − 1)
∈ ℤ) → (𝑥↑(0 − 1)) ∈
ℂ) | 
| 28 | 26, 27 | mp3an3 1451 | . . . . . . . . . . 11
⊢ ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥↑(0 − 1)) ∈
ℂ) | 
| 29 | 23, 28 | sylbi 217 | . . . . . . . . . 10
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ (𝑥↑(0 −
1)) ∈ ℂ) | 
| 30 | 29 | adantl 481 | . . . . . . . . 9
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ (ℂ
∖ {0})) → (𝑥↑(0 − 1)) ∈
ℂ) | 
| 31 | 30 | mul02d 11460 | . . . . . . . 8
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ (ℂ
∖ {0})) → (0 · (𝑥↑(0 − 1))) = 0) | 
| 32 | 22, 31 | sylan9eqr 2798 | . . . . . . 7
⊢ (((𝑁 ∈ ℕ0
∧ 𝑥 ∈ (ℂ
∖ {0})) ∧ 𝑁 = 0)
→ (𝑁 · (𝑥↑(𝑁 − 1))) = 0) | 
| 33 | 32 | ifeq1da 4556 | . . . . . 6
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ (ℂ
∖ {0})) → if(𝑁 =
0, (𝑁 · (𝑥↑(𝑁 − 1))), (𝑁 · (𝑥↑(𝑁 − 1)))) = if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1))))) | 
| 34 | 18, 33 | eqtr3id 2790 | . . . . 5
⊢ ((𝑁 ∈ ℕ0
∧ 𝑥 ∈ (ℂ
∖ {0})) → (𝑁
· (𝑥↑(𝑁 − 1))) = if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1))))) | 
| 35 | 34 | mpteq2dva 5241 | . . . 4
⊢ (𝑁 ∈ ℕ0
→ (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝑁
· (𝑥↑(𝑁 − 1)))) = (𝑥 ∈ (ℂ ∖ {0})
↦ if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1)))))) | 
| 36 | 17, 35 | eqtr4d 2779 | . . 3
⊢ (𝑁 ∈ ℕ0
→ (ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝑥↑𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1))))) | 
| 37 |  | eldifi 4130 | . . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ 𝑥 ∈
ℂ) | 
| 38 | 37 | adantl 481 | . . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ 𝑥 ∈
ℂ) | 
| 39 |  | simpll 766 | . . . . . . . 8
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ 𝑁 ∈
ℝ) | 
| 40 | 39 | recnd 11290 | . . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ 𝑁 ∈
ℂ) | 
| 41 |  | nnnn0 12535 | . . . . . . . 8
⊢ (-𝑁 ∈ ℕ → -𝑁 ∈
ℕ0) | 
| 42 | 41 | ad2antlr 727 | . . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ -𝑁 ∈
ℕ0) | 
| 43 |  | expneg2 14112 | . . . . . . 7
⊢ ((𝑥 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0)
→ (𝑥↑𝑁) = (1 / (𝑥↑-𝑁))) | 
| 44 | 38, 40, 42, 43 | syl3anc 1372 | . . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (𝑥↑𝑁) = (1 / (𝑥↑-𝑁))) | 
| 45 | 44 | mpteq2dva 5241 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (𝑥 ∈ (ℂ ∖ {0})
↦ (𝑥↑𝑁)) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 /
(𝑥↑-𝑁)))) | 
| 46 | 45 | oveq2d 7448 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝑥↑𝑁))) = (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 /
(𝑥↑-𝑁))))) | 
| 47 | 2 | a1i 11 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → ℂ
∈ {ℝ, ℂ}) | 
| 48 |  | eldifsni 4789 | . . . . . . . 8
⊢ (𝑥 ∈ (ℂ ∖ {0})
→ 𝑥 ≠
0) | 
| 49 | 48 | adantl 481 | . . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ 𝑥 ≠
0) | 
| 50 |  | nnz 12636 | . . . . . . . 8
⊢ (-𝑁 ∈ ℕ → -𝑁 ∈
ℤ) | 
| 51 | 50 | ad2antlr 727 | . . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ -𝑁 ∈
ℤ) | 
| 52 | 38, 49, 51 | expclzd 14192 | . . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (𝑥↑-𝑁) ∈
ℂ) | 
| 53 | 38, 49, 51 | expne0d 14193 | . . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (𝑥↑-𝑁) ≠ 0) | 
| 54 |  | eldifsn 4785 | . . . . . 6
⊢ ((𝑥↑-𝑁) ∈ (ℂ ∖ {0}) ↔
((𝑥↑-𝑁) ∈ ℂ ∧ (𝑥↑-𝑁) ≠ 0)) | 
| 55 | 52, 53, 54 | sylanbrc 583 | . . . . 5
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (𝑥↑-𝑁) ∈ (ℂ ∖
{0})) | 
| 56 |  | ovex 7465 | . . . . . 6
⊢ (-𝑁 · (𝑥↑(-𝑁 − 1))) ∈ V | 
| 57 | 56 | a1i 11 | . . . . 5
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (-𝑁 · (𝑥↑(-𝑁 − 1))) ∈ V) | 
| 58 |  | simpr 484 | . . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ 𝑦 ∈ (ℂ
∖ {0})) | 
| 59 |  | eldifsn 4785 | . . . . . . 7
⊢ (𝑦 ∈ (ℂ ∖ {0})
↔ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) | 
| 60 | 58, 59 | sylib 218 | . . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (𝑦 ∈ ℂ
∧ 𝑦 ≠
0)) | 
| 61 |  | reccl 11930 | . . . . . 6
⊢ ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (1 / 𝑦) ∈
ℂ) | 
| 62 | 60, 61 | syl 17 | . . . . 5
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ (1 / 𝑦) ∈
ℂ) | 
| 63 |  | negex 11507 | . . . . . 6
⊢ -(1 /
(𝑦↑2)) ∈
V | 
| 64 | 63 | a1i 11 | . . . . 5
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑦 ∈ (ℂ ∖ {0}))
→ -(1 / (𝑦↑2))
∈ V) | 
| 65 |  | simpr 484 | . . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℂ) → 𝑥 ∈
ℂ) | 
| 66 | 41 | ad2antlr 727 | . . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℂ) → -𝑁 ∈
ℕ0) | 
| 67 | 65, 66 | expcld 14187 | . . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℂ) → (𝑥↑-𝑁) ∈ ℂ) | 
| 68 | 56 | a1i 11 | . . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℂ) → (-𝑁 · (𝑥↑(-𝑁 − 1))) ∈ V) | 
| 69 |  | dvexp 25992 | . . . . . . 7
⊢ (-𝑁 ∈ ℕ → (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑-𝑁))) = (𝑥 ∈ ℂ ↦ (-𝑁 · (𝑥↑(-𝑁 − 1))))) | 
| 70 | 69 | adantl 481 | . . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (ℂ
D (𝑥 ∈ ℂ ↦
(𝑥↑-𝑁))) = (𝑥 ∈ ℂ ↦ (-𝑁 · (𝑥↑(-𝑁 − 1))))) | 
| 71 |  | difssd 4136 | . . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (ℂ
∖ {0}) ⊆ ℂ) | 
| 72 | 15 | a1i 11 | . . . . . 6
⊢ ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (ℂ
∖ {0}) ∈ (TopOpen‘ℂfld)) | 
| 73 | 47, 67, 68, 70, 71, 14, 12, 72 | dvmptres 26002 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝑥↑-𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (-𝑁 · (𝑥↑(-𝑁 − 1))))) | 
| 74 |  | ax-1cn 11214 | . . . . . 6
⊢ 1 ∈
ℂ | 
| 75 |  | dvrec 25994 | . . . . . 6
⊢ (1 ∈
ℂ → (ℂ D (𝑦 ∈ (ℂ ∖ {0}) ↦ (1 /
𝑦))) = (𝑦 ∈ (ℂ ∖ {0}) ↦ -(1 /
(𝑦↑2)))) | 
| 76 | 74, 75 | mp1i 13 | . . . . 5
⊢ ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (ℂ
D (𝑦 ∈ (ℂ
∖ {0}) ↦ (1 / 𝑦))) = (𝑦 ∈ (ℂ ∖ {0}) ↦ -(1 /
(𝑦↑2)))) | 
| 77 |  | oveq2 7440 | . . . . 5
⊢ (𝑦 = (𝑥↑-𝑁) → (1 / 𝑦) = (1 / (𝑥↑-𝑁))) | 
| 78 |  | oveq1 7439 | . . . . . . 7
⊢ (𝑦 = (𝑥↑-𝑁) → (𝑦↑2) = ((𝑥↑-𝑁)↑2)) | 
| 79 | 78 | oveq2d 7448 | . . . . . 6
⊢ (𝑦 = (𝑥↑-𝑁) → (1 / (𝑦↑2)) = (1 / ((𝑥↑-𝑁)↑2))) | 
| 80 | 79 | negeqd 11503 | . . . . 5
⊢ (𝑦 = (𝑥↑-𝑁) → -(1 / (𝑦↑2)) = -(1 / ((𝑥↑-𝑁)↑2))) | 
| 81 | 47, 47, 55, 57, 62, 64, 73, 76, 77, 80 | dvmptco 26011 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (1 / (𝑥↑-𝑁)))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (-(1 /
((𝑥↑-𝑁)↑2)) · (-𝑁 · (𝑥↑(-𝑁 − 1)))))) | 
| 82 |  | 2z 12651 | . . . . . . . . . . . 12
⊢ 2 ∈
ℤ | 
| 83 | 82 | a1i 11 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ 2 ∈ ℤ) | 
| 84 |  | expmulz 14150 | . . . . . . . . . . 11
⊢ (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (-𝑁 ∈ ℤ ∧ 2 ∈
ℤ)) → (𝑥↑(-𝑁 · 2)) = ((𝑥↑-𝑁)↑2)) | 
| 85 | 38, 49, 51, 83, 84 | syl22anc 838 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (𝑥↑(-𝑁 · 2)) = ((𝑥↑-𝑁)↑2)) | 
| 86 | 85 | eqcomd 2742 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ ((𝑥↑-𝑁)↑2) = (𝑥↑(-𝑁 · 2))) | 
| 87 | 86 | oveq2d 7448 | . . . . . . . 8
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (1 / ((𝑥↑-𝑁)↑2)) = (1 / (𝑥↑(-𝑁 · 2)))) | 
| 88 | 87 | negeqd 11503 | . . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ -(1 / ((𝑥↑-𝑁)↑2)) = -(1 / (𝑥↑(-𝑁 · 2)))) | 
| 89 |  | peano2zm 12662 | . . . . . . . . . 10
⊢ (-𝑁 ∈ ℤ → (-𝑁 − 1) ∈
ℤ) | 
| 90 | 51, 89 | syl 17 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (-𝑁 − 1)
∈ ℤ) | 
| 91 | 38, 49, 90 | expclzd 14192 | . . . . . . . 8
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (𝑥↑(-𝑁 − 1)) ∈
ℂ) | 
| 92 | 40, 91 | mulneg1d 11717 | . . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (-𝑁 · (𝑥↑(-𝑁 − 1))) = -(𝑁 · (𝑥↑(-𝑁 − 1)))) | 
| 93 | 88, 92 | oveq12d 7450 | . . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (-(1 / ((𝑥↑-𝑁)↑2)) · (-𝑁 · (𝑥↑(-𝑁 − 1)))) = (-(1 / (𝑥↑(-𝑁 · 2))) · -(𝑁 · (𝑥↑(-𝑁 − 1))))) | 
| 94 |  | zmulcl 12668 | . . . . . . . . . 10
⊢ ((-𝑁 ∈ ℤ ∧ 2 ∈
ℤ) → (-𝑁
· 2) ∈ ℤ) | 
| 95 | 51, 82, 94 | sylancl 586 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (-𝑁 · 2)
∈ ℤ) | 
| 96 | 38, 49, 95 | expclzd 14192 | . . . . . . . 8
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (𝑥↑(-𝑁 · 2)) ∈
ℂ) | 
| 97 | 38, 49, 95 | expne0d 14193 | . . . . . . . 8
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (𝑥↑(-𝑁 · 2)) ≠
0) | 
| 98 | 96, 97 | reccld 12037 | . . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (1 / (𝑥↑(-𝑁 · 2))) ∈
ℂ) | 
| 99 | 40, 91 | mulcld 11282 | . . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (𝑁 · (𝑥↑(-𝑁 − 1))) ∈
ℂ) | 
| 100 | 98, 99 | mul2negd 11719 | . . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (-(1 / (𝑥↑(-𝑁 · 2))) · -(𝑁 · (𝑥↑(-𝑁 − 1)))) = ((1 / (𝑥↑(-𝑁 · 2))) · (𝑁 · (𝑥↑(-𝑁 − 1))))) | 
| 101 | 98, 40, 91 | mul12d 11471 | . . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ ((1 / (𝑥↑(-𝑁 · 2))) · (𝑁 · (𝑥↑(-𝑁 − 1)))) = (𝑁 · ((1 / (𝑥↑(-𝑁 · 2))) · (𝑥↑(-𝑁 − 1))))) | 
| 102 | 38, 49, 95, 90 | expsubd 14198 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (𝑥↑((-𝑁 − 1) − (-𝑁 · 2))) = ((𝑥↑(-𝑁 − 1)) / (𝑥↑(-𝑁 · 2)))) | 
| 103 |  | nncn 12275 | . . . . . . . . . . . . 13
⊢ (-𝑁 ∈ ℕ → -𝑁 ∈
ℂ) | 
| 104 | 103 | ad2antlr 727 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ -𝑁 ∈
ℂ) | 
| 105 | 74 | a1i 11 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ 1 ∈ ℂ) | 
| 106 | 95 | zcnd 12725 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (-𝑁 · 2)
∈ ℂ) | 
| 107 | 104, 105,
106 | sub32d 11653 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ ((-𝑁 − 1)
− (-𝑁 · 2)) =
((-𝑁 − (-𝑁 · 2)) −
1)) | 
| 108 | 104 | times2d 12512 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (-𝑁 · 2) =
(-𝑁 + -𝑁)) | 
| 109 | 104, 40 | negsubd 11627 | . . . . . . . . . . . . . . 15
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (-𝑁 + -𝑁) = (-𝑁 − 𝑁)) | 
| 110 | 108, 109 | eqtrd 2776 | . . . . . . . . . . . . . 14
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (-𝑁 · 2) =
(-𝑁 − 𝑁)) | 
| 111 | 110 | oveq2d 7448 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (-𝑁 − (-𝑁 · 2)) = (-𝑁 − (-𝑁 − 𝑁))) | 
| 112 | 104, 40 | nncand 11626 | . . . . . . . . . . . . 13
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (-𝑁 − (-𝑁 − 𝑁)) = 𝑁) | 
| 113 | 111, 112 | eqtrd 2776 | . . . . . . . . . . . 12
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (-𝑁 − (-𝑁 · 2)) = 𝑁) | 
| 114 | 113 | oveq1d 7447 | . . . . . . . . . . 11
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ ((-𝑁 − (-𝑁 · 2)) − 1) =
(𝑁 −
1)) | 
| 115 | 107, 114 | eqtrd 2776 | . . . . . . . . . 10
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ ((-𝑁 − 1)
− (-𝑁 · 2)) =
(𝑁 −
1)) | 
| 116 | 115 | oveq2d 7448 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (𝑥↑((-𝑁 − 1) − (-𝑁 · 2))) = (𝑥↑(𝑁 − 1))) | 
| 117 | 91, 96, 97 | divrec2d 12048 | . . . . . . . . 9
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ ((𝑥↑(-𝑁 − 1)) / (𝑥↑(-𝑁 · 2))) = ((1 / (𝑥↑(-𝑁 · 2))) · (𝑥↑(-𝑁 − 1)))) | 
| 118 | 102, 116,
117 | 3eqtr3rd 2785 | . . . . . . . 8
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ ((1 / (𝑥↑(-𝑁 · 2))) · (𝑥↑(-𝑁 − 1))) = (𝑥↑(𝑁 − 1))) | 
| 119 | 118 | oveq2d 7448 | . . . . . . 7
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (𝑁 · ((1 /
(𝑥↑(-𝑁 · 2))) · (𝑥↑(-𝑁 − 1)))) = (𝑁 · (𝑥↑(𝑁 − 1)))) | 
| 120 | 101, 119 | eqtrd 2776 | . . . . . 6
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ ((1 / (𝑥↑(-𝑁 · 2))) · (𝑁 · (𝑥↑(-𝑁 − 1)))) = (𝑁 · (𝑥↑(𝑁 − 1)))) | 
| 121 | 93, 100, 120 | 3eqtrd 2780 | . . . . 5
⊢ (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0}))
→ (-(1 / ((𝑥↑-𝑁)↑2)) · (-𝑁 · (𝑥↑(-𝑁 − 1)))) = (𝑁 · (𝑥↑(𝑁 − 1)))) | 
| 122 | 121 | mpteq2dva 5241 | . . . 4
⊢ ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (𝑥 ∈ (ℂ ∖ {0})
↦ (-(1 / ((𝑥↑-𝑁)↑2)) · (-𝑁 · (𝑥↑(-𝑁 − 1))))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1))))) | 
| 123 | 46, 81, 122 | 3eqtrd 2780 | . . 3
⊢ ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝑥↑𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1))))) | 
| 124 | 36, 123 | jaoi 857 | . 2
⊢ ((𝑁 ∈ ℕ0 ∨
(𝑁 ∈ ℝ ∧
-𝑁 ∈ ℕ)) →
(ℂ D (𝑥 ∈
(ℂ ∖ {0}) ↦ (𝑥↑𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1))))) | 
| 125 | 1, 124 | sylbi 217 | 1
⊢ (𝑁 ∈ ℤ → (ℂ
D (𝑥 ∈ (ℂ
∖ {0}) ↦ (𝑥↑𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1))))) |