Theorem sin5tlem5

Description: Lemma 5 for quintupled angle sine calculation: sine of triple-angle and double-angle sum, as a polynomial in sine straight. (Contributed by Ender Ting, 17-Apr-2026)

	Ref	Expression
Assertion	sin5tlem5	$$⊢\left(N\in ℂ\wedge M\in ℂ\wedge N^2=1-M^2\right)\to \left(3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-4M^3\right)\left(1-2M^2\right)+\left(4N^3-3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)2\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=16M^5-20M^3+5\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$

Proof

Step	Hyp	Ref	Expression
1		sin5tlem1	$$⊢M\in ℂ\to \left(3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-4M^3\right)\left(1-2M^2\right)=8M^5-10M^3+3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
2	1	3ad2ant2	$$⊢\left(N\in ℂ\wedge M\in ℂ\wedge N^2=1-M^2\right)\to \left(3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-4M^3\right)\left(1-2M^2\right)=8M^5-10M^3+3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
3		sin5tlem4	$$⊢\left(N\in ℂ\wedge M\in ℂ\wedge N^2=1-M^2\right)\to \left(4N^3-3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)2\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\left(8M^5-16M^3\right)+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-\left(6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6M^3\right)$$
4	2 3	oveq12d	$$⊢\left(N\in ℂ\wedge M\in ℂ\wedge N^2=1-M^2\right)\to \left(3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-4M^3\right)\left(1-2M^2\right)+\left(4N^3-3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)2\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=\left(8M^5-10M^3\right)+3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(\left(8M^5-16M^3\right)+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-\left(6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6M^3\right)\right)$$
5		8cn	$$⊢8\in ℂ$$
6	5	a1i	$$⊢M\in ℂ\to 8\in ℂ$$
7		id	$$⊢M\in ℂ\to M\in ℂ$$
8	6 7	mulcld	$$⊢M\in ℂ\to 8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℂ$$
9		6cn	$$⊢6\in ℂ$$
10	9	a1i	$$⊢M\in ℂ\to 6\in ℂ$$
11	10 7	mulcld	$$⊢M\in ℂ\to 6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℂ$$
12	8 11	subcld	$$⊢M\in ℂ\to 8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℂ$$
13		5nn0	$$⊢5\in {\mathbb{N}}_0$$
14	13	a1i	$$⊢M\in ℂ\to 5\in {\mathbb{N}}_0$$
15	7 14	expcld	$$⊢M\in ℂ\to M^5\in ℂ$$
16	6 15	mulcld	$$⊢M\in ℂ\to 8M^5\in ℂ$$
17		1nn0	$$⊢1\in {\mathbb{N}}_0$$
18		6nn0	$$⊢6\in {\mathbb{N}}_0$$
19	17 18	deccl	$$⊢16\in {\mathbb{N}}_0$$
20	19	nn0cni	$$⊢16\in ℂ$$
21	20	a1i	$$⊢M\in ℂ\to 16\in ℂ$$
22		3nn0	$$⊢3\in {\mathbb{N}}_0$$
23	22	a1i	$$⊢M\in ℂ\to 3\in {\mathbb{N}}_0$$
24	7 23	expcld	$$⊢M\in ℂ\to M^3\in ℂ$$
25	21 24	mulcld	$$⊢M\in ℂ\to 16M^3\in ℂ$$
26	16 25	subcld	$$⊢M\in ℂ\to 8M^5-16M^3\in ℂ$$
27	10 24	mulcld	$$⊢M\in ℂ\to 6M^3\in ℂ$$
28	26 27	addcld	$$⊢M\in ℂ\to 8M^5-16M^3+6M^3\in ℂ$$
29	26 8	addcomd	$$⊢M\in ℂ\to 8M^5-16M^3+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+8M^5-16M^3$$
30	29	oveq1d	$$⊢M\in ℂ\to \left(8M^5-16M^3\right)+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-\left(6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6M^3\right)=8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(8M^5-16M^3\right)-\left(6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6M^3\right)$$
31	8 26 11 27	addsubsub23	$$⊢M\in ℂ\to 8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(8M^5-16M^3\right)-\left(6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6M^3\right)=\left(8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)+\left(8M^5-16M^3\right)+6M^3$$
32	30 31	eqtrd	$$⊢M\in ℂ\to \left(8M^5-16M^3\right)+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-\left(6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6M^3\right)=\left(8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)+\left(8M^5-16M^3\right)+6M^3$$
33	12 28 32	comraddd	$$⊢M\in ℂ\to \left(8M^5-16M^3\right)+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-\left(6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6M^3\right)=\left(8M^5-16M^3\right)+6M^3+\left(8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)$$
34	33	oveq2d	$$⊢M\in ℂ\to \left(8M^5-10M^3\right)+3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(\left(8M^5-16M^3\right)+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-\left(6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6M^3\right)\right)=\left(8M^5-10M^3\right)+3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(8M^5-16M^3+6M^3\right)+\left(8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)$$
35		10nn	$$⊢10\in \mathbb{N}$$
36	35	nncni	$$⊢10\in ℂ$$
37	36	a1i	$$⊢M\in ℂ\to 10\in ℂ$$
38	37 24	mulcld	$$⊢M\in ℂ\to 10M^3\in ℂ$$
39	16 38	subcld	$$⊢M\in ℂ\to 8M^5-10M^3\in ℂ$$
40		3cn	$$⊢3\in ℂ$$
41	40	a1i	$$⊢M\in ℂ\to 3\in ℂ$$
42	41 7	mulcld	$$⊢M\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℂ$$
43	39 42 28 12	add4d	$$⊢M\in ℂ\to \left(8M^5-10M^3\right)+3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(8M^5-16M^3+6M^3\right)+\left(8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)=\left(8M^5-10M^3\right)+\left(8M^5-16M^3+6M^3\right)+3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)$$
44	16 16 38 38	addsub4d	$$⊢M\in ℂ\to 8M^5+8M^5-\left(10M^3+10M^3\right)=\left(8M^5-10M^3\right)+8M^5-10M^3$$
45		8p8e16	$$⊢8+8=16$$
46	45	eqcomi	$$⊢16=8+8$$
47	46	a1i	$$⊢M\in ℂ\to 16=8+8$$
48	47	oveq1d	$$⊢M\in ℂ\to 16M^5=\left(8+8\right)M^5$$
49	6 6 15	adddird	$$⊢M\in ℂ\to \left(8+8\right)M^5=8M^5+8M^5$$
50	48 49	eqtrd	$$⊢M\in ℂ\to 16M^5=8M^5+8M^5$$
51		10p10e20	$$⊢10+10=20$$
52	51	eqcomi	$$⊢20=10+10$$
53	52	a1i	$$⊢M\in ℂ\to 20=10+10$$
54	53	oveq1d	$$⊢M\in ℂ\to 20M^3=\left(10+10\right)M^3$$
55	37 37 24	adddird	$$⊢M\in ℂ\to \left(10+10\right)M^3=10M^3+10M^3$$
56	54 55	eqtrd	$$⊢M\in ℂ\to 20M^3=10M^3+10M^3$$
57	50 56	oveq12d	$$⊢M\in ℂ\to 16M^5-20M^3=8M^5+8M^5-\left(10M^3+10M^3\right)$$
58	21 10 24	subdird	$$⊢M\in ℂ\to \left(16-6\right)M^3=16M^3-6M^3$$
59	58	eqcomd	$$⊢M\in ℂ\to 16M^3-6M^3=\left(16-6\right)M^3$$
60	59	oveq2d	$$⊢M\in ℂ\to 8M^5-\left(16M^3-6M^3\right)=8M^5-\left(16-6\right)M^3$$
61	16 25 27	subsubd	$$⊢M\in ℂ\to 8M^5-\left(16M^3-6M^3\right)=8M^5-16M^3+6M^3$$
62		dec10p	$$⊢10+6=16$$
63	62	eqcomi	$$⊢16=10+6$$
64	63	a1i	$$⊢M\in ℂ\to 16=10+6$$
65	37 10 64	mvrraddd	$$⊢M\in ℂ\to 16-6=10$$
66	65	oveq1d	$$⊢M\in ℂ\to \left(16-6\right)M^3=10M^3$$
67	66	oveq2d	$$⊢M\in ℂ\to 8M^5-\left(16-6\right)M^3=8M^5-10M^3$$
68	60 61 67	3eqtr3d	$$⊢M\in ℂ\to 8M^5-16M^3+6M^3=8M^5-10M^3$$
69	68	oveq2d	$$⊢M\in ℂ\to \left(8M^5-10M^3\right)+\left(8M^5-16M^3\right)+6M^3=\left(8M^5-10M^3\right)+8M^5-10M^3$$
70	44 57 69	3eqtr4rd	$$⊢M\in ℂ\to \left(8M^5-10M^3\right)+\left(8M^5-16M^3\right)+6M^3=16M^5-20M^3$$
71	6 10	subcld	$$⊢M\in ℂ\to 8-6\in ℂ$$
72	41 71 7	adddird	$$⊢M\in ℂ\to \left(3+8-6\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(8-6\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
73		2cn	$$⊢2\in ℂ$$
74		6p2e8	$$⊢6+2=8$$
75	74	eqcomi	$$⊢8=6+2$$
76	9 73 75	mvrladdi	$$⊢8-6=2$$
77	76	oveq2i	$$⊢3+8-6=3+2$$
78		3p2e5	$$⊢3+2=5$$
79	77 78	eqtri	$$⊢3+8-6=5$$
80	79	a1i	$$⊢M\in ℂ\to 3+8-6=5$$
81	80	oveq1d	$$⊢M\in ℂ\to \left(3+8-6\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=5\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
82	6 10 7	subdird	$$⊢M\in ℂ\to \left(8-6\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
83	82	oveq2d	$$⊢M\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(8-6\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
84	72 81 83	3eqtr3rd	$$⊢M\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=5\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
85	70 84	oveq12d	$$⊢M\in ℂ\to \left(8M^5-10M^3\right)+\left(8M^5-16M^3+6M^3\right)+3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\right)=16M^5-20M^3+5\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
86	34 43 85	3eqtrd	$$⊢M\in ℂ\to \left(8M^5-10M^3\right)+3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(\left(8M^5-16M^3\right)+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-\left(6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6M^3\right)\right)=16M^5-20M^3+5\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
87	86	3ad2ant2	$$⊢\left(N\in ℂ\wedge M\in ℂ\wedge N^2=1-M^2\right)\to \left(8M^5-10M^3\right)+3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+\left(\left(8M^5-16M^3\right)+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-\left(6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6M^3\right)\right)=16M^5-20M^3+5\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
88	4 87	eqtrd	$$⊢\left(N\in ℂ\wedge M\in ℂ\wedge N^2=1-M^2\right)\to \left(3\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-4M^3\right)\left(1-2M^2\right)+\left(4N^3-3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\right)2\mathrm{<mi\; mathcolor="\#808">M</mi>}\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=16M^5-20M^3+5\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$