MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  dvexp3 Structured version   Visualization version   GIF version

Theorem dvexp3 24493
Description: Derivative of an exponential of integer exponent. (Contributed by Mario Carneiro, 26-Feb-2015.)
Assertion
Ref Expression
dvexp3 (𝑁 ∈ ℤ → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑥𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))
Distinct variable group:   𝑥,𝑁

Proof of Theorem dvexp3
Dummy variable 𝑦 is distinct from all other variables.
StepHypRef Expression
1 elznn0nn 11987 . 2 (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)))
2 cnelprrecn 10622 . . . . . 6 ℂ ∈ {ℝ, ℂ}
32a1i 11 . . . . 5 (𝑁 ∈ ℕ0 → ℂ ∈ {ℝ, ℂ})
4 expcl 13440 . . . . . 6 ((𝑥 ∈ ℂ ∧ 𝑁 ∈ ℕ0) → (𝑥𝑁) ∈ ℂ)
54ancoms 459 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℂ) → (𝑥𝑁) ∈ ℂ)
6 c0ex 10627 . . . . . . 7 0 ∈ V
7 ovex 7184 . . . . . . 7 (𝑁 · (𝑥↑(𝑁 − 1))) ∈ V
86, 7ifex 4517 . . . . . 6 if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1)))) ∈ V
98a1i 11 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ ℂ) → if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1)))) ∈ V)
10 dvexp2 24469 . . . . 5 (𝑁 ∈ ℕ0 → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥𝑁))) = (𝑥 ∈ ℂ ↦ if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1))))))
11 difssd 4112 . . . . 5 (𝑁 ∈ ℕ0 → (ℂ ∖ {0}) ⊆ ℂ)
12 eqid 2825 . . . . . . 7 (TopOpen‘ℂfld) = (TopOpen‘ℂfld)
1312cnfldtopon 23309 . . . . . 6 (TopOpen‘ℂfld) ∈ (TopOn‘ℂ)
1413toponrestid 21448 . . . . 5 (TopOpen‘ℂfld) = ((TopOpen‘ℂfld) ↾t ℂ)
1512cnfldhaus 23311 . . . . . . . 8 (TopOpen‘ℂfld) ∈ Haus
16 0cn 10625 . . . . . . . 8 0 ∈ ℂ
17 unicntop 23312 . . . . . . . . 9 ℂ = (TopOpen‘ℂfld)
1817sncld 21898 . . . . . . . 8 (((TopOpen‘ℂfld) ∈ Haus ∧ 0 ∈ ℂ) → {0} ∈ (Clsd‘(TopOpen‘ℂfld)))
1915, 16, 18mp2an 688 . . . . . . 7 {0} ∈ (Clsd‘(TopOpen‘ℂfld))
2017cldopn 21558 . . . . . . 7 ({0} ∈ (Clsd‘(TopOpen‘ℂfld)) → (ℂ ∖ {0}) ∈ (TopOpen‘ℂfld))
2119, 20ax-mp 5 . . . . . 6 (ℂ ∖ {0}) ∈ (TopOpen‘ℂfld)
2221a1i 11 . . . . 5 (𝑁 ∈ ℕ0 → (ℂ ∖ {0}) ∈ (TopOpen‘ℂfld))
233, 5, 9, 10, 11, 14, 12, 22dvmptres 24478 . . . 4 (𝑁 ∈ ℕ0 → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑥𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1))))))
24 ifid 4508 . . . . . 6 if(𝑁 = 0, (𝑁 · (𝑥↑(𝑁 − 1))), (𝑁 · (𝑥↑(𝑁 − 1)))) = (𝑁 · (𝑥↑(𝑁 − 1)))
25 id 22 . . . . . . . . 9 (𝑁 = 0 → 𝑁 = 0)
26 oveq1 7158 . . . . . . . . . 10 (𝑁 = 0 → (𝑁 − 1) = (0 − 1))
2726oveq2d 7167 . . . . . . . . 9 (𝑁 = 0 → (𝑥↑(𝑁 − 1)) = (𝑥↑(0 − 1)))
2825, 27oveq12d 7169 . . . . . . . 8 (𝑁 = 0 → (𝑁 · (𝑥↑(𝑁 − 1))) = (0 · (𝑥↑(0 − 1))))
29 eldifsn 4717 . . . . . . . . . . 11 (𝑥 ∈ (ℂ ∖ {0}) ↔ (𝑥 ∈ ℂ ∧ 𝑥 ≠ 0))
30 0z 11984 . . . . . . . . . . . . 13 0 ∈ ℤ
31 peano2zm 12017 . . . . . . . . . . . . 13 (0 ∈ ℤ → (0 − 1) ∈ ℤ)
3230, 31ax-mp 5 . . . . . . . . . . . 12 (0 − 1) ∈ ℤ
33 expclz 13447 . . . . . . . . . . . 12 ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ∧ (0 − 1) ∈ ℤ) → (𝑥↑(0 − 1)) ∈ ℂ)
3432, 33mp3an3 1443 . . . . . . . . . . 11 ((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) → (𝑥↑(0 − 1)) ∈ ℂ)
3529, 34sylbi 218 . . . . . . . . . 10 (𝑥 ∈ (ℂ ∖ {0}) → (𝑥↑(0 − 1)) ∈ ℂ)
3635adantl 482 . . . . . . . . 9 ((𝑁 ∈ ℕ0𝑥 ∈ (ℂ ∖ {0})) → (𝑥↑(0 − 1)) ∈ ℂ)
3736mul02d 10830 . . . . . . . 8 ((𝑁 ∈ ℕ0𝑥 ∈ (ℂ ∖ {0})) → (0 · (𝑥↑(0 − 1))) = 0)
3828, 37sylan9eqr 2882 . . . . . . 7 (((𝑁 ∈ ℕ0𝑥 ∈ (ℂ ∖ {0})) ∧ 𝑁 = 0) → (𝑁 · (𝑥↑(𝑁 − 1))) = 0)
3938ifeq1da 4499 . . . . . 6 ((𝑁 ∈ ℕ0𝑥 ∈ (ℂ ∖ {0})) → if(𝑁 = 0, (𝑁 · (𝑥↑(𝑁 − 1))), (𝑁 · (𝑥↑(𝑁 − 1)))) = if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1)))))
4024, 39syl5eqr 2874 . . . . 5 ((𝑁 ∈ ℕ0𝑥 ∈ (ℂ ∖ {0})) → (𝑁 · (𝑥↑(𝑁 − 1))) = if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1)))))
4140mpteq2dva 5157 . . . 4 (𝑁 ∈ ℕ0 → (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1)))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ if(𝑁 = 0, 0, (𝑁 · (𝑥↑(𝑁 − 1))))))
4223, 41eqtr4d 2863 . . 3 (𝑁 ∈ ℕ0 → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑥𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))
43 eldifi 4106 . . . . . . . 8 (𝑥 ∈ (ℂ ∖ {0}) → 𝑥 ∈ ℂ)
4443adantl 482 . . . . . . 7 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ∈ ℂ)
45 simpll 763 . . . . . . . 8 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑁 ∈ ℝ)
4645recnd 10661 . . . . . . 7 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑁 ∈ ℂ)
47 nnnn0 11896 . . . . . . . 8 (-𝑁 ∈ ℕ → -𝑁 ∈ ℕ0)
4847ad2antlr 723 . . . . . . 7 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → -𝑁 ∈ ℕ0)
49 expneg2 13431 . . . . . . 7 ((𝑥 ∈ ℂ ∧ 𝑁 ∈ ℂ ∧ -𝑁 ∈ ℕ0) → (𝑥𝑁) = (1 / (𝑥↑-𝑁)))
5044, 46, 48, 49syl3anc 1365 . . . . . 6 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥𝑁) = (1 / (𝑥↑-𝑁)))
5150mpteq2dva 5157 . . . . 5 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑥𝑁)) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / (𝑥↑-𝑁))))
5251oveq2d 7167 . . . 4 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑥𝑁))) = (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / (𝑥↑-𝑁)))))
532a1i 11 . . . . 5 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → ℂ ∈ {ℝ, ℂ})
54 eldifsni 4720 . . . . . . . 8 (𝑥 ∈ (ℂ ∖ {0}) → 𝑥 ≠ 0)
5554adantl 482 . . . . . . 7 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → 𝑥 ≠ 0)
56 nnz 11996 . . . . . . . 8 (-𝑁 ∈ ℕ → -𝑁 ∈ ℤ)
5756ad2antlr 723 . . . . . . 7 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → -𝑁 ∈ ℤ)
5844, 55, 57expclzd 13508 . . . . . 6 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥↑-𝑁) ∈ ℂ)
5944, 55, 57expne0d 13509 . . . . . 6 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥↑-𝑁) ≠ 0)
60 eldifsn 4717 . . . . . 6 ((𝑥↑-𝑁) ∈ (ℂ ∖ {0}) ↔ ((𝑥↑-𝑁) ∈ ℂ ∧ (𝑥↑-𝑁) ≠ 0))
6158, 59, 60sylanbrc 583 . . . . 5 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥↑-𝑁) ∈ (ℂ ∖ {0}))
62 ovex 7184 . . . . . 6 (-𝑁 · (𝑥↑(-𝑁 − 1))) ∈ V
6362a1i 11 . . . . 5 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (-𝑁 · (𝑥↑(-𝑁 − 1))) ∈ V)
64 simpr 485 . . . . . . 7 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑦 ∈ (ℂ ∖ {0})) → 𝑦 ∈ (ℂ ∖ {0}))
65 eldifsn 4717 . . . . . . 7 (𝑦 ∈ (ℂ ∖ {0}) ↔ (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
6664, 65sylib 219 . . . . . 6 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑦 ∈ (ℂ ∖ {0})) → (𝑦 ∈ ℂ ∧ 𝑦 ≠ 0))
67 reccl 11297 . . . . . 6 ((𝑦 ∈ ℂ ∧ 𝑦 ≠ 0) → (1 / 𝑦) ∈ ℂ)
6866, 67syl 17 . . . . 5 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑦 ∈ (ℂ ∖ {0})) → (1 / 𝑦) ∈ ℂ)
69 negex 10876 . . . . . 6 -(1 / (𝑦↑2)) ∈ V
7069a1i 11 . . . . 5 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑦 ∈ (ℂ ∖ {0})) → -(1 / (𝑦↑2)) ∈ V)
71 simpr 485 . . . . . . 7 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℂ) → 𝑥 ∈ ℂ)
7247ad2antlr 723 . . . . . . 7 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℂ) → -𝑁 ∈ ℕ0)
7371, 72expcld 13503 . . . . . 6 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℂ) → (𝑥↑-𝑁) ∈ ℂ)
7462a1i 11 . . . . . 6 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ ℂ) → (-𝑁 · (𝑥↑(-𝑁 − 1))) ∈ V)
75 dvexp 24468 . . . . . . 7 (-𝑁 ∈ ℕ → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑-𝑁))) = (𝑥 ∈ ℂ ↦ (-𝑁 · (𝑥↑(-𝑁 − 1)))))
7675adantl 482 . . . . . 6 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (ℂ D (𝑥 ∈ ℂ ↦ (𝑥↑-𝑁))) = (𝑥 ∈ ℂ ↦ (-𝑁 · (𝑥↑(-𝑁 − 1)))))
77 difssd 4112 . . . . . 6 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (ℂ ∖ {0}) ⊆ ℂ)
7821a1i 11 . . . . . 6 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (ℂ ∖ {0}) ∈ (TopOpen‘ℂfld))
7953, 73, 74, 76, 77, 14, 12, 78dvmptres 24478 . . . . 5 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑥↑-𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (-𝑁 · (𝑥↑(-𝑁 − 1)))))
80 ax-1cn 10587 . . . . . 6 1 ∈ ℂ
81 dvrec 24470 . . . . . 6 (1 ∈ ℂ → (ℂ D (𝑦 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑦))) = (𝑦 ∈ (ℂ ∖ {0}) ↦ -(1 / (𝑦↑2))))
8280, 81mp1i 13 . . . . 5 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (ℂ D (𝑦 ∈ (ℂ ∖ {0}) ↦ (1 / 𝑦))) = (𝑦 ∈ (ℂ ∖ {0}) ↦ -(1 / (𝑦↑2))))
83 oveq2 7159 . . . . 5 (𝑦 = (𝑥↑-𝑁) → (1 / 𝑦) = (1 / (𝑥↑-𝑁)))
84 oveq1 7158 . . . . . . 7 (𝑦 = (𝑥↑-𝑁) → (𝑦↑2) = ((𝑥↑-𝑁)↑2))
8584oveq2d 7167 . . . . . 6 (𝑦 = (𝑥↑-𝑁) → (1 / (𝑦↑2)) = (1 / ((𝑥↑-𝑁)↑2)))
8685negeqd 10872 . . . . 5 (𝑦 = (𝑥↑-𝑁) → -(1 / (𝑦↑2)) = -(1 / ((𝑥↑-𝑁)↑2)))
8753, 53, 61, 63, 68, 70, 79, 82, 83, 86dvmptco 24487 . . . 4 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (1 / (𝑥↑-𝑁)))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (-(1 / ((𝑥↑-𝑁)↑2)) · (-𝑁 · (𝑥↑(-𝑁 − 1))))))
88 2z 12006 . . . . . . . . . . . 12 2 ∈ ℤ
8988a1i 11 . . . . . . . . . . 11 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → 2 ∈ ℤ)
90 expmulz 13468 . . . . . . . . . . 11 (((𝑥 ∈ ℂ ∧ 𝑥 ≠ 0) ∧ (-𝑁 ∈ ℤ ∧ 2 ∈ ℤ)) → (𝑥↑(-𝑁 · 2)) = ((𝑥↑-𝑁)↑2))
9144, 55, 57, 89, 90syl22anc 836 . . . . . . . . . 10 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥↑(-𝑁 · 2)) = ((𝑥↑-𝑁)↑2))
9291eqcomd 2831 . . . . . . . . 9 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((𝑥↑-𝑁)↑2) = (𝑥↑(-𝑁 · 2)))
9392oveq2d 7167 . . . . . . . 8 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (1 / ((𝑥↑-𝑁)↑2)) = (1 / (𝑥↑(-𝑁 · 2))))
9493negeqd 10872 . . . . . . 7 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → -(1 / ((𝑥↑-𝑁)↑2)) = -(1 / (𝑥↑(-𝑁 · 2))))
95 peano2zm 12017 . . . . . . . . . 10 (-𝑁 ∈ ℤ → (-𝑁 − 1) ∈ ℤ)
9657, 95syl 17 . . . . . . . . 9 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (-𝑁 − 1) ∈ ℤ)
9744, 55, 96expclzd 13508 . . . . . . . 8 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥↑(-𝑁 − 1)) ∈ ℂ)
9846, 97mulneg1d 11085 . . . . . . 7 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (-𝑁 · (𝑥↑(-𝑁 − 1))) = -(𝑁 · (𝑥↑(-𝑁 − 1))))
9994, 98oveq12d 7169 . . . . . 6 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (-(1 / ((𝑥↑-𝑁)↑2)) · (-𝑁 · (𝑥↑(-𝑁 − 1)))) = (-(1 / (𝑥↑(-𝑁 · 2))) · -(𝑁 · (𝑥↑(-𝑁 − 1)))))
100 zmulcl 12023 . . . . . . . . . 10 ((-𝑁 ∈ ℤ ∧ 2 ∈ ℤ) → (-𝑁 · 2) ∈ ℤ)
10157, 88, 100sylancl 586 . . . . . . . . 9 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (-𝑁 · 2) ∈ ℤ)
10244, 55, 101expclzd 13508 . . . . . . . 8 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥↑(-𝑁 · 2)) ∈ ℂ)
10344, 55, 101expne0d 13509 . . . . . . . 8 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥↑(-𝑁 · 2)) ≠ 0)
104102, 103reccld 11401 . . . . . . 7 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (1 / (𝑥↑(-𝑁 · 2))) ∈ ℂ)
10546, 97mulcld 10653 . . . . . . 7 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑁 · (𝑥↑(-𝑁 − 1))) ∈ ℂ)
106104, 105mul2negd 11087 . . . . . 6 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (-(1 / (𝑥↑(-𝑁 · 2))) · -(𝑁 · (𝑥↑(-𝑁 − 1)))) = ((1 / (𝑥↑(-𝑁 · 2))) · (𝑁 · (𝑥↑(-𝑁 − 1)))))
107104, 46, 97mul12d 10841 . . . . . . 7 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((1 / (𝑥↑(-𝑁 · 2))) · (𝑁 · (𝑥↑(-𝑁 − 1)))) = (𝑁 · ((1 / (𝑥↑(-𝑁 · 2))) · (𝑥↑(-𝑁 − 1)))))
10844, 55, 101, 96expsubd 13514 . . . . . . . . 9 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥↑((-𝑁 − 1) − (-𝑁 · 2))) = ((𝑥↑(-𝑁 − 1)) / (𝑥↑(-𝑁 · 2))))
109 nncn 11638 . . . . . . . . . . . . 13 (-𝑁 ∈ ℕ → -𝑁 ∈ ℂ)
110109ad2antlr 723 . . . . . . . . . . . 12 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → -𝑁 ∈ ℂ)
11180a1i 11 . . . . . . . . . . . 12 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → 1 ∈ ℂ)
112101zcnd 12080 . . . . . . . . . . . 12 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (-𝑁 · 2) ∈ ℂ)
113110, 111, 112sub32d 11021 . . . . . . . . . . 11 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((-𝑁 − 1) − (-𝑁 · 2)) = ((-𝑁 − (-𝑁 · 2)) − 1))
114110times2d 11873 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (-𝑁 · 2) = (-𝑁 + -𝑁))
115110, 46negsubd 10995 . . . . . . . . . . . . . . 15 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (-𝑁 + -𝑁) = (-𝑁𝑁))
116114, 115eqtrd 2860 . . . . . . . . . . . . . 14 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (-𝑁 · 2) = (-𝑁𝑁))
117116oveq2d 7167 . . . . . . . . . . . . 13 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (-𝑁 − (-𝑁 · 2)) = (-𝑁 − (-𝑁𝑁)))
118110, 46nncand 10994 . . . . . . . . . . . . 13 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (-𝑁 − (-𝑁𝑁)) = 𝑁)
119117, 118eqtrd 2860 . . . . . . . . . . . 12 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (-𝑁 − (-𝑁 · 2)) = 𝑁)
120119oveq1d 7166 . . . . . . . . . . 11 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((-𝑁 − (-𝑁 · 2)) − 1) = (𝑁 − 1))
121113, 120eqtrd 2860 . . . . . . . . . 10 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((-𝑁 − 1) − (-𝑁 · 2)) = (𝑁 − 1))
122121oveq2d 7167 . . . . . . . . 9 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑥↑((-𝑁 − 1) − (-𝑁 · 2))) = (𝑥↑(𝑁 − 1)))
12397, 102, 103divrec2d 11412 . . . . . . . . 9 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((𝑥↑(-𝑁 − 1)) / (𝑥↑(-𝑁 · 2))) = ((1 / (𝑥↑(-𝑁 · 2))) · (𝑥↑(-𝑁 − 1))))
124108, 122, 1233eqtr3rd 2869 . . . . . . . 8 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((1 / (𝑥↑(-𝑁 · 2))) · (𝑥↑(-𝑁 − 1))) = (𝑥↑(𝑁 − 1)))
125124oveq2d 7167 . . . . . . 7 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (𝑁 · ((1 / (𝑥↑(-𝑁 · 2))) · (𝑥↑(-𝑁 − 1)))) = (𝑁 · (𝑥↑(𝑁 − 1))))
126107, 125eqtrd 2860 . . . . . 6 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → ((1 / (𝑥↑(-𝑁 · 2))) · (𝑁 · (𝑥↑(-𝑁 − 1)))) = (𝑁 · (𝑥↑(𝑁 − 1))))
12799, 106, 1263eqtrd 2864 . . . . 5 (((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) ∧ 𝑥 ∈ (ℂ ∖ {0})) → (-(1 / ((𝑥↑-𝑁)↑2)) · (-𝑁 · (𝑥↑(-𝑁 − 1)))) = (𝑁 · (𝑥↑(𝑁 − 1))))
128127mpteq2dva 5157 . . . 4 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (𝑥 ∈ (ℂ ∖ {0}) ↦ (-(1 / ((𝑥↑-𝑁)↑2)) · (-𝑁 · (𝑥↑(-𝑁 − 1))))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))
12952, 87, 1283eqtrd 2864 . . 3 ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ) → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑥𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))
13042, 129jaoi 853 . 2 ((𝑁 ∈ ℕ0 ∨ (𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ)) → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑥𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))
1311, 130sylbi 218 1 (𝑁 ∈ ℤ → (ℂ D (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑥𝑁))) = (𝑥 ∈ (ℂ ∖ {0}) ↦ (𝑁 · (𝑥↑(𝑁 − 1)))))
Colors of variables: wff setvar class
Syntax hints:  wi 4  wa 396  wo 843   = wceq 1530  wcel 2107  wne 3020  Vcvv 3499  cdif 3936  ifcif 4469  {csn 4563  {cpr 4565  cmpt 5142  cfv 6351  (class class class)co 7151  cc 10527  cr 10528  0cc0 10529  1c1 10530   + caddc 10532   · cmul 10534  cmin 10862  -cneg 10863   / cdiv 11289  cn 11630  2c2 11684  0cn0 11889  cz 11973  cexp 13422  TopOpenctopn 16688  fldccnfld 20464  Clsdccld 21543  Hauscha 21835   D cdv 24379
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1789  ax-4 1803  ax-5 1904  ax-6 1963  ax-7 2008  ax-8 2109  ax-9 2117  ax-10 2138  ax-11 2153  ax-12 2169  ax-ext 2797  ax-rep 5186  ax-sep 5199  ax-nul 5206  ax-pow 5262  ax-pr 5325  ax-un 7454  ax-cnex 10585  ax-resscn 10586  ax-1cn 10587  ax-icn 10588  ax-addcl 10589  ax-addrcl 10590  ax-mulcl 10591  ax-mulrcl 10592  ax-mulcom 10593  ax-addass 10594  ax-mulass 10595  ax-distr 10596  ax-i2m1 10597  ax-1ne0 10598  ax-1rid 10599  ax-rnegex 10600  ax-rrecex 10601  ax-cnre 10602  ax-pre-lttri 10603  ax-pre-lttrn 10604  ax-pre-ltadd 10605  ax-pre-mulgt0 10606  ax-pre-sup 10607  ax-addf 10608  ax-mulf 10609
This theorem depends on definitions:  df-bi 208  df-an 397  df-or 844  df-3or 1082  df-3an 1083  df-tru 1533  df-ex 1774  df-nf 1778  df-sb 2063  df-mo 2619  df-eu 2651  df-clab 2804  df-cleq 2818  df-clel 2897  df-nfc 2967  df-ne 3021  df-nel 3128  df-ral 3147  df-rex 3148  df-reu 3149  df-rmo 3150  df-rab 3151  df-v 3501  df-sbc 3776  df-csb 3887  df-dif 3942  df-un 3944  df-in 3946  df-ss 3955  df-pss 3957  df-nul 4295  df-if 4470  df-pw 4543  df-sn 4564  df-pr 4566  df-tp 4568  df-op 4570  df-uni 4837  df-int 4874  df-iun 4918  df-iin 4919  df-br 5063  df-opab 5125  df-mpt 5143  df-tr 5169  df-id 5458  df-eprel 5463  df-po 5472  df-so 5473  df-fr 5512  df-se 5513  df-we 5514  df-xp 5559  df-rel 5560  df-cnv 5561  df-co 5562  df-dm 5563  df-rn 5564  df-res 5565  df-ima 5566  df-pred 6145  df-ord 6191  df-on 6192  df-lim 6193  df-suc 6194  df-iota 6311  df-fun 6353  df-fn 6354  df-f 6355  df-f1 6356  df-fo 6357  df-f1o 6358  df-fv 6359  df-isom 6360  df-riota 7109  df-ov 7154  df-oprab 7155  df-mpo 7156  df-of 7402  df-om 7572  df-1st 7683  df-2nd 7684  df-supp 7825  df-wrecs 7941  df-recs 8002  df-rdg 8040  df-1o 8096  df-2o 8097  df-oadd 8100  df-er 8282  df-map 8401  df-pm 8402  df-ixp 8454  df-en 8502  df-dom 8503  df-sdom 8504  df-fin 8505  df-fsupp 8826  df-fi 8867  df-sup 8898  df-inf 8899  df-oi 8966  df-card 9360  df-pnf 10669  df-mnf 10670  df-xr 10671  df-ltxr 10672  df-le 10673  df-sub 10864  df-neg 10865  df-div 11290  df-nn 11631  df-2 11692  df-3 11693  df-4 11694  df-5 11695  df-6 11696  df-7 11697  df-8 11698  df-9 11699  df-n0 11890  df-z 11974  df-dec 12091  df-uz 12236  df-q 12341  df-rp 12383  df-xneg 12500  df-xadd 12501  df-xmul 12502  df-icc 12738  df-fz 12886  df-fzo 13027  df-seq 13363  df-exp 13423  df-hash 13684  df-cj 14451  df-re 14452  df-im 14453  df-sqrt 14587  df-abs 14588  df-struct 16478  df-ndx 16479  df-slot 16480  df-base 16482  df-sets 16483  df-ress 16484  df-plusg 16571  df-mulr 16572  df-starv 16573  df-sca 16574  df-vsca 16575  df-ip 16576  df-tset 16577  df-ple 16578  df-ds 16580  df-unif 16581  df-hom 16582  df-cco 16583  df-rest 16689  df-topn 16690  df-0g 16708  df-gsum 16709  df-topgen 16710  df-pt 16711  df-prds 16714  df-xrs 16768  df-qtop 16773  df-imas 16774  df-xps 16776  df-mre 16850  df-mrc 16851  df-acs 16853  df-mgm 17845  df-sgrp 17893  df-mnd 17904  df-submnd 17948  df-mulg 18158  df-cntz 18380  df-cmn 18831  df-psmet 20456  df-xmet 20457  df-met 20458  df-bl 20459  df-mopn 20460  df-fbas 20461  df-fg 20462  df-cnfld 20465  df-top 21421  df-topon 21438  df-topsp 21460  df-bases 21473  df-cld 21546  df-ntr 21547  df-cls 21548  df-nei 21625  df-lp 21663  df-perf 21664  df-cn 21754  df-cnp 21755  df-t1 21841  df-haus 21842  df-tx 22089  df-hmeo 22282  df-fil 22373  df-fm 22465  df-flim 22466  df-flf 22467  df-xms 22848  df-ms 22849  df-tms 22850  df-cncf 23404  df-limc 24382  df-dv 24383
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator