Database
REAL AND COMPLEX NUMBERS
Elementary trigonometry
The exponential, sine, and cosine functions
sin2t
Next ⟩
cos2t
Metamath Proof Explorer
Ascii
Unicode
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