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 ⊢ A ∈ ℂ → sin ⁡ 2 ⁢ A = 2 ⁢ sin ⁡ A ⁢ cos ⁡ A

Proof

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