Metamath Proof Explorer

Theorem dvsinexp

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

Ref Expression
Hypothesis dvsinexp.5 ⊢ φ → N ∈ ℕ
Assertion dvsinexp ⊢ φ → dx ∈ ℂ sin ⁡ x N d ℂ x = x ∈ ℂ ⟼ N ⁢ sin ⁡ x N − 1 ⁢ cos ⁡ x

Proof

Step Hyp Ref Expression
1 dvsinexp.5 ⊢ φ → N ∈ ℕ
2 cnelprrecn ⊢ ℂ ∈ ℝ ℂ
3 2 a1i ⊢ φ → ℂ ∈ ℝ ℂ
4 sinf ⊢ sin : ℂ ⟶ ℂ
5 4 a1i ⊢ φ → sin : ℂ ⟶ ℂ
6 5 ffvelrnda ⊢ φ ∧ x ∈ ℂ → sin ⁡ x ∈ ℂ
7 cosf ⊢ cos : ℂ ⟶ ℂ
8 7 a1i ⊢ φ → cos : ℂ ⟶ ℂ
9 8 ffvelrnda ⊢ φ ∧ x ∈ ℂ → cos ⁡ x ∈ ℂ
10 simpr ⊢ φ ∧ y ∈ ℂ → y ∈ ℂ
11 1 nnnn0d ⊢ φ → N ∈ ℕ 0
12 11 adantr ⊢ φ ∧ y ∈ ℂ → N ∈ ℕ 0
13 10 12 expcld ⊢ φ ∧ y ∈ ℂ → y N ∈ ℂ
14 1 nncnd ⊢ φ → N ∈ ℂ
15 14 adantr ⊢ φ ∧ y ∈ ℂ → N ∈ ℂ
16 nnm1nn0 ⊢ N ∈ ℕ → N − 1 ∈ ℕ 0
17 1 16 syl ⊢ φ → N − 1 ∈ ℕ 0
18 17 adantr ⊢ φ ∧ y ∈ ℂ → N − 1 ∈ ℕ 0
19 10 18 expcld ⊢ φ ∧ y ∈ ℂ → y N − 1 ∈ ℂ
20 15 19 mulcld ⊢ φ ∧ y ∈ ℂ → N ⁢ y N − 1 ∈ ℂ
21 dvsin ⊢ ℂ D sin = cos
22 5 feqmptd ⊢ φ → sin = x ∈ ℂ ⟼ sin ⁡ x
23 22 oveq2d ⊢ φ → ℂ D sin = dx ∈ ℂ sin ⁡ x d ℂ x
24 8 feqmptd ⊢ φ → cos = x ∈ ℂ ⟼ cos ⁡ x
25 21 23 24 3eqtr3a ⊢ φ → dx ∈ ℂ sin ⁡ x d ℂ x = x ∈ ℂ ⟼ cos ⁡ x
26 dvexp ⊢ N ∈ ℕ → dy ∈ ℂ y N d ℂ y = y ∈ ℂ ⟼ N ⁢ y N − 1
27 1 26 syl ⊢ φ → dy ∈ ℂ y N d ℂ y = y ∈ ℂ ⟼ N ⁢ y N − 1
28 oveq1 ⊢ y = sin ⁡ x → y N = sin ⁡ x N
29 oveq1 ⊢ y = sin ⁡ x → y N − 1 = sin ⁡ x N − 1
30 29 oveq2d ⊢ y = sin ⁡ x → N ⁢ y N − 1 = N ⁢ sin ⁡ x N − 1
31 3 3 6 9 13 20 25 27 28 30 dvmptco ⊢ φ → dx ∈ ℂ sin ⁡ x N d ℂ x = x ∈ ℂ ⟼ N ⁢ sin ⁡ x N − 1 ⁢ cos ⁡ x