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

Metamath Proof Explorer

Theorem sin2t

Description: Double-angle formula for sine. (Contributed by Paul Chapman, 17-Jan-2008)

Ref Expression
Assertion sin2t ( 𝐴 ∈ ℂ → ( sin ‘ ( 2 · 𝐴 ) ) = ( 2 · ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 2times ⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
2 1 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( 2 · 𝐴 ) ) = ( sin ‘ ( 𝐴 + 𝐴 ) ) )
3 coscl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
4 sincl ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
5 3 4 mulcomd ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐴 ) ) = ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) )
6 5 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐴 ) ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) + ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) ) )
7 sinadd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( sin ‘ ( 𝐴 + 𝐴 ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐴 ) ) ) )
8 7 anidms ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( 𝐴 + 𝐴 ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) + ( ( cos ‘ 𝐴 ) · ( sin ‘ 𝐴 ) ) ) )
9 4 3 mulcld ⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) ∈ ℂ )
10 9 2timesd ⊢ ( 𝐴 ∈ ℂ → ( 2 · ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) ) = ( ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) + ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) ) )
11 6 8 10 3eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( 𝐴 + 𝐴 ) ) = ( 2 · ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) ) )
12 2 11 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( 2 · 𝐴 ) ) = ( 2 · ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) ) )