Metamath Proof Explorer


Theorem cos2tsin

Description: Double-angle formula for cosine in terms of sine. (Contributed by NM, 12-Sep-2008)

Ref Expression
Assertion cos2tsin ( 𝐴 ∈ ℂ → ( cos ‘ ( 2 · 𝐴 ) ) = ( 1 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) )

Proof

Step Hyp Ref Expression
1 cos2t ( 𝐴 ∈ ℂ → ( cos ‘ ( 2 · 𝐴 ) ) = ( ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) − 1 ) )
2 2cn 2 ∈ ℂ
3 sincl ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
4 3 sqcld ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
5 coscl ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
6 5 sqcld ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
7 adddi ( ( 2 ∈ ℂ ∧ ( ( sin ‘ 𝐴 ) ↑ 2 ) ∈ ℂ ∧ ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℂ ) → ( 2 · ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) = ( ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) + ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) )
8 2 4 6 7 mp3an2i ( 𝐴 ∈ ℂ → ( 2 · ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) = ( ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) + ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) )
9 sincossq ( 𝐴 ∈ ℂ → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = 1 )
10 9 oveq2d ( 𝐴 ∈ ℂ → ( 2 · ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) = ( 2 · 1 ) )
11 8 10 eqtr3d ( 𝐴 ∈ ℂ → ( ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) + ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) = ( 2 · 1 ) )
12 2t1e2 ( 2 · 1 ) = 2
13 11 12 eqtrdi ( 𝐴 ∈ ℂ → ( ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) + ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) = 2 )
14 mulcl ( ( 2 ∈ ℂ ∧ ( ( sin ‘ 𝐴 ) ↑ 2 ) ∈ ℂ ) → ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ )
15 2 4 14 sylancr ( 𝐴 ∈ ℂ → ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ )
16 mulcl ( ( 2 ∈ ℂ ∧ ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℂ ) → ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ )
17 2 6 16 sylancr ( 𝐴 ∈ ℂ → ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ )
18 subadd ( ( 2 ∈ ℂ ∧ ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ ∧ ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ ) → ( ( 2 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) = ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ↔ ( ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) + ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) = 2 ) )
19 2 15 17 18 mp3an2i ( 𝐴 ∈ ℂ → ( ( 2 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) = ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ↔ ( ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) + ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) = 2 ) )
20 13 19 mpbird ( 𝐴 ∈ ℂ → ( 2 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) = ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) )
21 20 oveq1d ( 𝐴 ∈ ℂ → ( ( 2 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) − 1 ) = ( ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) − 1 ) )
22 ax-1cn 1 ∈ ℂ
23 sub32 ( ( 2 ∈ ℂ ∧ ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 2 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) − 1 ) = ( ( 2 − 1 ) − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) )
24 2 22 23 mp3an13 ( ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ∈ ℂ → ( ( 2 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) − 1 ) = ( ( 2 − 1 ) − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) )
25 15 24 syl ( 𝐴 ∈ ℂ → ( ( 2 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) − 1 ) = ( ( 2 − 1 ) − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) )
26 2m1e1 ( 2 − 1 ) = 1
27 26 oveq1i ( ( 2 − 1 ) − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) = ( 1 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) )
28 25 27 eqtrdi ( 𝐴 ∈ ℂ → ( ( 2 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) − 1 ) = ( 1 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) )
29 1 21 28 3eqtr2d ( 𝐴 ∈ ℂ → ( cos ‘ ( 2 · 𝐴 ) ) = ( 1 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) )