Theorem sin5t

Description: Five-times-angle formula for sine, in pure sine form. (Contributed by Ender Ting, 17-Apr-2026)

	Ref	Expression
Assertion	sin5t	$$⊢A\in ℂ\to \sin 5A=16{\sin A}^5-20{\sin A}^3+5\sin A$$

Proof

Step	Hyp	Ref	Expression
1		3p2e5	$$⊢3+2=5$$
2	1	eqcomi	$$⊢5=3+2$$
3	2	a1i	$$⊢A\in ℂ\to 5=3+2$$
4	3	oveq1d	$$⊢A\in ℂ\to 5A=\left(3+2\right)A$$
5		3cn	$$⊢3\in ℂ$$
6	5	a1i	$$⊢A\in ℂ\to 3\in ℂ$$
7		2cnd	$$⊢A\in ℂ\to 2\in ℂ$$
8		id	$$⊢A\in ℂ\to A\in ℂ$$
9	6 7 8	adddird	$$⊢A\in ℂ\to \left(3+2\right)A=3A+2A$$
10	4 9	eqtrd	$$⊢A\in ℂ\to 5A=3A+2A$$
11	10	fveq2d	$$⊢A\in ℂ\to \sin 5A=\sin \left(3A+2A\right)$$
12	6 8	mulcld	$$⊢A\in ℂ\to 3A\in ℂ$$
13	7 8	mulcld	$$⊢A\in ℂ\to 2A\in ℂ$$
14		sinadd	$$⊢\left(3A\in ℂ\wedge 2A\in ℂ\right)\to \sin \left(3A+2A\right)=\sin 3A\cos 2A+\cos 3A\sin 2A$$
15	12 13 14	syl2anc	$$⊢A\in ℂ\to \sin \left(3A+2A\right)=\sin 3A\cos 2A+\cos 3A\sin 2A$$
16		sin3t	$$⊢A\in ℂ\to \sin 3A=3\sin A-4{\sin A}^3$$
17		cos2tsin	$$⊢A\in ℂ\to \cos 2A=1-2{\sin A}^2$$
18	16 17	oveq12d	$$⊢A\in ℂ\to \sin 3A\cos 2A=\left(3\sin A-4{\sin A}^3\right)\left(1-2{\sin A}^2\right)$$
19		cos3t	$$⊢A\in ℂ\to \cos 3A=4{\cos A}^3-3\cos A$$
20		sin2t	$$⊢A\in ℂ\to \sin 2A=2\sin A\cos A$$
21	19 20	oveq12d	$$⊢A\in ℂ\to \cos 3A\sin 2A=\left(4{\cos A}^3-3\cos A\right)2\sin A\cos A$$
22	18 21	oveq12d	$$⊢A\in ℂ\to \sin 3A\cos 2A+\cos 3A\sin 2A=\left(3\sin A-4{\sin A}^3\right)\left(1-2{\sin A}^2\right)+\left(4{\cos A}^3-3\cos A\right)2\sin A\cos A$$
23	15 22	eqtrd	$$⊢A\in ℂ\to \sin \left(3A+2A\right)=\left(3\sin A-4{\sin A}^3\right)\left(1-2{\sin A}^2\right)+\left(4{\cos A}^3-3\cos A\right)2\sin A\cos A$$
24		coscl	$$⊢A\in ℂ\to \cos A\in ℂ$$
25		sincl	$$⊢A\in ℂ\to \sin A\in ℂ$$
26	25	sqcld	$$⊢A\in ℂ\to {\sin A}^2\in ℂ$$
27	24	sqcld	$$⊢A\in ℂ\to {\cos A}^2\in ℂ$$
28		sincossq	$$⊢A\in ℂ\to {\sin A}^2+{\cos A}^2=1$$
29	26 27 28	mvlladdd	$$⊢A\in ℂ\to {\cos A}^2=1-{\sin A}^2$$
30		sin5tlem5	$$⊢\left(\cos A\in ℂ\wedge \sin A\in ℂ\wedge {\cos A}^2=1-{\sin A}^2\right)\to \left(3\sin A-4{\sin A}^3\right)\left(1-2{\sin A}^2\right)+\left(4{\cos A}^3-3\cos A\right)2\sin A\cos A=16{\sin A}^5-20{\sin A}^3+5\sin A$$
31	24 25 29 30	syl3anc	$$⊢A\in ℂ\to \left(3\sin A-4{\sin A}^3\right)\left(1-2{\sin A}^2\right)+\left(4{\cos A}^3-3\cos A\right)2\sin A\cos A=16{\sin A}^5-20{\sin A}^3+5\sin A$$
32	11 23 31	3eqtrd	$$⊢A\in ℂ\to \sin 5A=16{\sin A}^5-20{\sin A}^3+5\sin A$$