Theorem dvsinexp

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

	Ref	Expression
Hypothesis	dvsinexp.5	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
Assertion	dvsinexp	⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝑁 · ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · ( cos ‘ 𝑥 ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dvsinexp.5	⊢ ( 𝜑 → 𝑁 ∈ ℕ )
2		cnelprrecn	⊢ ℂ ∈ { ℝ , ℂ }
3	2	a1i	⊢ ( 𝜑 → ℂ ∈ { ℝ , ℂ } )
4		sinf	⊢ sin : ℂ ⟶ ℂ
5	4	a1i	⊢ ( 𝜑 → sin : ℂ ⟶ ℂ )
6	5	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( sin ‘ 𝑥 ) ∈ ℂ )
7		cosf	⊢ cos : ℂ ⟶ ℂ
8	7	a1i	⊢ ( 𝜑 → cos : ℂ ⟶ ℂ )
9	8	ffvelcdmda	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℂ ) → ( cos ‘ 𝑥 ) ∈ ℂ )
10		simpr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑦 ∈ ℂ )
11	1	nnnn0d	⊢ ( 𝜑 → 𝑁 ∈ ℕ0 )
12	11	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑁 ∈ ℕ0 )
13	10 12	expcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ 𝑁 ) ∈ ℂ )
14	1	nncnd	⊢ ( 𝜑 → 𝑁 ∈ ℂ )
15	14	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → 𝑁 ∈ ℂ )
16		nnm1nn0	⊢ ( 𝑁 ∈ ℕ → ( 𝑁 − 1 ) ∈ ℕ0 )
17	1 16	syl	⊢ ( 𝜑 → ( 𝑁 − 1 ) ∈ ℕ0 )
18	17	adantr	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑁 − 1 ) ∈ ℕ0 )
19	10 18	expcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑦 ↑ ( 𝑁 − 1 ) ) ∈ ℂ )
20	15 19	mulcld	⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℂ ) → ( 𝑁 · ( 𝑦 ↑ ( 𝑁 − 1 ) ) ) ∈ ℂ )
21		dvsin	⊢ ( ℂ D sin ) = cos
22	5	feqmptd	⊢ ( 𝜑 → sin = ( 𝑥 ∈ ℂ ↦ ( sin ‘ 𝑥 ) ) )
23	22	oveq2d	⊢ ( 𝜑 → ( ℂ D sin ) = ( ℂ D ( 𝑥 ∈ ℂ ↦ ( sin ‘ 𝑥 ) ) ) )
24	8	feqmptd	⊢ ( 𝜑 → cos = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) )
25	21 23 24	3eqtr3a	⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( sin ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( cos ‘ 𝑥 ) ) )
26		dvexp	⊢ ( 𝑁 ∈ ℕ → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑁 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑁 · ( 𝑦 ↑ ( 𝑁 − 1 ) ) ) ) )
27	1 26	syl	⊢ ( 𝜑 → ( ℂ D ( 𝑦 ∈ ℂ ↦ ( 𝑦 ↑ 𝑁 ) ) ) = ( 𝑦 ∈ ℂ ↦ ( 𝑁 · ( 𝑦 ↑ ( 𝑁 − 1 ) ) ) ) )
28		oveq1	⊢ ( 𝑦 = ( sin ‘ 𝑥 ) → ( 𝑦 ↑ 𝑁 ) = ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) )
29		oveq1	⊢ ( 𝑦 = ( sin ‘ 𝑥 ) → ( 𝑦 ↑ ( 𝑁 − 1 ) ) = ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) )
30	29	oveq2d	⊢ ( 𝑦 = ( sin ‘ 𝑥 ) → ( 𝑁 · ( 𝑦 ↑ ( 𝑁 − 1 ) ) ) = ( 𝑁 · ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) )
31	3 3 6 9 13 20 25 27 28 30	dvmptco	⊢ ( 𝜑 → ( ℂ D ( 𝑥 ∈ ℂ ↦ ( ( sin ‘ 𝑥 ) ↑ 𝑁 ) ) ) = ( 𝑥 ∈ ℂ ↦ ( ( 𝑁 · ( ( sin ‘ 𝑥 ) ↑ ( 𝑁 − 1 ) ) ) · ( cos ‘ 𝑥 ) ) ) )