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 ) ) ) ) )