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		cnn0opn	$⊢ ℂ ∖ \{0\} \in TopOpen (ℂ_{fld})$
16	15	a1i	$⊢ N \in ℕ_{0} \to ℂ ∖ \{0\} \in TopOpen (ℂ_{fld})$
17	3 5 9 10 11 14 12 16	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}))$
18		ifid	$⊢ if (N = 0, N x^{N - 1}, N x^{N - 1}) = N x^{N - 1}$
19		id	$⊢ N = 0 \to N = 0$
20		oveq1	$⊢ N = 0 \to N - 1 = 0 - 1$
21	20	oveq2d	$⊢ N = 0 \to x^{N - 1} = x^{0 - 1}$
22	19 21	oveq12d	$⊢ N = 0 \to N x^{N - 1} = 0 \cdot x^{0 - 1}$
23		eldifsn	$⊢ x \in (ℂ ∖ \{0\}) \leftrightarrow (x \in ℂ \land x \neq 0)$
24		0z	$⊢ 0 \in ℤ$
25		peano2zm	$⊢ 0 \in ℤ \to 0 - 1 \in ℤ$
26	24 25	ax-mp	$⊢ 0 - 1 \in ℤ$
27		expclz	$⊢ (x \in ℂ \land x \neq 0 \land 0 - 1 \in ℤ) \to x^{0 - 1} \in ℂ$
28	26 27	mp3an3	$⊢ (x \in ℂ \land x \neq 0) \to x^{0 - 1} \in ℂ$
29	23 28	sylbi	$⊢ x \in (ℂ ∖ \{0\}) \to x^{0 - 1} \in ℂ$
30	29	adantl	$⊢ (N \in ℕ_{0} \land x \in (ℂ ∖ \{0\})) \to x^{0 - 1} \in ℂ$
31	30	mul02d	$⊢ (N \in ℕ_{0} \land x \in (ℂ ∖ \{0\})) \to 0 \cdot x^{0 - 1} = 0$
32	22 31	sylan9eqr	$⊢ ((N \in ℕ_{0} \land x \in (ℂ ∖ \{0\})) \land N = 0) \to N x^{N - 1} = 0$
33	32	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})$
34	18 33	eqtr3id	$⊢ (N \in ℕ_{0} \land x \in (ℂ ∖ \{0\})) \to N x^{N - 1} = if (N = 0, 0, N x^{N - 1})$
35	34	mpteq2dva	$⊢ N \in ℕ_{0} \to (x \in (ℂ ∖ \{0\}) ⟼ N x^{N - 1}) = (x \in (ℂ ∖ \{0\}) ⟼ if (N = 0, 0, N x^{N - 1}))$
36	17 35	eqtr4d	$⊢ N \in ℕ_{0} \to \frac{d (x \in (ℂ ∖ \{0\})⟼ x^{N})}{d_{ℂ} x} = (x \in (ℂ ∖ \{0\}) ⟼ N x^{N - 1})$
37		eldifi	$⊢ x \in (ℂ ∖ \{0\}) \to x \in ℂ$
38	37	adantl	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x \in ℂ$
39		simpll	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to N \in ℝ$
40	39	recnd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to N \in ℂ$
41		nnnn0	$⊢ - N \in ℕ \to - N \in ℕ_{0}$
42	41	ad2antlr	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N \in ℕ_{0}$
43		expneg2	$⊢ (x \in ℂ \land N \in ℂ \land - N \in ℕ_{0}) \to x^{N} = \frac{1}{x^{- N}}$
44	38 40 42 43	syl3anc	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{N} = \frac{1}{x^{- N}}$
45	44	mpteq2dva	$⊢ (N \in ℝ \land - N \in ℕ) \to (x \in (ℂ ∖ \{0\}) ⟼ x^{N}) = (x \in (ℂ ∖ \{0\}) ⟼ \frac{1}{x^{- N}})$
46	45	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}$
47	2	a1i	$⊢ (N \in ℝ \land - N \in ℕ) \to ℂ \in \{ℝ, ℂ\}$
48		eldifsni	$⊢ x \in (ℂ ∖ \{0\}) \to x \neq 0$
49	48	adantl	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x \neq 0$
50		nnz	$⊢ - N \in ℕ \to - N \in ℤ$
51	50	ad2antlr	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N \in ℤ$
52	38 49 51	expclzd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{- N} \in ℂ$
53	38 49 51	expne0d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{- N} \neq 0$
54		eldifsn	$⊢ x^{- N} \in (ℂ ∖ \{0\}) \leftrightarrow (x^{- N} \in ℂ \land x^{- N} \neq 0)$
55	52 53 54	sylanbrc	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{- N} \in (ℂ ∖ \{0\})$
56		ovex	$⊢ -N x^{- N - 1} \in V$
57	56	a1i	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N x^{- N - 1} \in V$
58		eldifsn	$⊢ y \in (ℂ ∖ \{0\}) \leftrightarrow (y \in ℂ \land y \neq 0)$
59	58	bilani	$⊢ ((N \in ℝ \land - N \in ℕ) \land y \in (ℂ ∖ \{0\})) \to (y \in ℂ \land y \neq 0)$
60		reccl	$⊢ (y \in ℂ \land y \neq 0) \to \frac{1}{y} \in ℂ$
61	59 60	syl	$⊢ ((N \in ℝ \land - N \in ℕ) \land y \in (ℂ ∖ \{0\})) \to \frac{1}{y} \in ℂ$
62		negex	$⊢ - \frac{1}{y^{2}} \in V$
63	62	a1i	$⊢ ((N \in ℝ \land - N \in ℕ) \land y \in (ℂ ∖ \{0\})) \to - \frac{1}{y^{2}} \in V$
64		simpr	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in ℂ) \to x \in ℂ$
65	41	ad2antlr	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in ℂ) \to - N \in ℕ_{0}$
66	64 65	expcld	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in ℂ) \to x^{- N} \in ℂ$
67	56	a1i	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in ℂ) \to -N x^{- N - 1} \in V$
68		dvexp	$⊢ - N \in ℕ \to \frac{d (x \in ℂ⟼ x^{- N})}{d_{ℂ} x} = (x \in ℂ ⟼ -N x^{- N - 1})$
69	68	adantl	$⊢ (N \in ℝ \land - N \in ℕ) \to \frac{d (x \in ℂ⟼ x^{- N})}{d_{ℂ} x} = (x \in ℂ ⟼ -N x^{- N - 1})$
70		difssd	$⊢ (N \in ℝ \land - N \in ℕ) \to ℂ ∖ \{0\} \subseteq ℂ$
71	15	a1i	$⊢ (N \in ℝ \land - N \in ℕ) \to ℂ ∖ \{0\} \in TopOpen (ℂ_{fld})$
72	47 66 67 69 70 14 12 71	dvmptres	$⊢ (N \in ℝ \land - N \in ℕ) \to \frac{d (x \in (ℂ ∖ \{0\})⟼ x^{- N})}{d_{ℂ} x} = (x \in (ℂ ∖ \{0\}) ⟼ -N x^{- N - 1})$
73		ax-1cn	$⊢ 1 \in ℂ$
74		dvrec	$⊢ 1 \in ℂ \to \frac{d (y \in (ℂ ∖ \{0\})⟼ \frac{1}{y})}{d_{ℂ} y} = (y \in (ℂ ∖ \{0\}) ⟼ - \frac{1}{y^{2}})$
75	73 74	mp1i	$⊢ (N \in ℝ \land - N \in ℕ) \to \frac{d (y \in (ℂ ∖ \{0\})⟼ \frac{1}{y})}{d_{ℂ} y} = (y \in (ℂ ∖ \{0\}) ⟼ - \frac{1}{y^{2}})$
76		oveq2	$⊢ y = x^{- N} \to \frac{1}{y} = \frac{1}{x^{- N}}$
77		oveq1	$⊢ y = x^{- N} \to y^{2} = {(x^{- N})}^{2}$
78	77	oveq2d	$⊢ y = x^{- N} \to \frac{1}{y^{2}} = \frac{1}{{(x^{- N})}^{2}}$
79	78	negeqd	$⊢ y = x^{- N} \to - \frac{1}{y^{2}} = - \frac{1}{{(x^{- N})}^{2}}$
80	47 47 55 57 61 63 72 75 76 79	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})$
81		2z	$⊢ 2 \in ℤ$
82	81	a1i	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to 2 \in ℤ$
83		expmulz	$⊢ ((x \in ℂ \land x \neq 0) \land (- N \in ℤ \land 2 \in ℤ)) \to x^{-N \cdot 2} = {(x^{- N})}^{2}$
84	38 49 51 82 83	syl22anc	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{-N \cdot 2} = {(x^{- N})}^{2}$
85	84	eqcomd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to {(x^{- N})}^{2} = x^{-N \cdot 2}$
86	85	oveq2d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to \frac{1}{{(x^{- N})}^{2}} = \frac{1}{x^{-N \cdot 2}}$
87	86	negeqd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - \frac{1}{{(x^{- N})}^{2}} = - \frac{1}{x^{-N \cdot 2}}$
88		peano2zm	$⊢ - N \in ℤ \to - N - 1 \in ℤ$
89	51 88	syl	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N - 1 \in ℤ$
90	38 49 89	expclzd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{- N - 1} \in ℂ$
91	40 90	mulneg1d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N x^{- N - 1} = - N x^{- N - 1}$
92	87 91	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})$
93		zmulcl	$⊢ (- N \in ℤ \land 2 \in ℤ) \to -N \cdot 2 \in ℤ$
94	51 81 93	sylancl	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N \cdot 2 \in ℤ$
95	38 49 94	expclzd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{-N \cdot 2} \in ℂ$
96	38 49 94	expne0d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{-N \cdot 2} \neq 0$
97	95 96	reccld	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to \frac{1}{x^{-N \cdot 2}} \in ℂ$
98	40 90	mulcld	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to N x^{- N - 1} \in ℂ$
99	97 98	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}$
100	97 40 90	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}$
101	38 49 94 89	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}}$
102		nncn	$⊢ - N \in ℕ \to - N \in ℂ$
103	102	ad2antlr	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N \in ℂ$
104	73	a1i	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to 1 \in ℂ$
105	94	zcnd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N \cdot 2 \in ℂ$
106	103 104 105	sub32d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N - 1 - -N \cdot 2 = -N - -N \cdot 2 - 1$
107	103	times2d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N \cdot 2 = - N + -N$
108	103 40	negsubd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N + -N = - N - N$
109	107 108	eqtrd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N \cdot 2 = - N - N$
110	109	oveq2d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N - -N \cdot 2 = - N - (- N - N)$
111	103 40	nncand	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N - (- N - N) = N$
112	110 111	eqtrd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N - -N \cdot 2 = N$
113	112	oveq1d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N - -N \cdot 2 - 1 = N - 1$
114	106 113	eqtrd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N - 1 - -N \cdot 2 = N - 1$
115	114	oveq2d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{-N - 1 - -N \cdot 2} = x^{N - 1}$
116	90 95 96	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}$
117	101 115 116	3eqtr3rd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to (\frac{1}{x^{-N \cdot 2}}) x^{- N - 1} = x^{N - 1}$
118	117	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}$
119	100 118	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}$
120	92 99 119	3eqtrd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to (- \frac{1}{{(x^{- N})}^{2}}) -N x^{- N - 1} = N x^{N - 1}$
121	120	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})$
122	46 80 121	3eqtrd	$⊢ (N \in ℝ \land - N \in ℕ) \to \frac{d (x \in (ℂ ∖ \{0\})⟼ x^{N})}{d_{ℂ} x} = (x \in (ℂ ∖ \{0\}) ⟼ N x^{N - 1})$
123	36 122	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})$
124	1 123	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