dvexp3

Description: Derivative of an exponential of integer exponent. (Contributed by Mario Carneiro, 26-Feb-2015)

		Ref	Expression
	Assertion	dvexp3	$⊢ N \in ℤ \to \frac{d (x \in (ℂ ∖ \{0\})⟼ x^{N})}{d_{ℂ} x} = (x \in (ℂ ∖ \{0\}) ⟼ N x^{N - 1})$

Proof

Step	Hyp	Ref	Expression
1		elznn0nn	$⊢ N \in ℤ \leftrightarrow (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ))$
2		cnelprrecn	$⊢ ℂ \in \{ℝ, ℂ\}$
3	2	a1i	$⊢ N \in ℕ_{0} \to ℂ \in \{ℝ, ℂ\}$
4		expcl	$⊢ (x \in ℂ \land N \in ℕ_{0}) \to x^{N} \in ℂ$
5	4	ancoms	$⊢ (N \in ℕ_{0} \land x \in ℂ) \to x^{N} \in ℂ$
6		c0ex	$⊢ 0 \in V$
7		ovex	$⊢ N x^{N - 1} \in V$
8	6 7	ifex	$⊢ if (N = 0, 0, N x^{N - 1}) \in V$
9	8	a1i	$⊢ (N \in ℕ_{0} \land x \in ℂ) \to if (N = 0, 0, N x^{N - 1}) \in V$
10		dvexp2	$⊢ N \in ℕ_{0} \to \frac{d (x \in ℂ⟼ x^{N})}{d_{ℂ} x} = (x \in ℂ ⟼ if (N = 0, 0, N x^{N - 1}))$
11		difssd	$⊢ N \in ℕ_{0} \to ℂ ∖ \{0\} \subseteq ℂ$
12		eqid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld})$
13	12	cnfldtopon	$⊢ TopOpen (ℂ_{fld}) \in TopOn (ℂ)$
14	13	toponrestid	$⊢ TopOpen (ℂ_{fld}) = TopOpen (ℂ_{fld}) ↾_{𝑡} ℂ$
15	12	cnfldhaus	$⊢ TopOpen (ℂ_{fld}) \in Haus$
16		0cn	$⊢ 0 \in ℂ$
17		unicntop	$⊢ ℂ = ⋃ TopOpen (ℂ_{fld})$
18	17	sncld	$⊢ (TopOpen (ℂ_{fld}) \in Haus \land 0 \in ℂ) \to \{0\} \in Clsd (TopOpen (ℂ_{fld}))$
19	15 16 18	mp2an	$⊢ \{0\} \in Clsd (TopOpen (ℂ_{fld}))$
20	17	cldopn	$⊢ \{0\} \in Clsd (TopOpen (ℂ_{fld})) \to ℂ ∖ \{0\} \in TopOpen (ℂ_{fld})$
21	19 20	ax-mp	$⊢ ℂ ∖ \{0\} \in TopOpen (ℂ_{fld})$
22	21	a1i	$⊢ N \in ℕ_{0} \to ℂ ∖ \{0\} \in TopOpen (ℂ_{fld})$
23	3 5 9 10 11 14 12 22	dvmptres	$⊢ N \in ℕ_{0} \to \frac{d (x \in (ℂ ∖ \{0\})⟼ x^{N})}{d_{ℂ} x} = (x \in (ℂ ∖ \{0\}) ⟼ if (N = 0, 0, N x^{N - 1}))$
24		ifid	$⊢ if (N = 0, N x^{N - 1}, N x^{N - 1}) = N x^{N - 1}$
25		id	$⊢ N = 0 \to N = 0$
26		oveq1	$⊢ N = 0 \to N - 1 = 0 - 1$
27	26	oveq2d	$⊢ N = 0 \to x^{N - 1} = x^{0 - 1}$
28	25 27	oveq12d	$⊢ N = 0 \to N x^{N - 1} = 0 \cdot x^{0 - 1}$
29		eldifsn	$⊢ x \in (ℂ ∖ \{0\}) \leftrightarrow (x \in ℂ \land x \neq 0)$
30		0z	$⊢ 0 \in ℤ$
31		peano2zm	$⊢ 0 \in ℤ \to 0 - 1 \in ℤ$
32	30 31	ax-mp	$⊢ 0 - 1 \in ℤ$
33		expclz	$⊢ (x \in ℂ \land x \neq 0 \land 0 - 1 \in ℤ) \to x^{0 - 1} \in ℂ$
34	32 33	mp3an3	$⊢ (x \in ℂ \land x \neq 0) \to x^{0 - 1} \in ℂ$
35	29 34	sylbi	$⊢ x \in (ℂ ∖ \{0\}) \to x^{0 - 1} \in ℂ$
36	35	adantl	$⊢ (N \in ℕ_{0} \land x \in (ℂ ∖ \{0\})) \to x^{0 - 1} \in ℂ$
37	36	mul02d	$⊢ (N \in ℕ_{0} \land x \in (ℂ ∖ \{0\})) \to 0 \cdot x^{0 - 1} = 0$
38	28 37	sylan9eqr	$⊢ ((N \in ℕ_{0} \land x \in (ℂ ∖ \{0\})) \land N = 0) \to N x^{N - 1} = 0$
39	38	ifeq1da	$⊢ (N \in ℕ_{0} \land x \in (ℂ ∖ \{0\})) \to if (N = 0, N x^{N - 1}, N x^{N - 1}) = if (N = 0, 0, N x^{N - 1})$
40	24 39	syl5eqr	$⊢ (N \in ℕ_{0} \land x \in (ℂ ∖ \{0\})) \to N x^{N - 1} = if (N = 0, 0, N x^{N - 1})$
41	40	mpteq2dva	$⊢ N \in ℕ_{0} \to (x \in (ℂ ∖ \{0\}) ⟼ N x^{N - 1}) = (x \in (ℂ ∖ \{0\}) ⟼ if (N = 0, 0, N x^{N - 1}))$
42	23 41	eqtr4d	$⊢ N \in ℕ_{0} \to \frac{d (x \in (ℂ ∖ \{0\})⟼ x^{N})}{d_{ℂ} x} = (x \in (ℂ ∖ \{0\}) ⟼ N x^{N - 1})$
43		eldifi	$⊢ x \in (ℂ ∖ \{0\}) \to x \in ℂ$
44	43	adantl	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x \in ℂ$
45		simpll	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to N \in ℝ$
46	45	recnd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to N \in ℂ$
47		nnnn0	$⊢ - N \in ℕ \to - N \in ℕ_{0}$
48	47	ad2antlr	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N \in ℕ_{0}$
49		expneg2	$⊢ (x \in ℂ \land N \in ℂ \land - N \in ℕ_{0}) \to x^{N} = \frac{1}{x^{- N}}$
50	44 46 48 49	syl3anc	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{N} = \frac{1}{x^{- N}}$
51	50	mpteq2dva	$⊢ (N \in ℝ \land - N \in ℕ) \to (x \in (ℂ ∖ \{0\}) ⟼ x^{N}) = (x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x^{- N}})$
52	51	oveq2d	$⊢ (N \in ℝ \land - N \in ℕ) \to \frac{d (x \in (ℂ ∖ \{0\})⟼ x^{N})}{d_{ℂ} x} = \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{1}{x^{- N}})}{d_{ℂ} x}$
53	2	a1i	$⊢ (N \in ℝ \land - N \in ℕ) \to ℂ \in \{ℝ, ℂ\}$
54		eldifsni	$⊢ x \in (ℂ ∖ \{0\}) \to x \neq 0$
55	54	adantl	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x \neq 0$
56		nnz	$⊢ - N \in ℕ \to - N \in ℤ$
57	56	ad2antlr	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N \in ℤ$
58	44 55 57	expclzd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{- N} \in ℂ$
59	44 55 57	expne0d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{- N} \neq 0$
60		eldifsn	$⊢ x^{- N} \in (ℂ ∖ \{0\}) \leftrightarrow (x^{- N} \in ℂ \land x^{- N} \neq 0)$
61	58 59 60	sylanbrc	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{- N} \in (ℂ ∖ \{0\})$
62		ovex	$⊢ -N x^{- N - 1} \in V$
63	62	a1i	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N x^{- N - 1} \in V$
64		simpr	$⊢ ((N \in ℝ \land - N \in ℕ) \land y \in (ℂ ∖ \{0\})) \to y \in (ℂ ∖ \{0\})$
65		eldifsn	$⊢ y \in (ℂ ∖ \{0\}) \leftrightarrow (y \in ℂ \land y \neq 0)$
66	64 65	sylib	$⊢ ((N \in ℝ \land - N \in ℕ) \land y \in (ℂ ∖ \{0\})) \to (y \in ℂ \land y \neq 0)$
67		reccl	$⊢ (y \in ℂ \land y \neq 0) \to \frac{1}{y} \in ℂ$
68	66 67	syl	$⊢ ((N \in ℝ \land - N \in ℕ) \land y \in (ℂ ∖ \{0\})) \to \frac{1}{y} \in ℂ$
69		negex	$⊢ - \frac{1}{y^{2}} \in V$
70	69	a1i	$⊢ ((N \in ℝ \land - N \in ℕ) \land y \in (ℂ ∖ \{0\})) \to - \frac{1}{y^{2}} \in V$
71		simpr	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in ℂ) \to x \in ℂ$
72	47	ad2antlr	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in ℂ) \to - N \in ℕ_{0}$
73	71 72	expcld	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in ℂ) \to x^{- N} \in ℂ$
74	62	a1i	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in ℂ) \to -N x^{- N - 1} \in V$
75		dvexp	$⊢ - N \in ℕ \to \frac{d (x \in ℂ⟼ x^{- N})}{d_{ℂ} x} = (x \in ℂ ⟼ -N x^{- N - 1})$
76	75	adantl	$⊢ (N \in ℝ \land - N \in ℕ) \to \frac{d (x \in ℂ⟼ x^{- N})}{d_{ℂ} x} = (x \in ℂ ⟼ -N x^{- N - 1})$
77		difssd	$⊢ (N \in ℝ \land - N \in ℕ) \to ℂ ∖ \{0\} \subseteq ℂ$
78	21	a1i	$⊢ (N \in ℝ \land - N \in ℕ) \to ℂ ∖ \{0\} \in TopOpen (ℂ_{fld})$
79	53 73 74 76 77 14 12 78	dvmptres	$⊢ (N \in ℝ \land - N \in ℕ) \to \frac{d (x \in (ℂ ∖ \{0\})⟼ x^{- N})}{d_{ℂ} x} = (x \in (ℂ ∖ \{0\}) ⟼ -N x^{- N - 1})$
80		ax-1cn	$⊢ 1 \in ℂ$
81		dvrec	$⊢ 1 \in ℂ \to \frac{d (y \in (ℂ ∖ \{0\})⟼ \frac{1}{y})}{d_{ℂ} y} = (y \in (ℂ ∖ \{0\}) ⟼ - \frac{1}{y^{2}})$
82	80 81	mp1i	$⊢ (N \in ℝ \land - N \in ℕ) \to \frac{d (y \in (ℂ ∖ \{0\})⟼ \frac{1}{y})}{d_{ℂ} y} = (y \in (ℂ ∖ \{0\}) ⟼ - \frac{1}{y^{2}})$
83		oveq2	$⊢ y = x^{- N} \to \frac{1}{y} = \frac{1}{x^{- N}}$
84		oveq1	$⊢ y = x^{- N} \to y^{2} = {(x^{- N})}^{2}$
85	84	oveq2d	$⊢ y = x^{- N} \to \frac{1}{y^{2}} = \frac{1}{{(x^{- N})}^{2}}$
86	85	negeqd	$⊢ y = x^{- N} \to - \frac{1}{y^{2}} = - \frac{1}{{(x^{- N})}^{2}}$
87	53 53 61 63 68 70 79 82 83 86	dvmptco	$⊢ (N \in ℝ \land - N \in ℕ) \to \frac{d (x \in (ℂ ∖ \{0\})⟼ \frac{1}{x^{- N}})}{d_{ℂ} x} = (x \in (ℂ ∖ \{0\}) ⟼ (- \frac{1}{{(x^{- N})}^{2}}) -N x^{- N - 1})$
88		2z	$⊢ 2 \in ℤ$
89	88	a1i	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to 2 \in ℤ$
90		expmulz	$⊢ ((x \in ℂ \land x \neq 0) \land (- N \in ℤ \land 2 \in ℤ)) \to x^{-N \cdot 2} = {(x^{- N})}^{2}$
91	44 55 57 89 90	syl22anc	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{-N \cdot 2} = {(x^{- N})}^{2}$
92	91	eqcomd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to {(x^{- N})}^{2} = x^{-N \cdot 2}$
93	92	oveq2d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to \frac{1}{{(x^{- N})}^{2}} = \frac{1}{x^{-N \cdot 2}}$
94	93	negeqd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - \frac{1}{{(x^{- N})}^{2}} = - \frac{1}{x^{-N \cdot 2}}$
95		peano2zm	$⊢ - N \in ℤ \to - N - 1 \in ℤ$
96	57 95	syl	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N - 1 \in ℤ$
97	44 55 96	expclzd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{- N - 1} \in ℂ$
98	46 97	mulneg1d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N x^{- N - 1} = - N x^{- N - 1}$
99	94 98	oveq12d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to (- \frac{1}{{(x^{- N})}^{2}}) -N x^{- N - 1} = (- \frac{1}{x^{-N \cdot 2}}) (- N x^{- N - 1})$
100		zmulcl	$⊢ (- N \in ℤ \land 2 \in ℤ) \to -N \cdot 2 \in ℤ$
101	57 88 100	sylancl	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N \cdot 2 \in ℤ$
102	44 55 101	expclzd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{-N \cdot 2} \in ℂ$
103	44 55 101	expne0d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{-N \cdot 2} \neq 0$
104	102 103	reccld	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to \frac{1}{x^{-N \cdot 2}} \in ℂ$
105	46 97	mulcld	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to N x^{- N - 1} \in ℂ$
106	104 105	mul2negd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to (- \frac{1}{x^{-N \cdot 2}}) (- N x^{- N - 1}) = (\frac{1}{x^{-N \cdot 2}}) N x^{- N - 1}$
107	104 46 97	mul12d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to (\frac{1}{x^{-N \cdot 2}}) N x^{- N - 1} = N (\frac{1}{x^{-N \cdot 2}}) x^{- N - 1}$
108	44 55 101 96	expsubd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{-N - 1 - -N \cdot 2} = \frac{x^{- N - 1}}{x^{-N \cdot 2}}$
109		nncn	$⊢ - N \in ℕ \to - N \in ℂ$
110	109	ad2antlr	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N \in ℂ$
111	80	a1i	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to 1 \in ℂ$
112	101	zcnd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N \cdot 2 \in ℂ$
113	110 111 112	sub32d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N - 1 - -N \cdot 2 = -N - -N \cdot 2 - 1$
114	110	times2d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N \cdot 2 = - N + -N$
115	110 46	negsubd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N + -N = - N - N$
116	114 115	eqtrd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N \cdot 2 = - N - N$
117	116	oveq2d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N - -N \cdot 2 = - N - (- N - N)$
118	110 46	nncand	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N - (- N - N) = N$
119	117 118	eqtrd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N - -N \cdot 2 = N$
120	119	oveq1d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N - -N \cdot 2 - 1 = N - 1$
121	113 120	eqtrd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N - 1 - -N \cdot 2 = N - 1$
122	121	oveq2d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{-N - 1 - -N \cdot 2} = x^{N - 1}$
123	97 102 103	divrec2d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to \frac{x^{- N - 1}}{x^{-N \cdot 2}} = (\frac{1}{x^{-N \cdot 2}}) x^{- N - 1}$
124	108 122 123	3eqtr3rd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to (\frac{1}{x^{-N \cdot 2}}) x^{- N - 1} = x^{N - 1}$
125	124	oveq2d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to N (\frac{1}{x^{-N \cdot 2}}) x^{- N - 1} = N x^{N - 1}$
126	107 125	eqtrd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to (\frac{1}{x^{-N \cdot 2}}) N x^{- N - 1} = N x^{N - 1}$
127	99 106 126	3eqtrd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to (- \frac{1}{{(x^{- N})}^{2}}) -N x^{- N - 1} = N x^{N - 1}$
128	127	mpteq2dva	$⊢ (N \in ℝ \land - N \in ℕ) \to (x \in (ℂ ∖ \{0\}) ⟼ (- \frac{1}{{(x^{- N})}^{2}}) -N x^{- N - 1}) = (x \in (ℂ ∖ \{0\}) ⟼ N x^{N - 1})$
129	52 87 128	3eqtrd	$⊢ (N \in ℝ \land - N \in ℕ) \to \frac{d (x \in (ℂ ∖ \{0\})⟼ x^{N})}{d_{ℂ} x} = (x \in (ℂ ∖ \{0\}) ⟼ N x^{N - 1})$
130	42 129	jaoi	$⊢ (N \in ℕ_{0} \lor (N \in ℝ \land - N \in ℕ)) \to \frac{d (x \in (ℂ ∖ \{0\})⟼ x^{N})}{d_{ℂ} x} = (x \in (ℂ ∖ \{0\}) ⟼ N x^{N - 1})$
131	1 130	sylbi	$⊢ N \in ℤ \to \frac{d (x \in (ℂ ∖ \{0\})⟼ x^{N})}{d_{ℂ} x} = (x \in (ℂ ∖ \{0\}) ⟼ N x^{N - 1})$

Metamath Proof Explorer

Theorem dvexp3

Proof