Theorem sin5tlem1

Description: Lemma 1 for quintupled angle sine calculation, expanding triple-angle sine times double-angle cosine. (Contributed by Ender Ting, 16-Mar-2026)

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

Proof

Step	Hyp	Ref	Expression
1		3cn	$$⊢3\in ℂ$$
2	1	a1i	$$⊢N\in ℂ\to 3\in ℂ$$
3		id	$$⊢N\in ℂ\to N\in ℂ$$
4	2 3	mulcld	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\in ℂ$$
5		4cn	$$⊢4\in ℂ$$
6	5	a1i	$$⊢N\in ℂ\to 4\in ℂ$$
7		3nn0	$$⊢3\in {\mathbb{N}}_0$$
8	7	a1i	$$⊢N\in ℂ\to 3\in {\mathbb{N}}_0$$
9	3 8	expcld	$$⊢N\in ℂ\to N^3\in ℂ$$
10	6 9	mulcld	$$⊢N\in ℂ\to 4N^3\in ℂ$$
11		1cnd	$$⊢N\in ℂ\to 1\in ℂ$$
12		2cnd	$$⊢N\in ℂ\to 2\in ℂ$$
13		sqcl	$$⊢N\in ℂ\to N^2\in ℂ$$
14	12 13	mulcld	$$⊢N\in ℂ\to 2N^2\in ℂ$$
15	4 10 11 14	mulsubd	$$⊢N\in ℂ\to \left(3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-4N^3\right)\left(1-2N^2\right)=3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1+2N^{2}4N^3-\left(3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2+14N^3\right)$$
16	4 11	mulcld	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1\in ℂ$$
17	14 10	mulcld	$$⊢N\in ℂ\to 2N^{2}4N^3\in ℂ$$
18	16 17	addcomd	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1+2N^{2}4N^3=2N^{2}4N^3+3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1$$
19	18	oveq1d	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1+2N^{2}4N^3-\left(3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2+14N^3\right)=2N^{2}4N^3+3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1-\left(3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2+14N^3\right)$$
20	4 14	mulcld	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2\in ℂ$$
21	11 10	mulcld	$$⊢N\in ℂ\to 14N^3\in ℂ$$
22	20 21	addcld	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2+14N^3\in ℂ$$
23	17 16 22	addsubd	$$⊢N\in ℂ\to 2N^{2}4N^3+3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1-\left(3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2+14N^3\right)=2N^{2}4N^3-\left(3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2+14N^3\right)+3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1$$
24	19 23	eqtrd	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1+2N^{2}4N^3-\left(3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2+14N^3\right)=2N^{2}4N^3-\left(3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2+14N^3\right)+3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1$$
25	12 13 6 9	mul4d	$$⊢N\in ℂ\to 2N^{2}4N^3=2\cdot 4N^2{N}^3$$
26		2t4e8	$$⊢2\cdot 4=8$$
27	26	a1i	$$⊢N\in ℂ\to 2\cdot 4=8$$
28		2nn0	$$⊢2\in {\mathbb{N}}_0$$
29	28	a1i	$$⊢N\in ℂ\to 2\in {\mathbb{N}}_0$$
30	3 8 29	expaddd	$$⊢N\in ℂ\to N^{2+3}=N^2{N}^3$$
31		2cn	$$⊢2\in ℂ$$
32		3p2e5	$$⊢3+2=5$$
33	1 31 32	addcomli	$$⊢2+3=5$$
34	33	oveq2i	$$⊢N^{2+3}=N^5$$
35	30 34	eqtr3di	$$⊢N\in ℂ\to N^2{N}^3=N^5$$
36	27 35	oveq12d	$$⊢N\in ℂ\to 2\cdot 4N^2{N}^3=8N^5$$
37	25 36	eqtrd	$$⊢N\in ℂ\to 2N^{2}4N^3=8N^5$$
38	2 3 12 13	mul4d	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2=3\cdot 2N{N}^2$$
39		3t2e6	$$⊢3\cdot 2=6$$
40	39	a1i	$$⊢N\in ℂ\to 3\cdot 2=6$$
41		df-3	$$⊢3=2+1$$
42	41	oveq2i	$$⊢N^3=N^{2+1}$$
43	3 29	expp1d	$$⊢N\in ℂ\to N^{2+1}=N^2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
44	13 3	mulcomd	$$⊢N\in ℂ\to N^2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N{N}^2$$
45	43 44	eqtrd	$$⊢N\in ℂ\to N^{2+1}=N{N}^2$$
46	42 45	eqtr2id	$$⊢N\in ℂ\to N{N}^2=N^3$$
47	40 46	oveq12d	$$⊢N\in ℂ\to 3\cdot 2N{N}^2=6N^3$$
48	38 47	eqtrd	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2=6N^3$$
49	10	mullidd	$$⊢N\in ℂ\to 14N^3=4N^3$$
50	48 49	oveq12d	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2+14N^3=6N^3+4N^3$$
51		6cn	$$⊢6\in ℂ$$
52	51	a1i	$$⊢N\in ℂ\to 6\in ℂ$$
53	52 6 9	adddird	$$⊢N\in ℂ\to \left(6+4\right)N^3=6N^3+4N^3$$
54		6p4e10	$$⊢6+4=10$$
55	54	a1i	$$⊢N\in ℂ\to 6+4=10$$
56	55	oveq1d	$$⊢N\in ℂ\to \left(6+4\right)N^3=10N^3$$
57	50 53 56	3eqtr2d	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2+14N^3=10N^3$$
58	37 57	oveq12d	$$⊢N\in ℂ\to 2N^{2}4N^3-\left(3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2+14N^3\right)=8N^5-10N^3$$
59	4	mulridd	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1=3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
60	58 59	oveq12d	$$⊢N\in ℂ\to 2N^{2}4N^3-\left(3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2+14N^3\right)+3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1=8N^5-10N^3+3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
61	15 24 60	3eqtrd	$$⊢N\in ℂ\to \left(3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}-4N^3\right)\left(1-2N^2\right)=8N^5-10N^3+3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$