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