# Metamath Proof Explorer

## Theorem cos2t

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

Ref Expression
Assertion cos2t ${⊢}{A}\in ℂ\to \mathrm{cos}2{A}=2{\mathrm{cos}{A}}^{2}-1$

### Proof

Step Hyp Ref Expression
1 coscl ${⊢}{A}\in ℂ\to \mathrm{cos}{A}\in ℂ$
2 1 sqcld ${⊢}{A}\in ℂ\to {\mathrm{cos}{A}}^{2}\in ℂ$
3 ax-1cn ${⊢}1\in ℂ$
4 subsub3 ${⊢}\left({\mathrm{cos}{A}}^{2}\in ℂ\wedge 1\in ℂ\wedge {\mathrm{cos}{A}}^{2}\in ℂ\right)\to {\mathrm{cos}{A}}^{2}-\left(1-{\mathrm{cos}{A}}^{2}\right)={\mathrm{cos}{A}}^{2}+{\mathrm{cos}{A}}^{2}-1$
5 3 4 mp3an2 ${⊢}\left({\mathrm{cos}{A}}^{2}\in ℂ\wedge {\mathrm{cos}{A}}^{2}\in ℂ\right)\to {\mathrm{cos}{A}}^{2}-\left(1-{\mathrm{cos}{A}}^{2}\right)={\mathrm{cos}{A}}^{2}+{\mathrm{cos}{A}}^{2}-1$
6 2 2 5 syl2anc ${⊢}{A}\in ℂ\to {\mathrm{cos}{A}}^{2}-\left(1-{\mathrm{cos}{A}}^{2}\right)={\mathrm{cos}{A}}^{2}+{\mathrm{cos}{A}}^{2}-1$
7 cosadd ${⊢}\left({A}\in ℂ\wedge {A}\in ℂ\right)\to \mathrm{cos}\left({A}+{A}\right)=\mathrm{cos}{A}\mathrm{cos}{A}-\mathrm{sin}{A}\mathrm{sin}{A}$
8 7 anidms ${⊢}{A}\in ℂ\to \mathrm{cos}\left({A}+{A}\right)=\mathrm{cos}{A}\mathrm{cos}{A}-\mathrm{sin}{A}\mathrm{sin}{A}$
9 2times ${⊢}{A}\in ℂ\to 2{A}={A}+{A}$
10 9 fveq2d ${⊢}{A}\in ℂ\to \mathrm{cos}2{A}=\mathrm{cos}\left({A}+{A}\right)$
11 1 sqvald ${⊢}{A}\in ℂ\to {\mathrm{cos}{A}}^{2}=\mathrm{cos}{A}\mathrm{cos}{A}$
12 sincl ${⊢}{A}\in ℂ\to \mathrm{sin}{A}\in ℂ$
13 12 sqvald ${⊢}{A}\in ℂ\to {\mathrm{sin}{A}}^{2}=\mathrm{sin}{A}\mathrm{sin}{A}$
14 11 13 oveq12d ${⊢}{A}\in ℂ\to {\mathrm{cos}{A}}^{2}-{\mathrm{sin}{A}}^{2}=\mathrm{cos}{A}\mathrm{cos}{A}-\mathrm{sin}{A}\mathrm{sin}{A}$
15 8 10 14 3eqtr4d ${⊢}{A}\in ℂ\to \mathrm{cos}2{A}={\mathrm{cos}{A}}^{2}-{\mathrm{sin}{A}}^{2}$
16 12 sqcld ${⊢}{A}\in ℂ\to {\mathrm{sin}{A}}^{2}\in ℂ$
17 16 2 addcomd ${⊢}{A}\in ℂ\to {\mathrm{sin}{A}}^{2}+{\mathrm{cos}{A}}^{2}={\mathrm{cos}{A}}^{2}+{\mathrm{sin}{A}}^{2}$
18 sincossq ${⊢}{A}\in ℂ\to {\mathrm{sin}{A}}^{2}+{\mathrm{cos}{A}}^{2}=1$
19 17 18 eqtr3d ${⊢}{A}\in ℂ\to {\mathrm{cos}{A}}^{2}+{\mathrm{sin}{A}}^{2}=1$
20 subadd ${⊢}\left(1\in ℂ\wedge {\mathrm{cos}{A}}^{2}\in ℂ\wedge {\mathrm{sin}{A}}^{2}\in ℂ\right)\to \left(1-{\mathrm{cos}{A}}^{2}={\mathrm{sin}{A}}^{2}↔{\mathrm{cos}{A}}^{2}+{\mathrm{sin}{A}}^{2}=1\right)$
21 3 2 16 20 mp3an2i ${⊢}{A}\in ℂ\to \left(1-{\mathrm{cos}{A}}^{2}={\mathrm{sin}{A}}^{2}↔{\mathrm{cos}{A}}^{2}+{\mathrm{sin}{A}}^{2}=1\right)$
22 19 21 mpbird ${⊢}{A}\in ℂ\to 1-{\mathrm{cos}{A}}^{2}={\mathrm{sin}{A}}^{2}$
23 22 oveq2d ${⊢}{A}\in ℂ\to {\mathrm{cos}{A}}^{2}-\left(1-{\mathrm{cos}{A}}^{2}\right)={\mathrm{cos}{A}}^{2}-{\mathrm{sin}{A}}^{2}$
24 15 23 eqtr4d ${⊢}{A}\in ℂ\to \mathrm{cos}2{A}={\mathrm{cos}{A}}^{2}-\left(1-{\mathrm{cos}{A}}^{2}\right)$
25 2 2timesd ${⊢}{A}\in ℂ\to 2{\mathrm{cos}{A}}^{2}={\mathrm{cos}{A}}^{2}+{\mathrm{cos}{A}}^{2}$
26 25 oveq1d ${⊢}{A}\in ℂ\to 2{\mathrm{cos}{A}}^{2}-1={\mathrm{cos}{A}}^{2}+{\mathrm{cos}{A}}^{2}-1$
27 6 24 26 3eqtr4d ${⊢}{A}\in ℂ\to \mathrm{cos}2{A}=2{\mathrm{cos}{A}}^{2}-1$