sin5tlem2

Description: Lemma 2 for quintupled angle sine calculation, multiplicating triple angle cosine by cosine straight and converting into sine. (Contributed by Ender Ting, 16-Apr-2026)

		Ref	Expression
	Assertion	sin5tlem2	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to (4 N^{3} - 3 \cdot N) \cdot N = 4 (1 - 2 M^{2} + M^{4}) - 3 (1 - M^{2})$

Proof

Step	Hyp	Ref	Expression
1		4cn	$⊢ 4 \in ℂ$
2	1	a1i	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 4 \in ℂ$
3		simp1	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to N \in ℂ$
4		3nn0	$⊢ 3 \in ℕ_{0}$
5	4	a1i	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 3 \in ℕ_{0}$
6	3 5	expcld	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to N^{3} \in ℂ$
7	2 6	mulcld	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 4 N^{3} \in ℂ$
8		3cn	$⊢ 3 \in ℂ$
9	8	a1i	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 3 \in ℂ$
10	9 3	mulcld	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 3 \cdot N \in ℂ$
11	7 10 3	subdird	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to (4 N^{3} - 3 \cdot N) \cdot N = 4 N^{3} \cdot N - 3 \cdot N \cdot N$
12	2 6 3	mulassd	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 4 N^{3} \cdot N = 4 N^{3} \cdot N$
13		2t2e4	$⊢ 2 \cdot 2 = 4$
14		df-4	$⊢ 4 = 3 + 1$
15	13 14	eqtri	$⊢ 2 \cdot 2 = 3 + 1$
16	15	a1i	$⊢ N \in ℂ \to 2 \cdot 2 = 3 + 1$
17	16	oveq2d	$⊢ N \in ℂ \to N^{2 \cdot 2} = N^{3 + 1}$
18		id	$⊢ N \in ℂ \to N \in ℂ$
19		2nn0	$⊢ 2 \in ℕ_{0}$
20	19	a1i	$⊢ N \in ℂ \to 2 \in ℕ_{0}$
21	18 20 20	expmuld	$⊢ N \in ℂ \to N^{2 \cdot 2} = {(N^{2})}^{2}$
22	4	a1i	$⊢ N \in ℂ \to 3 \in ℕ_{0}$
23	18 22	expp1d	$⊢ N \in ℂ \to N^{3 + 1} = N^{3} \cdot N$
24	17 21 23	3eqtr3rd	$⊢ N \in ℂ \to N^{3} \cdot N = {(N^{2})}^{2}$
25	24	3ad2ant1	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to N^{3} \cdot N = {(N^{2})}^{2}$
26	25	oveq2d	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 4 N^{3} \cdot N = 4 {(N^{2})}^{2}$
27		oveq1	$⊢ N^{2} = 1 - M^{2} \to {(N^{2})}^{2} = {(1 - M^{2})}^{2}$
28	27	oveq2d	$⊢ N^{2} = 1 - M^{2} \to 4 {(N^{2})}^{2} = 4 {(1 - M^{2})}^{2}$
29	28	3ad2ant3	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 4 {(N^{2})}^{2} = 4 {(1 - M^{2})}^{2}$
30	12 26 29	3eqtrd	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 4 N^{3} \cdot N = 4 {(1 - M^{2})}^{2}$
31		1cnd	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 1 \in ℂ$
32		simp2	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to M \in ℂ$
33	19	a1i	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 2 \in ℕ_{0}$
34	32 33	expcld	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to M^{2} \in ℂ$
35		binom2sub	$⊢ (1 \in ℂ \land M^{2} \in ℂ) \to {(1 - M^{2})}^{2} = 1^{2} - 2 1 M^{2} + {(M^{2})}^{2}$
36	31 34 35	syl2anc	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to {(1 - M^{2})}^{2} = 1^{2} - 2 1 M^{2} + {(M^{2})}^{2}$
37		sq1	$⊢ 1^{2} = 1$
38	37	a1i	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 1^{2} = 1$
39	34	mullidd	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 1 M^{2} = M^{2}$
40	39	oveq2d	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 2 1 M^{2} = 2 M^{2}$
41	38 40	oveq12d	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 1^{2} - 2 1 M^{2} = 1 - 2 M^{2}$
42	13	eqcomi	$⊢ 4 = 2 \cdot 2$
43	42	a1i	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 4 = 2 \cdot 2$
44	43	oveq2d	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to M^{4} = M^{2 \cdot 2}$
45	32 33 33	expmuld	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to M^{2 \cdot 2} = {(M^{2})}^{2}$
46	44 45	eqtr2d	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to {(M^{2})}^{2} = M^{4}$
47	41 46	oveq12d	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 1^{2} - 2 1 M^{2} + {(M^{2})}^{2} = 1 - 2 M^{2} + M^{4}$
48	36 47	eqtrd	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to {(1 - M^{2})}^{2} = 1 - 2 M^{2} + M^{4}$
49	48	oveq2d	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 4 {(1 - M^{2})}^{2} = 4 (1 - 2 M^{2} + M^{4})$
50	30 49	eqtrd	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 4 N^{3} \cdot N = 4 (1 - 2 M^{2} + M^{4})$
51	9 3 3	mulassd	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 3 \cdot N \cdot N = 3 N \cdot N$
52		sqval	$⊢ N \in ℂ \to N^{2} = N \cdot N$
53	52	eqcomd	$⊢ N \in ℂ \to N \cdot N = N^{2}$
54	53	3ad2ant1	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to N \cdot N = N^{2}$
55	54	oveq2d	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 3 N \cdot N = 3 N^{2}$
56		oveq2	$⊢ N^{2} = 1 - M^{2} \to 3 N^{2} = 3 (1 - M^{2})$
57	56	3ad2ant3	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 3 N^{2} = 3 (1 - M^{2})$
58	51 55 57	3eqtrd	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 3 \cdot N \cdot N = 3 (1 - M^{2})$
59	50 58	oveq12d	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to 4 N^{3} \cdot N - 3 \cdot N \cdot N = 4 (1 - 2 M^{2} + M^{4}) - 3 (1 - M^{2})$
60	11 59	eqtrd	$⊢ (N \in ℂ \land M \in ℂ \land N^{2} = 1 - M^{2}) \to (4 N^{3} - 3 \cdot N) \cdot N = 4 (1 - 2 M^{2} + M^{4}) - 3 (1 - M^{2})$

Metamath Proof Explorer

Theorem sin5tlem2

Proof