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		simpr	$⊢ ((N \in ℝ \land - N \in ℕ) \land y \in (ℂ ∖ \{0\})) \to y \in (ℂ ∖ \{0\})$
59		eldifsn	$⊢ y \in (ℂ ∖ \{0\}) \leftrightarrow (y \in ℂ \land y \neq 0)$
60	58 59	sylib	$⊢ ((N \in ℝ \land - N \in ℕ) \land y \in (ℂ ∖ \{0\})) \to (y \in ℂ \land y \neq 0)$
61		reccl	$⊢ (y \in ℂ \land y \neq 0) \to \frac{1}{y} \in ℂ$
62	60 61	syl	$⊢ ((N \in ℝ \land - N \in ℕ) \land y \in (ℂ ∖ \{0\})) \to \frac{1}{y} \in ℂ$
63		negex	$⊢ - \frac{1}{y^{2}} \in V$
64	63	a1i	$⊢ ((N \in ℝ \land - N \in ℕ) \land y \in (ℂ ∖ \{0\})) \to - \frac{1}{y^{2}} \in V$
65		simpr	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in ℂ) \to x \in ℂ$
66	41	ad2antlr	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in ℂ) \to - N \in ℕ_{0}$
67	65 66	expcld	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in ℂ) \to x^{- N} \in ℂ$
68	56	a1i	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in ℂ) \to -N x^{- N - 1} \in V$
69		dvexp	$⊢ - N \in ℕ \to \frac{d (x \in ℂ⟼ x^{- N})}{d_{ℂ} x} = (x \in ℂ ⟼ -N x^{- N - 1})$
70	69	adantl	$⊢ (N \in ℝ \land - N \in ℕ) \to \frac{d (x \in ℂ⟼ x^{- N})}{d_{ℂ} x} = (x \in ℂ ⟼ -N x^{- N - 1})$
71		difssd	$⊢ (N \in ℝ \land - N \in ℕ) \to ℂ ∖ \{0\} \subseteq ℂ$
72	15	a1i	$⊢ (N \in ℝ \land - N \in ℕ) \to ℂ ∖ \{0\} \in TopOpen (ℂ_{fld})$
73	47 67 68 70 71 14 12 72	dvmptres	$⊢ (N \in ℝ \land - N \in ℕ) \to \frac{d (x \in (ℂ ∖ \{0\})⟼ x^{- N})}{d_{ℂ} x} = (x \in (ℂ ∖ \{0\}) ⟼ -N x^{- N - 1})$
74		ax-1cn	$⊢ 1 \in ℂ$
75		dvrec	$⊢ 1 \in ℂ \to \frac{d (y \in (ℂ ∖ \{0\})⟼ \frac{1}{y})}{d_{ℂ} y} = (y \in (ℂ ∖ \{0\}) ⟼ - \frac{1}{y^{2}})$
76	74 75	mp1i	$⊢ (N \in ℝ \land - N \in ℕ) \to \frac{d (y \in (ℂ ∖ \{0\})⟼ \frac{1}{y})}{d_{ℂ} y} = (y \in (ℂ ∖ \{0\}) ⟼ - \frac{1}{y^{2}})$
77		oveq2	$⊢ y = x^{- N} \to \frac{1}{y} = \frac{1}{x^{- N}}$
78		oveq1	$⊢ y = x^{- N} \to y^{2} = {(x^{- N})}^{2}$
79	78	oveq2d	$⊢ y = x^{- N} \to \frac{1}{y^{2}} = \frac{1}{{(x^{- N})}^{2}}$
80	79	negeqd	$⊢ y = x^{- N} \to - \frac{1}{y^{2}} = - \frac{1}{{(x^{- N})}^{2}}$
81	47 47 55 57 62 64 73 76 77 80	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})$
82		2z	$⊢ 2 \in ℤ$
83	82	a1i	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to 2 \in ℤ$
84		expmulz	$⊢ ((x \in ℂ \land x \neq 0) \land (- N \in ℤ \land 2 \in ℤ)) \to x^{-N \cdot 2} = {(x^{- N})}^{2}$
85	38 49 51 83 84	syl22anc	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{-N \cdot 2} = {(x^{- N})}^{2}$
86	85	eqcomd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to {(x^{- N})}^{2} = x^{-N \cdot 2}$
87	86	oveq2d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to \frac{1}{{(x^{- N})}^{2}} = \frac{1}{x^{-N \cdot 2}}$
88	87	negeqd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - \frac{1}{{(x^{- N})}^{2}} = - \frac{1}{x^{-N \cdot 2}}$
89		peano2zm	$⊢ - N \in ℤ \to - N - 1 \in ℤ$
90	51 89	syl	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N - 1 \in ℤ$
91	38 49 90	expclzd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{- N - 1} \in ℂ$
92	40 91	mulneg1d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N x^{- N - 1} = - N x^{- N - 1}$
93	88 92	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})$
94		zmulcl	$⊢ (- N \in ℤ \land 2 \in ℤ) \to -N \cdot 2 \in ℤ$
95	51 82 94	sylancl	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N \cdot 2 \in ℤ$
96	38 49 95	expclzd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{-N \cdot 2} \in ℂ$
97	38 49 95	expne0d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{-N \cdot 2} \neq 0$
98	96 97	reccld	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to \frac{1}{x^{-N \cdot 2}} \in ℂ$
99	40 91	mulcld	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to N x^{- N - 1} \in ℂ$
100	98 99	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}$
101	98 40 91	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}$
102	38 49 95 90	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}}$
103		nncn	$⊢ - N \in ℕ \to - N \in ℂ$
104	103	ad2antlr	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N \in ℂ$
105	74	a1i	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to 1 \in ℂ$
106	95	zcnd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N \cdot 2 \in ℂ$
107	104 105 106	sub32d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N - 1 - -N \cdot 2 = -N - -N \cdot 2 - 1$
108	104	times2d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N \cdot 2 = - N + -N$
109	104 40	negsubd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N + -N = - N - N$
110	108 109	eqtrd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N \cdot 2 = - N - N$
111	110	oveq2d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N - -N \cdot 2 = - N - (- N - N)$
112	104 40	nncand	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N - (- N - N) = N$
113	111 112	eqtrd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to - N - -N \cdot 2 = N$
114	113	oveq1d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N - -N \cdot 2 - 1 = N - 1$
115	107 114	eqtrd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to -N - 1 - -N \cdot 2 = N - 1$
116	115	oveq2d	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to x^{-N - 1 - -N \cdot 2} = x^{N - 1}$
117	91 96 97	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}$
118	102 116 117	3eqtr3rd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to (\frac{1}{x^{-N \cdot 2}}) x^{- N - 1} = x^{N - 1}$
119	118	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}$
120	101 119	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}$
121	93 100 120	3eqtrd	$⊢ ((N \in ℝ \land - N \in ℕ) \land x \in (ℂ ∖ \{0\})) \to (- \frac{1}{{(x^{- N})}^{2}}) -N x^{- N - 1} = N x^{N - 1}$
122	121	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})$
123	46 81 122	3eqtrd	$⊢ (N \in ℝ \land - N \in ℕ) \to \frac{d (x \in (ℂ ∖ \{0\})⟼ x^{N})}{d_{ℂ} x} = (x \in (ℂ ∖ \{0\}) ⟼ N x^{N - 1})$
124	36 123	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})$
125	1 124	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