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