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	5	2timesi	$$⊢2\cdot 4=4+4$$
27		4p4e8	$$⊢4+4=8$$
28	26 27	eqtri	$$⊢2\cdot 4=8$$
29	28	a1i	$$⊢N\in ℂ\to 2\cdot 4=8$$
30		2nn0	$$⊢2\in {\mathbb{N}}_0$$
31	30	a1i	$$⊢N\in ℂ\to 2\in {\mathbb{N}}_0$$
32	3 8 31	expaddd	$$⊢N\in ℂ\to N^{2+3}=N^2{N}^3$$
33		2cn	$$⊢2\in ℂ$$
34		3p2e5	$$⊢3+2=5$$
35	1 33 34	addcomli	$$⊢2+3=5$$
36	35	oveq2i	$$⊢N^{2+3}=N^5$$
37	32 36	eqtr3di	$$⊢N\in ℂ\to N^2{N}^3=N^5$$
38	29 37	oveq12d	$$⊢N\in ℂ\to 2\cdot 4N^2{N}^3=8N^5$$
39	25 38	eqtrd	$$⊢N\in ℂ\to 2N^{2}4N^3=8N^5$$
40	2 3 12 13	mul4d	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2=3\cdot 2N{N}^2$$
41		3t2e6	$$⊢3\cdot 2=6$$
42	41	a1i	$$⊢N\in ℂ\to 3\cdot 2=6$$
43		df-3	$$⊢3=2+1$$
44	43	oveq2i	$$⊢N^3=N^{2+1}$$
45	3 31	expp1d	$$⊢N\in ℂ\to N^{2+1}=N^2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
46	13 3	mulcomd	$$⊢N\in ℂ\to N^2\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}=N{N}^2$$
47	45 46	eqtrd	$$⊢N\in ℂ\to N^{2+1}=N{N}^2$$
48	44 47	eqtr2id	$$⊢N\in ℂ\to N{N}^2=N^3$$
49	42 48	oveq12d	$$⊢N\in ℂ\to 3\cdot 2N{N}^2=6N^3$$
50	40 49	eqtrd	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2=6N^3$$
51	10	mullidd	$$⊢N\in ℂ\to 14N^3=4N^3$$
52	50 51	oveq12d	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2+14N^3=6N^3+4N^3$$
53		6cn	$$⊢6\in ℂ$$
54	53	a1i	$$⊢N\in ℂ\to 6\in ℂ$$
55	54 6 9	adddird	$$⊢N\in ℂ\to \left(6+4\right)N^3=6N^3+4N^3$$
56		6p4e10	$$⊢6+4=10$$
57	56	a1i	$$⊢N\in ℂ\to 6+4=10$$
58	57	oveq1d	$$⊢N\in ℂ\to \left(6+4\right)N^3=10N^3$$
59	52 55 58	3eqtr2d	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}2N^2+14N^3=10N^3$$
60	39 59	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$$
61	4	mulridd	$$⊢N\in ℂ\to 3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}\cdot 1=3\cdot \mathrm{<mi\; mathcolor="\#808">N</mi>}$$
62	60 61	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>}$$
63	15 24 62	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>}$$