This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ‘ 𝑥 ) ) ) )