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