Theorem sin5tlem4

Description: Lemma 4 for quintupled angle sine calculation: expanding lemma 3 result to difference of polynomials. (Contributed by Ender Ting, 17-Apr-2026)

	Ref	Expression
Assertion	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)$$

Proof

Step	Hyp	Ref	Expression
1		sin5tlem3	$$⊢\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(4\left(1-2M^2+M^4\right)-3\left(1-M^2\right)\right)2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
2		4cn	$$⊢4\in ℂ$$
3	2	a1i	$$⊢M\in ℂ\to 4\in ℂ$$
4		1cnd	$$⊢M\in ℂ\to 1\in ℂ$$
5		2cnd	$$⊢M\in ℂ\to 2\in ℂ$$
6		sqcl	$$⊢M\in ℂ\to M^2\in ℂ$$
7	5 6	mulcld	$$⊢M\in ℂ\to 2M^2\in ℂ$$
8	4 7	subcld	$$⊢M\in ℂ\to 1-2M^2\in ℂ$$
9		id	$$⊢M\in ℂ\to M\in ℂ$$
10		4nn0	$$⊢4\in {\mathbb{N}}_0$$
11	10	a1i	$$⊢M\in ℂ\to 4\in {\mathbb{N}}_0$$
12	9 11	expcld	$$⊢M\in ℂ\to M^4\in ℂ$$
13	8 12	addcld	$$⊢M\in ℂ\to 1-2M^2+M^4\in ℂ$$
14	3 13	mulcld	$$⊢M\in ℂ\to 4\left(1-2M^2+M^4\right)\in ℂ$$
15		3cn	$$⊢3\in ℂ$$
16	15	a1i	$$⊢M\in ℂ\to 3\in ℂ$$
17	4 6	subcld	$$⊢M\in ℂ\to 1-M^2\in ℂ$$
18	16 17	mulcld	$$⊢M\in ℂ\to 3\left(1-M^2\right)\in ℂ$$
19	5 9	mulcld	$$⊢M\in ℂ\to 2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℂ$$
20	14 18 19	subdird	$$⊢M\in ℂ\to \left(4\left(1-2M^2+M^4\right)-3\left(1-M^2\right)\right)2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=4\left(1-2M^2+M^4\right)2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-3\left(1-M^2\right)2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
21	3 13 5 9	mul4d	$$⊢M\in ℂ\to 4\left(1-2M^2+M^4\right)2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=4\cdot 2\left(1-2M^2+M^4\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
22		4t2e8	$$⊢4\cdot 2=8$$
23	22	a1i	$$⊢M\in ℂ\to 4\cdot 2=8$$
24	23	oveq1d	$$⊢M\in ℂ\to 4\cdot 2\left(1-2M^2+M^4\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=8\left(1-2M^2+M^4\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
25	4 12 7	addsubd	$$⊢M\in ℂ\to 1+M^4-2M^2=1-2M^2+M^4$$
26	25	eqcomd	$$⊢M\in ℂ\to 1-2M^2+M^4=1+M^4-2M^2$$
27	26	oveq1d	$$⊢M\in ℂ\to \left(1-2M^2+M^4\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=\left(1+M^4-2M^2\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
28	4 12	addcld	$$⊢M\in ℂ\to 1+M^4\in ℂ$$
29	28 7 9	subdird	$$⊢M\in ℂ\to \left(1+M^4-2M^2\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=\left(1+M^4\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-2M^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
30		5nn0	$$⊢5\in {\mathbb{N}}_0$$
31	30	a1i	$$⊢M\in ℂ\to 5\in {\mathbb{N}}_0$$
32	9 31	expcld	$$⊢M\in ℂ\to M^5\in ℂ$$
33		mullid	$$⊢M\in ℂ\to 1\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M$$
34	9 11	expp1d	$$⊢M\in ℂ\to M^{4+1}=M^4\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
35		4p1e5	$$⊢4+1=5$$
36	35	a1i	$$⊢M\in ℂ\to 4+1=5$$
37	36	oveq2d	$$⊢M\in ℂ\to M^{4+1}=M^5$$
38	34 37	eqtr3d	$$⊢M\in ℂ\to M^4\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M^5$$
39	33 38	oveq12d	$$⊢M\in ℂ\to 1\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}+M^4\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M+M^5$$
40	4 9 12 39	joinlmuladdmuld	$$⊢M\in ℂ\to \left(1+M^4\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M+M^5$$
41	9 32 40	comraddd	$$⊢M\in ℂ\to \left(1+M^4\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M^5+M$$
42	5 6 9	mulassd	$$⊢M\in ℂ\to 2M^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=2M^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
43		2nn0	$$⊢2\in {\mathbb{N}}_0$$
44	43	a1i	$$⊢M\in ℂ\to 2\in {\mathbb{N}}_0$$
45	9 44	expp1d	$$⊢M\in ℂ\to M^{2+1}=M^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
46		2p1e3	$$⊢2+1=3$$
47	46	a1i	$$⊢M\in ℂ\to 2+1=3$$
48	47	oveq2d	$$⊢M\in ℂ\to M^{2+1}=M^3$$
49	45 48	eqtr3d	$$⊢M\in ℂ\to M^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M^3$$
50	49	oveq2d	$$⊢M\in ℂ\to 2M^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=2M^3$$
51	42 50	eqtrd	$$⊢M\in ℂ\to 2M^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=2M^3$$
52	41 51	oveq12d	$$⊢M\in ℂ\to \left(1+M^4\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-2M^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M^5+M-2M^3$$
53	27 29 52	3eqtrd	$$⊢M\in ℂ\to \left(1-2M^2+M^4\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M^5+M-2M^3$$
54	53	oveq2d	$$⊢M\in ℂ\to 8\left(1-2M^2+M^4\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=8\left(M^5+M-2M^3\right)$$
55		8cn	$$⊢8\in ℂ$$
56	55	a1i	$$⊢M\in ℂ\to 8\in ℂ$$
57	32 9	addcld	$$⊢M\in ℂ\to M^5+M\in ℂ$$
58		3nn0	$$⊢3\in {\mathbb{N}}_0$$
59	58	a1i	$$⊢M\in ℂ\to 3\in {\mathbb{N}}_0$$
60	9 59	expcld	$$⊢M\in ℂ\to M^3\in ℂ$$
61	5 60	mulcld	$$⊢M\in ℂ\to 2M^3\in ℂ$$
62	56 57 61	subdid	$$⊢M\in ℂ\to 8\left(M^5+M-2M^3\right)=8\left(M^5+M\right)-82M^3$$
63	56 5 60	mulassd	$$⊢M\in ℂ\to 8\cdot 2M^3=82M^3$$
64	63	eqcomd	$$⊢M\in ℂ\to 82M^3=8\cdot 2M^3$$
65	64	oveq2d	$$⊢M\in ℂ\to 8\left(M^5+M\right)-82M^3=8\left(M^5+M\right)-8\cdot 2M^3$$
66	54 62 65	3eqtrd	$$⊢M\in ℂ\to 8\left(1-2M^2+M^4\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=8\left(M^5+M\right)-8\cdot 2M^3$$
67	56 32 9	adddid	$$⊢M\in ℂ\to 8\left(M^5+M\right)=8M^5+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
68		8t2e16	$$⊢8\cdot 2=16$$
69	68	a1i	$$⊢M\in ℂ\to 8\cdot 2=16$$
70	69	oveq1d	$$⊢M\in ℂ\to 8\cdot 2M^3=16M^3$$
71	67 70	oveq12d	$$⊢M\in ℂ\to 8\left(M^5+M\right)-8\cdot 2M^3=8M^5+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-16M^3$$
72	24 66 71	3eqtrd	$$⊢M\in ℂ\to 4\cdot 2\left(1-2M^2+M^4\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=8M^5+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-16M^3$$
73	56 32	mulcld	$$⊢M\in ℂ\to 8M^5\in ℂ$$
74	56 9	mulcld	$$⊢M\in ℂ\to 8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}\in ℂ$$
75		1nn0	$$⊢1\in {\mathbb{N}}_0$$
76		6nn0	$$⊢6\in {\mathbb{N}}_0$$
77	75 76	deccl	$$⊢16\in {\mathbb{N}}_0$$
78	77	nn0cni	$$⊢16\in ℂ$$
79	78	a1i	$$⊢M\in ℂ\to 16\in ℂ$$
80	79 60	mulcld	$$⊢M\in ℂ\to 16M^3\in ℂ$$
81	73 74 80	addsubd	$$⊢M\in ℂ\to 8M^5+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-16M^3=8M^5-16M^3+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
82	21 72 81	3eqtrd	$$⊢M\in ℂ\to 4\left(1-2M^2+M^4\right)2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=8M^5-16M^3+8\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
83	16 17 5 9	mul4d	$$⊢M\in ℂ\to 3\left(1-M^2\right)2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=3\cdot 2\left(1-M^2\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
84		3t2e6	$$⊢3\cdot 2=6$$
85	84	a1i	$$⊢M\in ℂ\to 3\cdot 2=6$$
86	4 6 9	subdird	$$⊢M\in ℂ\to \left(1-M^2\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=1\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-M^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}$$
87	33 49	oveq12d	$$⊢M\in ℂ\to 1\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-M^2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M-M^3$$
88	86 87	eqtrd	$$⊢M\in ℂ\to \left(1-M^2\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=M-M^3$$
89	85 88	oveq12d	$$⊢M\in ℂ\to 3\cdot 2\left(1-M^2\right)\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=6\left(M-M^3\right)$$
90		6cn	$$⊢6\in ℂ$$
91	90	a1i	$$⊢M\in ℂ\to 6\in ℂ$$
92	91 9 60	subdid	$$⊢M\in ℂ\to 6\left(M-M^3\right)=6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6M^3$$
93	83 89 92	3eqtrd	$$⊢M\in ℂ\to 3\left(1-M^2\right)2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}=6\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-6M^3$$
94	82 93	oveq12d	$$⊢M\in ℂ\to 4\left(1-2M^2+M^4\right)2\cdot \mathrm{<mi\; mathcolor="\#808">M</mi>}-3\left(1-M^2\right)2\cdot \mathrm{<mi\; mathcolor="\#808">M</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)$$
95	20 94	eqtrd	$$⊢M\in ℂ\to \left(4\left(1-2M^2+M^4\right)-3\left(1-M^2\right)\right)2\cdot \mathrm{<mi\; mathcolor="\#808">M</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)$$
96	95	3ad2ant2	$$⊢\left(N\in ℂ\wedge M\in ℂ\wedge N^2=1-M^2\right)\to \left(4\left(1-2M^2+M^4\right)-3\left(1-M^2\right)\right)2\cdot \mathrm{<mi\; mathcolor="\#808">M</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)$$
97	1 96	eqtrd	$$⊢\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)$$