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