Theorem sin3t

Description: Triple-angle formula for sine, in pure sine form. (Contributed by Ender Ting, 16-Mar-2026)

	Ref	Expression
Assertion	sin3t	$$⊢A\in ℂ\to \sin 3A=3\sin A-4{\sin A}^3$$

Proof

Step	Hyp	Ref	Expression
1		df-3	$$⊢3=2+1$$
2	1	oveq1i	$$⊢3A=\left(2+1\right)A$$
3		2cnd	$$⊢A\in ℂ\to 2\in ℂ$$
4		1cnd	$$⊢A\in ℂ\to 1\in ℂ$$
5		id	$$⊢A\in ℂ\to A\in ℂ$$
6	3 4 5	adddird	$$⊢A\in ℂ\to \left(2+1\right)A=2A+1A$$
7	2 6	eqtrid	$$⊢A\in ℂ\to 3A=2A+1A$$
8	7	fveq2d	$$⊢A\in ℂ\to \sin 3A=\sin \left(2A+1A\right)$$
9	3 5	mulcld	$$⊢A\in ℂ\to 2A\in ℂ$$
10	4 5	mulcld	$$⊢A\in ℂ\to 1A\in ℂ$$
11		sinadd	$$⊢\left(2A\in ℂ\wedge 1A\in ℂ\right)\to \sin \left(2A+1A\right)=\sin 2A\cos 1A+\cos 2A\sin 1A$$
12	9 10 11	syl2anc	$$⊢A\in ℂ\to \sin \left(2A+1A\right)=\sin 2A\cos 1A+\cos 2A\sin 1A$$
13		sin2t	$$⊢A\in ℂ\to \sin 2A=2\sin A\cos A$$
14	13	oveq1d	$$⊢A\in ℂ\to \sin 2A\cos 1A=2\sin A\cos A\cos 1A$$
15		sincl	$$⊢A\in ℂ\to \sin A\in ℂ$$
16		coscl	$$⊢A\in ℂ\to \cos A\in ℂ$$
17	15 16	mulcld	$$⊢A\in ℂ\to \sin A\cos A\in ℂ$$
18	10	coscld	$$⊢A\in ℂ\to \cos 1A\in ℂ$$
19	3 17 18	mulassd	$$⊢A\in ℂ\to 2\sin A\cos A\cos 1A=2\sin A\cos A\cos 1A$$
20		mullid	$$⊢A\in ℂ\to 1A=A$$
21	20	fveq2d	$$⊢A\in ℂ\to \cos 1A=\cos A$$
22	21	oveq2d	$$⊢A\in ℂ\to \sin A\cos A\cos 1A=\sin A\cos A\cos A$$
23	15 16 16	mulassd	$$⊢A\in ℂ\to \sin A\cos A\cos A=\sin A\cos A\cos A$$
24	16	sqvald	$$⊢A\in ℂ\to {\cos A}^2=\cos A\cos A$$
25	15	sqcld	$$⊢A\in ℂ\to {\sin A}^2\in ℂ$$
26	16	sqcld	$$⊢A\in ℂ\to {\cos A}^2\in ℂ$$
27		sincossq	$$⊢A\in ℂ\to {\sin A}^2+{\cos A}^2=1$$
28	25 26 27	mvlladdd	$$⊢A\in ℂ\to {\cos A}^2=1-{\sin A}^2$$
29	24 28	eqtr3d	$$⊢A\in ℂ\to \cos A\cos A=1-{\sin A}^2$$
30	29	oveq2d	$$⊢A\in ℂ\to \sin A\cos A\cos A=\sin A\left(1-{\sin A}^2\right)$$
31	22 23 30	3eqtrd	$$⊢A\in ℂ\to \sin A\cos A\cos 1A=\sin A\left(1-{\sin A}^2\right)$$
32	31	oveq2d	$$⊢A\in ℂ\to 2\sin A\cos A\cos 1A=2\sin A\left(1-{\sin A}^2\right)$$
33	15 4 25	subdid	$$⊢A\in ℂ\to \sin A\left(1-{\sin A}^2\right)=\sin A\cdot 1-\sin A{\sin A}^2$$
34	15	mulridd	$$⊢A\in ℂ\to \sin A\cdot 1=\sin A$$
35	1	a1i	$$⊢A\in ℂ\to 3=2+1$$
36	35	oveq2d	$$⊢A\in ℂ\to {\sin A}^3={\sin A}^{2+1}$$
37		2nn0	$$⊢2\in {\mathbb{N}}_0$$
38	37	a1i	$$⊢A\in ℂ\to 2\in {\mathbb{N}}_0$$
39	15 38	expp1d	$$⊢A\in ℂ\to {\sin A}^{2+1}={\sin A}^2\sin A$$
40	25 15	mulcomd	$$⊢A\in ℂ\to {\sin A}^2\sin A=\sin A{\sin A}^2$$
41	36 39 40	3eqtrrd	$$⊢A\in ℂ\to \sin A{\sin A}^2={\sin A}^3$$
42	34 41	oveq12d	$$⊢A\in ℂ\to \sin A\cdot 1-\sin A{\sin A}^2=\sin A-{\sin A}^3$$
43	33 42	eqtrd	$$⊢A\in ℂ\to \sin A\left(1-{\sin A}^2\right)=\sin A-{\sin A}^3$$
44	43	oveq2d	$$⊢A\in ℂ\to 2\sin A\left(1-{\sin A}^2\right)=2\left(\sin A-{\sin A}^3\right)$$
45		3nn0	$$⊢3\in {\mathbb{N}}_0$$
46	45	a1i	$$⊢A\in ℂ\to 3\in {\mathbb{N}}_0$$
47	15 46	expcld	$$⊢A\in ℂ\to {\sin A}^3\in ℂ$$
48	3 15 47	subdid	$$⊢A\in ℂ\to 2\left(\sin A-{\sin A}^3\right)=2\sin A-2{\sin A}^3$$
49	32 44 48	3eqtrd	$$⊢A\in ℂ\to 2\sin A\cos A\cos 1A=2\sin A-2{\sin A}^3$$
50	14 19 49	3eqtrd	$$⊢A\in ℂ\to \sin 2A\cos 1A=2\sin A-2{\sin A}^3$$
51		cos2tsin	$$⊢A\in ℂ\to \cos 2A=1-2{\sin A}^2$$
52	20	fveq2d	$$⊢A\in ℂ\to \sin 1A=\sin A$$
53	51 52	oveq12d	$$⊢A\in ℂ\to \cos 2A\sin 1A=\left(1-2{\sin A}^2\right)\sin A$$
54	3 25	mulcld	$$⊢A\in ℂ\to 2{\sin A}^2\in ℂ$$
55	4 54 15	subdird	$$⊢A\in ℂ\to \left(1-2{\sin A}^2\right)\sin A=1\sin A-2{\sin A}^2\sin A$$
56	53 55	eqtrd	$$⊢A\in ℂ\to \cos 2A\sin 1A=1\sin A-2{\sin A}^2\sin A$$
57	50 56	oveq12d	$$⊢A\in ℂ\to \sin 2A\cos 1A+\cos 2A\sin 1A=\left(2\sin A-2{\sin A}^3\right)+1\sin A-2{\sin A}^2\sin A$$
58	3 15	mulcld	$$⊢A\in ℂ\to 2\sin A\in ℂ$$
59	4 15	mulcld	$$⊢A\in ℂ\to 1\sin A\in ℂ$$
60	3 47	mulcld	$$⊢A\in ℂ\to 2{\sin A}^3\in ℂ$$
61	54 15	mulcld	$$⊢A\in ℂ\to 2{\sin A}^2\sin A\in ℂ$$
62	58 59 60 61	addsub4d	$$⊢A\in ℂ\to 2\sin A+1\sin A-\left(2{\sin A}^3+2{\sin A}^2\sin A\right)=\left(2\sin A-2{\sin A}^3\right)+1\sin A-2{\sin A}^2\sin A$$
63	3 4 15	adddird	$$⊢A\in ℂ\to \left(2+1\right)\sin A=2\sin A+1\sin A$$
64		2p1e3	$$⊢2+1=3$$
65	64	a1i	$$⊢A\in ℂ\to 2+1=3$$
66	65	oveq1d	$$⊢A\in ℂ\to \left(2+1\right)\sin A=3\sin A$$
67	63 66	eqtr3d	$$⊢A\in ℂ\to 2\sin A+1\sin A=3\sin A$$
68	3 3 47	adddird	$$⊢A\in ℂ\to \left(2+2\right){\sin A}^3=2{\sin A}^3+2{\sin A}^3$$
69		2p2e4	$$⊢2+2=4$$
70	69	eqcomi	$$⊢4=2+2$$
71	70	a1i	$$⊢A\in ℂ\to 4=2+2$$
72	71	oveq1d	$$⊢A\in ℂ\to 4{\sin A}^3=\left(2+2\right){\sin A}^3$$
73	3 25 15	mulassd	$$⊢A\in ℂ\to 2{\sin A}^2\sin A=2{\sin A}^2\sin A$$
74	40	oveq2d	$$⊢A\in ℂ\to 2{\sin A}^2\sin A=2\sin A{\sin A}^2$$
75	41	oveq2d	$$⊢A\in ℂ\to 2\sin A{\sin A}^2=2{\sin A}^3$$
76	73 74 75	3eqtrd	$$⊢A\in ℂ\to 2{\sin A}^2\sin A=2{\sin A}^3$$
77	76	oveq2d	$$⊢A\in ℂ\to 2{\sin A}^3+2{\sin A}^2\sin A=2{\sin A}^3+2{\sin A}^3$$
78	68 72 77	3eqtr4rd	$$⊢A\in ℂ\to 2{\sin A}^3+2{\sin A}^2\sin A=4{\sin A}^3$$
79	67 78	oveq12d	$$⊢A\in ℂ\to 2\sin A+1\sin A-\left(2{\sin A}^3+2{\sin A}^2\sin A\right)=3\sin A-4{\sin A}^3$$
80	57 62 79	3eqtr2d	$$⊢A\in ℂ\to \sin 2A\cos 1A+\cos 2A\sin 1A=3\sin A-4{\sin A}^3$$
81	8 12 80	3eqtrd	$$⊢A\in ℂ\to \sin 3A=3\sin A-4{\sin A}^3$$