Theorem dvsinexp

Description: The derivative of sin^N . (Contributed by Glauco Siliprandi, 29-Jun-2017)

	Ref	Expression
Hypothesis	dvsinexp.5	$$⊢\phi \to N\in \mathbb{N}$$
Assertion	dvsinexp	$$⊢\phi \to \frac{d\left(x\in ℂ⟼{\sin x}^N\right)}{d_{ℂ}x}=\left(x\in ℂ⟼N{\sin x}^{N-1}\cos x\right)$$

Proof

Step	Hyp	Ref	Expression
1		dvsinexp.5	$$⊢\phi \to N\in \mathbb{N}$$
2		cnelprrecn	$$⊢ℂ\in \left\{ℝ,ℂ\right\}$$
3	2	a1i	$$⊢\phi \to ℂ\in \left\{ℝ,ℂ\right\}$$
4		sinf	$$⊢\sin :ℂ⟶ℂ$$
5	4	a1i	$$⊢\phi \to \sin :ℂ⟶ℂ$$
6	5	ffvelcdmda	$$⊢\left(\phi \wedge x\in ℂ\right)\to \sin x\in ℂ$$
7		cosf	$$⊢\cos :ℂ⟶ℂ$$
8	7	a1i	$$⊢\phi \to \cos :ℂ⟶ℂ$$
9	8	ffvelcdmda	$$⊢\left(\phi \wedge x\in ℂ\right)\to \cos x\in ℂ$$
10		simpr	$$⊢\left(\phi \wedge y\in ℂ\right)\to y\in ℂ$$
11	1	nnnn0d	$$⊢\phi \to N\in {\mathbb{N}}_0$$
12	11	adantr	$$⊢\left(\phi \wedge y\in ℂ\right)\to N\in {\mathbb{N}}_0$$
13	10 12	expcld	$$⊢\left(\phi \wedge y\in ℂ\right)\to y^N\in ℂ$$
14	1	nncnd	$$⊢\phi \to N\in ℂ$$
15	14	adantr	$$⊢\left(\phi \wedge y\in ℂ\right)\to N\in ℂ$$
16		nnm1nn0	$$⊢N\in \mathbb{N}\to N-1\in {\mathbb{N}}_0$$
17	1 16	syl	$$⊢\phi \to N-1\in {\mathbb{N}}_0$$
18	17	adantr	$$⊢\left(\phi \wedge y\in ℂ\right)\to N-1\in {\mathbb{N}}_0$$
19	10 18	expcld	$$⊢\left(\phi \wedge y\in ℂ\right)\to y^{N-1}\in ℂ$$
20	15 19	mulcld	$$⊢\left(\phi \wedge y\in ℂ\right)\to N{y}^{N-1}\in ℂ$$
21		dvsin	$$⊢ℂ\mathrm{D}\sin =\cos$$
22	5	feqmptd	$$⊢\phi \to \sin =\left(x\in ℂ⟼\sin x\right)$$
23	22	oveq2d	$$⊢\phi \to ℂ\mathrm{D}\sin =\frac{d\left(x\in ℂ⟼\sin x\right)}{d_{ℂ}x}$$
24	8	feqmptd	$$⊢\phi \to \cos =\left(x\in ℂ⟼\cos x\right)$$
25	21 23 24	3eqtr3a	$$⊢\phi \to \frac{d\left(x\in ℂ⟼\sin x\right)}{d_{ℂ}x}=\left(x\in ℂ⟼\cos x\right)$$
26		dvexp	$$⊢N\in \mathbb{N}\to \frac{d\left(y\in ℂ⟼y^N\right)}{d_{ℂ}y}=\left(y\in ℂ⟼N{y}^{N-1}\right)$$
27	1 26	syl	$$⊢\phi \to \frac{d\left(y\in ℂ⟼y^N\right)}{d_{ℂ}y}=\left(y\in ℂ⟼N{y}^{N-1}\right)$$
28		oveq1	$$⊢y=\sin x\to y^N={\sin x}^N$$
29		oveq1	$$⊢y=\sin x\to y^{N-1}={\sin x}^{N-1}$$
30	29	oveq2d	$$⊢y=\sin x\to N{y}^{N-1}=N{\sin x}^{N-1}$$
31	3 3 6 9 13 20 25 27 28 30	dvmptco	$$⊢\phi \to \frac{d\left(x\in ℂ⟼{\sin x}^N\right)}{d_{ℂ}x}=\left(x\in ℂ⟼N{\sin x}^{N-1}\cos x\right)$$