Metamath Proof Explorer

Theorem cos2t

Description: Double-angle formula for cosine. (Contributed by Paul Chapman, 24-Jan-2008)

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

Proof

Step Hyp Ref Expression
1 coscl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
2 1 sqcld ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
3 ax-1cn ⊢ 1 ∈ ℂ
4 subsub3 ⊢ ( ( ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℂ ) → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − ( 1 − ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) = ( ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) − 1 ) )
5 3 4 mp3an2 ⊢ ( ( ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℂ ∧ ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℂ ) → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − ( 1 − ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) = ( ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) − 1 ) )
6 2 2 5 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − ( 1 − ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) = ( ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) − 1 ) )
7 cosadd ⊢ ( ( 𝐴 ∈ ℂ ∧ 𝐴 ∈ ℂ ) → ( cos ‘ ( 𝐴 + 𝐴 ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐴 ) ) ) )
8 7 anidms ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 𝐴 + 𝐴 ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐴 ) ) ) )
9 2times ⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) = ( 𝐴 + 𝐴 ) )
10 9 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 2 · 𝐴 ) ) = ( cos ‘ ( 𝐴 + 𝐴 ) ) )
11 1 sqvald ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) ↑ 2 ) = ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) )
12 sincl ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
13 12 sqvald ⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) ↑ 2 ) = ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐴 ) ) )
14 11 13 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = ( ( ( cos ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) − ( ( sin ‘ 𝐴 ) · ( sin ‘ 𝐴 ) ) ) )
15 8 10 14 3eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 2 · 𝐴 ) ) = ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) )
16 12 sqcld ⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
17 16 2 addcomd ⊢ ( 𝐴 ∈ ℂ → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( sin ‘ 𝐴 ) ↑ 2 ) ) )
18 sincossq ⊢ ( 𝐴 ∈ ℂ → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = 1 )
19 17 18 eqtr3d ⊢ ( 𝐴 ∈ ℂ → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = 1 )
20 subadd ⊢ ( ( 1 ∈ ℂ ∧ ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℂ ∧ ( ( sin ‘ 𝐴 ) ↑ 2 ) ∈ ℂ ) → ( ( 1 − ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = ( ( sin ‘ 𝐴 ) ↑ 2 ) ↔ ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = 1 ) )
21 3 2 16 20 mp3an2i ⊢ ( 𝐴 ∈ ℂ → ( ( 1 − ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = ( ( sin ‘ 𝐴 ) ↑ 2 ) ↔ ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( sin ‘ 𝐴 ) ↑ 2 ) ) = 1 ) )
22 19 21 mpbird ⊢ ( 𝐴 ∈ ℂ → ( 1 − ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = ( ( sin ‘ 𝐴 ) ↑ 2 ) )
23 22 oveq2d ⊢ ( 𝐴 ∈ ℂ → ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − ( 1 − ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) = ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) )
24 15 23 eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 2 · 𝐴 ) ) = ( ( ( cos ‘ 𝐴 ) ↑ 2 ) − ( 1 − ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) )
25 2 2timesd ⊢ ( 𝐴 ∈ ℂ → ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) )
26 25 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) − 1 ) = ( ( ( ( cos ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) − 1 ) )
27 6 24 26 3eqtr4d ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 2 · 𝐴 ) ) = ( ( 2 · ( ( cos ‘ 𝐴 ) ↑ 2 ) ) − 1 ) )