sin5tlem5 - Mathbox for Ender Ting

	Mathbox for Ender Ting		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > sin5tlem5		Structured version Visualization version GIF version

Theorem sin5tlem5 47435

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.)

**Assertion**
Ref	Expression
sin5tlem5	⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → ((((3 · 𝑀) − (4 · (𝑀↑3))) · (1 − (2 · (𝑀↑2)))) + (((4 · (𝑁↑3)) − (3 · 𝑁)) · (2 · (𝑀 · 𝑁)))) = (((;16 · (𝑀↑5)) − (;20 · (𝑀↑3))) + (5 · 𝑀)))

**Proof of Theorem sin5tlem5**
Step	Hyp	Ref	Expression
1		sin5tlem1 47431	. . . 4 ⊢ (𝑀 ∈ ℂ → (((3 · 𝑀) − (4 · (𝑀↑3))) · (1 − (2 · (𝑀↑2)))) = (((8 · (𝑀↑5)) − (;10 · (𝑀↑3))) + (3 · 𝑀)))
2	1	3ad2ant2 1146	. . 3 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → (((3 · 𝑀) − (4 · (𝑀↑3))) · (1 − (2 · (𝑀↑2)))) = (((8 · (𝑀↑5)) − (;10 · (𝑀↑3))) + (3 · 𝑀)))
3		sin5tlem4 47434	. . 3 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → (((4 · (𝑁↑3)) − (3 · 𝑁)) · (2 · (𝑀 · 𝑁))) = ((((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (8 · 𝑀)) − ((6 · 𝑀) − (6 · (𝑀↑3)))))
4	2, 3	oveq12d 7410	. 2 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → ((((3 · 𝑀) − (4 · (𝑀↑3))) · (1 − (2 · (𝑀↑2)))) + (((4 · (𝑁↑3)) − (3 · 𝑁)) · (2 · (𝑀 · 𝑁)))) = ((((8 · (𝑀↑5)) − (;10 · (𝑀↑3))) + (3 · 𝑀)) + ((((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (8 · 𝑀)) − ((6 · 𝑀) − (6 · (𝑀↑3))))))
5		8cn 12312	. . . . . . . . 9 ⊢ 8 ∈ ℂ
6	5	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ ℂ → 8 ∈ ℂ)
7		id 22	. . . . . . . 8 ⊢ (𝑀 ∈ ℂ → 𝑀 ∈ ℂ)
8	6, 7	mulcld 11199	. . . . . . 7 ⊢ (𝑀 ∈ ℂ → (8 · 𝑀) ∈ ℂ)
9		6cn 12306	. . . . . . . . 9 ⊢ 6 ∈ ℂ
10	9	a1i 11	. . . . . . . 8 ⊢ (𝑀 ∈ ℂ → 6 ∈ ℂ)
11	10, 7	mulcld 11199	. . . . . . 7 ⊢ (𝑀 ∈ ℂ → (6 · 𝑀) ∈ ℂ)
12	8, 11	subcld 11539	. . . . . 6 ⊢ (𝑀 ∈ ℂ → ((8 · 𝑀) − (6 · 𝑀)) ∈ ℂ)
13		5nn0 12498	. . . . . . . . . . 11 ⊢ 5 ∈ ℕ₀
14	13	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℂ → 5 ∈ ℕ₀)
15	7, 14	expcld 14156	. . . . . . . . 9 ⊢ (𝑀 ∈ ℂ → (𝑀↑5) ∈ ℂ)
16	6, 15	mulcld 11199	. . . . . . . 8 ⊢ (𝑀 ∈ ℂ → (8 · (𝑀↑5)) ∈ ℂ)
17		16nn0 12703	. . . . . . . . . . 11 ⊢ ;16 ∈ ℕ₀
18	17	nn0cni 12490	. . . . . . . . . 10 ⊢ ;16 ∈ ℂ
19	18	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℂ → ;16 ∈ ℂ)
20		3nn0 12496	. . . . . . . . . . 11 ⊢ 3 ∈ ℕ₀
21	20	a1i 11	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℂ → 3 ∈ ℕ₀)
22	7, 21	expcld 14156	. . . . . . . . 9 ⊢ (𝑀 ∈ ℂ → (𝑀↑3) ∈ ℂ)
23	19, 22	mulcld 11199	. . . . . . . 8 ⊢ (𝑀 ∈ ℂ → (;16 · (𝑀↑3)) ∈ ℂ)
24	16, 23	subcld 11539	. . . . . . 7 ⊢ (𝑀 ∈ ℂ → ((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) ∈ ℂ)
25	10, 22	mulcld 11199	. . . . . . 7 ⊢ (𝑀 ∈ ℂ → (6 · (𝑀↑3)) ∈ ℂ)
26	24, 25	addcld 11198	. . . . . 6 ⊢ (𝑀 ∈ ℂ → (((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (6 · (𝑀↑3))) ∈ ℂ)
27	24, 8	addcomd 11382	. . . . . . . 8 ⊢ (𝑀 ∈ ℂ → (((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (8 · 𝑀)) = ((8 · 𝑀) + ((8 · (𝑀↑5)) − (;16 · (𝑀↑3)))))
28	27	oveq1d 7407	. . . . . . 7 ⊢ (𝑀 ∈ ℂ → ((((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (8 · 𝑀)) − ((6 · 𝑀) − (6 · (𝑀↑3)))) = (((8 · 𝑀) + ((8 · (𝑀↑5)) − (;16 · (𝑀↑3)))) − ((6 · 𝑀) − (6 · (𝑀↑3)))))
29	8, 24, 11, 25	addsubsub23 11592	. . . . . . 7 ⊢ (𝑀 ∈ ℂ → (((8 · 𝑀) + ((8 · (𝑀↑5)) − (;16 · (𝑀↑3)))) − ((6 · 𝑀) − (6 · (𝑀↑3)))) = (((8 · 𝑀) − (6 · 𝑀)) + (((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (6 · (𝑀↑3)))))
30	28, 29	eqtrd 2796	. . . . . 6 ⊢ (𝑀 ∈ ℂ → ((((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (8 · 𝑀)) − ((6 · 𝑀) − (6 · (𝑀↑3)))) = (((8 · 𝑀) − (6 · 𝑀)) + (((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (6 · (𝑀↑3)))))
31	12, 26, 30	comraddd 11394	. . . . 5 ⊢ (𝑀 ∈ ℂ → ((((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (8 · 𝑀)) − ((6 · 𝑀) − (6 · (𝑀↑3)))) = ((((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (6 · (𝑀↑3))) + ((8 · 𝑀) − (6 · 𝑀))))
32	31	oveq2d 7408	. . . 4 ⊢ (𝑀 ∈ ℂ → ((((8 · (𝑀↑5)) − (;10 · (𝑀↑3))) + (3 · 𝑀)) + ((((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (8 · 𝑀)) − ((6 · 𝑀) − (6 · (𝑀↑3))))) = ((((8 · (𝑀↑5)) − (;10 · (𝑀↑3))) + (3 · 𝑀)) + ((((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (6 · (𝑀↑3))) + ((8 · 𝑀) − (6 · 𝑀)))))
33		10nn 12705	. . . . . . . . 9 ⊢ ;10 ∈ ℕ
34	33	nncni 12217	. . . . . . . 8 ⊢ ;10 ∈ ℂ
35	34	a1i 11	. . . . . . 7 ⊢ (𝑀 ∈ ℂ → ;10 ∈ ℂ)
36	35, 22	mulcld 11199	. . . . . 6 ⊢ (𝑀 ∈ ℂ → (;10 · (𝑀↑3)) ∈ ℂ)
37	16, 36	subcld 11539	. . . . 5 ⊢ (𝑀 ∈ ℂ → ((8 · (𝑀↑5)) − (;10 · (𝑀↑3))) ∈ ℂ)
38		3cn 12296	. . . . . . 7 ⊢ 3 ∈ ℂ
39	38	a1i 11	. . . . . 6 ⊢ (𝑀 ∈ ℂ → 3 ∈ ℂ)
40	39, 7	mulcld 11199	. . . . 5 ⊢ (𝑀 ∈ ℂ → (3 · 𝑀) ∈ ℂ)
41	37, 40, 26, 12	add4d 11409	. . . 4 ⊢ (𝑀 ∈ ℂ → ((((8 · (𝑀↑5)) − (;10 · (𝑀↑3))) + (3 · 𝑀)) + ((((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (6 · (𝑀↑3))) + ((8 · 𝑀) − (6 · 𝑀)))) = ((((8 · (𝑀↑5)) − (;10 · (𝑀↑3))) + (((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (6 · (𝑀↑3)))) + ((3 · 𝑀) + ((8 · 𝑀) − (6 · 𝑀)))))
42	16, 16, 36, 36	addsub4d 11586	. . . . . 6 ⊢ (𝑀 ∈ ℂ → (((8 · (𝑀↑5)) + (8 · (𝑀↑5))) − ((;10 · (𝑀↑3)) + (;10 · (𝑀↑3)))) = (((8 · (𝑀↑5)) − (;10 · (𝑀↑3))) + ((8 · (𝑀↑5)) − (;10 · (𝑀↑3)))))
43		8p8e16 12776	. . . . . . . . . . 11 ⊢ (8 + 8) = ;16
44	43	eqcomi 2770	. . . . . . . . . 10 ⊢ ;16 = (8 + 8)
45	44	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℂ → ;16 = (8 + 8))
46	45	oveq1d 7407	. . . . . . . 8 ⊢ (𝑀 ∈ ℂ → (;16 · (𝑀↑5)) = ((8 + 8) · (𝑀↑5)))
47	6, 6, 15	adddird 11204	. . . . . . . 8 ⊢ (𝑀 ∈ ℂ → ((8 + 8) · (𝑀↑5)) = ((8 · (𝑀↑5)) + (8 · (𝑀↑5))))
48	46, 47	eqtrd 2796	. . . . . . 7 ⊢ (𝑀 ∈ ℂ → (;16 · (𝑀↑5)) = ((8 · (𝑀↑5)) + (8 · (𝑀↑5))))
49		10p10e20 12785	. . . . . . . . . . 11 ⊢ (;10 + ;10) = ;20
50	49	eqcomi 2770	. . . . . . . . . 10 ⊢ ;20 = (;10 + ;10)
51	50	a1i 11	. . . . . . . . 9 ⊢ (𝑀 ∈ ℂ → ;20 = (;10 + ;10))
52	51	oveq1d 7407	. . . . . . . 8 ⊢ (𝑀 ∈ ℂ → (;20 · (𝑀↑3)) = ((;10 + ;10) · (𝑀↑3)))
53	35, 35, 22	adddird 11204	. . . . . . . 8 ⊢ (𝑀 ∈ ℂ → ((;10 + ;10) · (𝑀↑3)) = ((;10 · (𝑀↑3)) + (;10 · (𝑀↑3))))
54	52, 53	eqtrd 2796	. . . . . . 7 ⊢ (𝑀 ∈ ℂ → (;20 · (𝑀↑3)) = ((;10 · (𝑀↑3)) + (;10 · (𝑀↑3))))
55	48, 54	oveq12d 7410	. . . . . 6 ⊢ (𝑀 ∈ ℂ → ((;16 · (𝑀↑5)) − (;20 · (𝑀↑3))) = (((8 · (𝑀↑5)) + (8 · (𝑀↑5))) − ((;10 · (𝑀↑3)) + (;10 · (𝑀↑3)))))
56	19, 10, 22	subdird 11641	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℂ → ((;16 − 6) · (𝑀↑3)) = ((;16 · (𝑀↑3)) − (6 · (𝑀↑3))))
57	56	eqcomd 2767	. . . . . . . . 9 ⊢ (𝑀 ∈ ℂ → ((;16 · (𝑀↑3)) − (6 · (𝑀↑3))) = ((;16 − 6) · (𝑀↑3)))
58	57	oveq2d 7408	. . . . . . . 8 ⊢ (𝑀 ∈ ℂ → ((8 · (𝑀↑5)) − ((;16 · (𝑀↑3)) − (6 · (𝑀↑3)))) = ((8 · (𝑀↑5)) − ((;16 − 6) · (𝑀↑3))))
59	16, 23, 25	subsubd 11567	. . . . . . . 8 ⊢ (𝑀 ∈ ℂ → ((8 · (𝑀↑5)) − ((;16 · (𝑀↑3)) − (6 · (𝑀↑3)))) = (((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (6 · (𝑀↑3))))
60		dec10p 12733	. . . . . . . . . . . . 13 ⊢ (;10 + 6) = ;16
61	60	eqcomi 2770	. . . . . . . . . . . 12 ⊢ ;16 = (;10 + 6)
62	61	a1i 11	. . . . . . . . . . 11 ⊢ (𝑀 ∈ ℂ → ;16 = (;10 + 6))
63	35, 10, 62	mvrraddd 11596	. . . . . . . . . 10 ⊢ (𝑀 ∈ ℂ → (;16 − 6) = ;10)
64	63	oveq1d 7407	. . . . . . . . 9 ⊢ (𝑀 ∈ ℂ → ((;16 − 6) · (𝑀↑3)) = (;10 · (𝑀↑3)))
65	64	oveq2d 7408	. . . . . . . 8 ⊢ (𝑀 ∈ ℂ → ((8 · (𝑀↑5)) − ((;16 − 6) · (𝑀↑3))) = ((8 · (𝑀↑5)) − (;10 · (𝑀↑3))))
66	58, 59, 65	3eqtr3d 2804	. . . . . . 7 ⊢ (𝑀 ∈ ℂ → (((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (6 · (𝑀↑3))) = ((8 · (𝑀↑5)) − (;10 · (𝑀↑3))))
67	66	oveq2d 7408	. . . . . 6 ⊢ (𝑀 ∈ ℂ → (((8 · (𝑀↑5)) − (;10 · (𝑀↑3))) + (((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (6 · (𝑀↑3)))) = (((8 · (𝑀↑5)) − (;10 · (𝑀↑3))) + ((8 · (𝑀↑5)) − (;10 · (𝑀↑3)))))
68	42, 55, 67	3eqtr4rd 2807	. . . . 5 ⊢ (𝑀 ∈ ℂ → (((8 · (𝑀↑5)) − (;10 · (𝑀↑3))) + (((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (6 · (𝑀↑3)))) = ((;16 · (𝑀↑5)) − (;20 · (𝑀↑3))))
69	6, 10	subcld 11539	. . . . . . 7 ⊢ (𝑀 ∈ ℂ → (8 − 6) ∈ ℂ)
70	39, 69, 7	adddird 11204	. . . . . 6 ⊢ (𝑀 ∈ ℂ → ((3 + (8 − 6)) · 𝑀) = ((3 · 𝑀) + ((8 − 6) · 𝑀)))
71		2cn 12290	. . . . . . . . . . 11 ⊢ 2 ∈ ℂ
72		6p2e8 12373	. . . . . . . . . . . 12 ⊢ (6 + 2) = 8
73	72	eqcomi 2770	. . . . . . . . . . 11 ⊢ 8 = (6 + 2)
74	9, 71, 73	mvrladdi 11445	. . . . . . . . . 10 ⊢ (8 − 6) = 2
75	74	oveq2i 7403	. . . . . . . . 9 ⊢ (3 + (8 − 6)) = (3 + 2)
76		3p2e5 12365	. . . . . . . . 9 ⊢ (3 + 2) = 5
77	75, 76	eqtri 2784	. . . . . . . 8 ⊢ (3 + (8 − 6)) = 5
78	77	a1i 11	. . . . . . 7 ⊢ (𝑀 ∈ ℂ → (3 + (8 − 6)) = 5)
79	78	oveq1d 7407	. . . . . 6 ⊢ (𝑀 ∈ ℂ → ((3 + (8 − 6)) · 𝑀) = (5 · 𝑀))
80	6, 10, 7	subdird 11641	. . . . . . 7 ⊢ (𝑀 ∈ ℂ → ((8 − 6) · 𝑀) = ((8 · 𝑀) − (6 · 𝑀)))
81	80	oveq2d 7408	. . . . . 6 ⊢ (𝑀 ∈ ℂ → ((3 · 𝑀) + ((8 − 6) · 𝑀)) = ((3 · 𝑀) + ((8 · 𝑀) − (6 · 𝑀))))
82	70, 79, 81	3eqtr3rd 2805	. . . . 5 ⊢ (𝑀 ∈ ℂ → ((3 · 𝑀) + ((8 · 𝑀) − (6 · 𝑀))) = (5 · 𝑀))
83	68, 82	oveq12d 7410	. . . 4 ⊢ (𝑀 ∈ ℂ → ((((8 · (𝑀↑5)) − (;10 · (𝑀↑3))) + (((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (6 · (𝑀↑3)))) + ((3 · 𝑀) + ((8 · 𝑀) − (6 · 𝑀)))) = (((;16 · (𝑀↑5)) − (;20 · (𝑀↑3))) + (5 · 𝑀)))
84	32, 41, 83	3eqtrd 2800	. . 3 ⊢ (𝑀 ∈ ℂ → ((((8 · (𝑀↑5)) − (;10 · (𝑀↑3))) + (3 · 𝑀)) + ((((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (8 · 𝑀)) − ((6 · 𝑀) − (6 · (𝑀↑3))))) = (((;16 · (𝑀↑5)) − (;20 · (𝑀↑3))) + (5 · 𝑀)))
85	84	3ad2ant2 1146	. 2 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → ((((8 · (𝑀↑5)) − (;10 · (𝑀↑3))) + (3 · 𝑀)) + ((((8 · (𝑀↑5)) − (;16 · (𝑀↑3))) + (8 · 𝑀)) − ((6 · 𝑀) − (6 · (𝑀↑3))))) = (((;16 · (𝑀↑5)) − (;20 · (𝑀↑3))) + (5 · 𝑀)))
86	4, 85	eqtrd 2796	1 ⊢ ((𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ (𝑁↑2) = (1 − (𝑀↑2))) → ((((3 · 𝑀) − (4 · (𝑀↑3))) · (1 − (2 · (𝑀↑2)))) + (((4 · (𝑁↑3)) − (3 · 𝑁)) · (2 · (𝑀 · 𝑁)))) = (((;16 · (𝑀↑5)) − (;20 · (𝑀↑3))) + (5 · 𝑀)))

Colors of variables: wff setvar class

Syntax hints: → wi 4 ∧ w3a 1097 = wceq 1559 ∈ wcel 2141 (class class class)co 7392 ℂcc 11068 0cc0 11070 1c1 11071 + caddc 11073 · cmul 11075 − cmin 11411 2c2 12269 3c3 12270 4c4 12271 5c5 12272 6c6 12273 8c8 12275 ℕ₀cn0 12478 cdc 12685 ↑cexp 14071

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1814 ax-4 1828 ax-5 1929 ax-6 1986 ax-7 2027 ax-8 2143 ax-9 2151 ax-10 2174 ax-11 2190 ax-12 2211 ax-ext 2733 ax-sep 5245 ax-nul 5255 ax-pow 5321 ax-pr 5389 ax-un 7714 ax-cnex 11126 ax-resscn 11127 ax-1cn 11128 ax-icn 11129 ax-addcl 11130 ax-addrcl 11131 ax-mulcl 11132 ax-mulrcl 11133 ax-mulcom 11134 ax-addass 11135 ax-mulass 11136 ax-distr 11137 ax-i2m1 11138 ax-1ne0 11139 ax-1rid 11140 ax-rnegex 11141 ax-rrecex 11142 ax-cnre 11143 ax-pre-lttri 11144 ax-pre-lttrn 11145 ax-pre-ltadd 11146 ax-pre-mulgt0 11147

This theorem depends on definitions: df-bi 209 df-an 400 df-or 859 df-3or 1098 df-3an 1099 df-tru 1562 df-fal 1572 df-ex 1799 df-nf 1803 df-sb 2090 df-mo 2565 df-eu 2595 df-clab 2740 df-cleq 2753 df-clel 2836 df-nfc 2910 df-ne 2957 df-nel 3061 df-ral 3076 df-rex 3086 df-rmo 3366 df-reu 3367 df-rab 3414 df-v 3455 df-sbc 3745 df-csb 3853 df-dif 3907 df-un 3909 df-in 3911 df-ss 3921 df-pss 3924 df-nul 4286 df-if 4480 df-pw 4556 df-sn 4582 df-pr 4584 df-op 4588 df-uni 4865 df-iun 4950 df-br 5100 df-opab 5162 df-mpt 5181 df-tr 5207 df-id 5540 df-eprel 5545 df-po 5553 df-so 5554 df-fr 5598 df-we 5600 df-xp 5651 df-rel 5652 df-cnv 5653 df-co 5654 df-dm 5655 df-rn 5656 df-res 5657 df-ima 5658 df-pred 6284 df-ord 6345 df-on 6346 df-lim 6347 df-suc 6348 df-iota 6473 df-fun 6519 df-fn 6520 df-f 6521 df-f1 6522 df-fo 6523 df-f1o 6524 df-fv 6525 df-riota 7349 df-ov 7395 df-oprab 7396 df-mpo 7397 df-om 7843 df-2nd 7967 df-frecs 8257 df-wrecs 8288 df-recs 8337 df-rdg 8376 df-er 8673 df-en 8924 df-dom 8925 df-sdom 8926 df-pnf 11215 df-mnf 11216 df-xr 11217 df-ltxr 11218 df-le 11219 df-sub 11413 df-neg 11414 df-div 11842 df-nn 12208 df-2 12277 df-3 12278 df-4 12279 df-5 12280 df-6 12281 df-7 12282 df-8 12283 df-9 12284 df-n0 12479 df-z 12566 df-dec 12686 df-uz 12837 df-seq 14012 df-exp 14072

This theorem is referenced by: sin5t 47436

W3C validator