Metamath Proof Explorer

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 ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · ( 2 · ( 𝑀 · 𝑁 ) ) ) = ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 8 · 𝑀 ) ) − ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 sin5tlem3 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · ( 2 · ( 𝑀 · 𝑁 ) ) ) = ( ( ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) − ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) ) · ( 2 · 𝑀 ) ) )
2 4cn ⊢ 4 ∈ ℂ
3 2 a1i ⊢ ( 𝑀 ∈ ℂ → 4 ∈ ℂ )
4 1cnd ⊢ ( 𝑀 ∈ ℂ → 1 ∈ ℂ )
5 2cnd ⊢ ( 𝑀 ∈ ℂ → 2 ∈ ℂ )
6 sqcl ⊢ ( 𝑀 ∈ ℂ → ( 𝑀 ↑ 2 ) ∈ ℂ )
7 5 6 mulcld ⊢ ( 𝑀 ∈ ℂ → ( 2 · ( 𝑀 ↑ 2 ) ) ∈ ℂ )
8 4 7 subcld ⊢ ( 𝑀 ∈ ℂ → ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) ∈ ℂ )
9 id ⊢ ( 𝑀 ∈ ℂ → 𝑀 ∈ ℂ )
10 4nn0 ⊢ 4 ∈ ℕ0
11 10 a1i ⊢ ( 𝑀 ∈ ℂ → 4 ∈ ℕ0 )
12 9 11 expcld ⊢ ( 𝑀 ∈ ℂ → ( 𝑀 ↑ 4 ) ∈ ℂ )
13 8 12 addcld ⊢ ( 𝑀 ∈ ℂ → ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ∈ ℂ )
14 3 13 mulcld ⊢ ( 𝑀 ∈ ℂ → ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) ∈ ℂ )
15 3cn ⊢ 3 ∈ ℂ
16 15 a1i ⊢ ( 𝑀 ∈ ℂ → 3 ∈ ℂ )
17 4 6 subcld ⊢ ( 𝑀 ∈ ℂ → ( 1 − ( 𝑀 ↑ 2 ) ) ∈ ℂ )
18 16 17 mulcld ⊢ ( 𝑀 ∈ ℂ → ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) ∈ ℂ )
19 5 9 mulcld ⊢ ( 𝑀 ∈ ℂ → ( 2 · 𝑀 ) ∈ ℂ )
20 14 18 19 subdird ⊢ ( 𝑀 ∈ ℂ → ( ( ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) − ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) ) · ( 2 · 𝑀 ) ) = ( ( ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) · ( 2 · 𝑀 ) ) − ( ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) · ( 2 · 𝑀 ) ) ) )
21 3 13 5 9 mul4d ⊢ ( 𝑀 ∈ ℂ → ( ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) · ( 2 · 𝑀 ) ) = ( ( 4 · 2 ) · ( ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) · 𝑀 ) ) )
22 4t2e8 ⊢ ( 4 · 2 ) = 8
23 22 a1i ⊢ ( 𝑀 ∈ ℂ → ( 4 · 2 ) = 8 )
24 23 oveq1d ⊢ ( 𝑀 ∈ ℂ → ( ( 4 · 2 ) · ( ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) · 𝑀 ) ) = ( 8 · ( ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) · 𝑀 ) ) )
25 4 12 7 addsubd ⊢ ( 𝑀 ∈ ℂ → ( ( 1 + ( 𝑀 ↑ 4 ) ) − ( 2 · ( 𝑀 ↑ 2 ) ) ) = ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) )
26 25 eqcomd ⊢ ( 𝑀 ∈ ℂ → ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) = ( ( 1 + ( 𝑀 ↑ 4 ) ) − ( 2 · ( 𝑀 ↑ 2 ) ) ) )
27 26 oveq1d ⊢ ( 𝑀 ∈ ℂ → ( ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) · 𝑀 ) = ( ( ( 1 + ( 𝑀 ↑ 4 ) ) − ( 2 · ( 𝑀 ↑ 2 ) ) ) · 𝑀 ) )
28 4 12 addcld ⊢ ( 𝑀 ∈ ℂ → ( 1 + ( 𝑀 ↑ 4 ) ) ∈ ℂ )
29 28 7 9 subdird ⊢ ( 𝑀 ∈ ℂ → ( ( ( 1 + ( 𝑀 ↑ 4 ) ) − ( 2 · ( 𝑀 ↑ 2 ) ) ) · 𝑀 ) = ( ( ( 1 + ( 𝑀 ↑ 4 ) ) · 𝑀 ) − ( ( 2 · ( 𝑀 ↑ 2 ) ) · 𝑀 ) ) )
30 5nn0 ⊢ 5 ∈ ℕ0
31 30 a1i ⊢ ( 𝑀 ∈ ℂ → 5 ∈ ℕ0 )
32 9 31 expcld ⊢ ( 𝑀 ∈ ℂ → ( 𝑀 ↑ 5 ) ∈ ℂ )
33 mullid ⊢ ( 𝑀 ∈ ℂ → ( 1 · 𝑀 ) = 𝑀 )
34 9 11 expp1d ⊢ ( 𝑀 ∈ ℂ → ( 𝑀 ↑ ( 4 + 1 ) ) = ( ( 𝑀 ↑ 4 ) · 𝑀 ) )
35 4p1e5 ⊢ ( 4 + 1 ) = 5
36 35 a1i ⊢ ( 𝑀 ∈ ℂ → ( 4 + 1 ) = 5 )
37 36 oveq2d ⊢ ( 𝑀 ∈ ℂ → ( 𝑀 ↑ ( 4 + 1 ) ) = ( 𝑀 ↑ 5 ) )
38 34 37 eqtr3d ⊢ ( 𝑀 ∈ ℂ → ( ( 𝑀 ↑ 4 ) · 𝑀 ) = ( 𝑀 ↑ 5 ) )
39 33 38 oveq12d ⊢ ( 𝑀 ∈ ℂ → ( ( 1 · 𝑀 ) + ( ( 𝑀 ↑ 4 ) · 𝑀 ) ) = ( 𝑀 + ( 𝑀 ↑ 5 ) ) )
40 4 9 12 39 joinlmuladdmuld ⊢ ( 𝑀 ∈ ℂ → ( ( 1 + ( 𝑀 ↑ 4 ) ) · 𝑀 ) = ( 𝑀 + ( 𝑀 ↑ 5 ) ) )
41 9 32 40 comraddd ⊢ ( 𝑀 ∈ ℂ → ( ( 1 + ( 𝑀 ↑ 4 ) ) · 𝑀 ) = ( ( 𝑀 ↑ 5 ) + 𝑀 ) )
42 5 6 9 mulassd ⊢ ( 𝑀 ∈ ℂ → ( ( 2 · ( 𝑀 ↑ 2 ) ) · 𝑀 ) = ( 2 · ( ( 𝑀 ↑ 2 ) · 𝑀 ) ) )
43 2nn0 ⊢ 2 ∈ ℕ0
44 43 a1i ⊢ ( 𝑀 ∈ ℂ → 2 ∈ ℕ0 )
45 9 44 expp1d ⊢ ( 𝑀 ∈ ℂ → ( 𝑀 ↑ ( 2 + 1 ) ) = ( ( 𝑀 ↑ 2 ) · 𝑀 ) )
46 2p1e3 ⊢ ( 2 + 1 ) = 3
47 46 a1i ⊢ ( 𝑀 ∈ ℂ → ( 2 + 1 ) = 3 )
48 47 oveq2d ⊢ ( 𝑀 ∈ ℂ → ( 𝑀 ↑ ( 2 + 1 ) ) = ( 𝑀 ↑ 3 ) )
49 45 48 eqtr3d ⊢ ( 𝑀 ∈ ℂ → ( ( 𝑀 ↑ 2 ) · 𝑀 ) = ( 𝑀 ↑ 3 ) )
50 49 oveq2d ⊢ ( 𝑀 ∈ ℂ → ( 2 · ( ( 𝑀 ↑ 2 ) · 𝑀 ) ) = ( 2 · ( 𝑀 ↑ 3 ) ) )
51 42 50 eqtrd ⊢ ( 𝑀 ∈ ℂ → ( ( 2 · ( 𝑀 ↑ 2 ) ) · 𝑀 ) = ( 2 · ( 𝑀 ↑ 3 ) ) )
52 41 51 oveq12d ⊢ ( 𝑀 ∈ ℂ → ( ( ( 1 + ( 𝑀 ↑ 4 ) ) · 𝑀 ) − ( ( 2 · ( 𝑀 ↑ 2 ) ) · 𝑀 ) ) = ( ( ( 𝑀 ↑ 5 ) + 𝑀 ) − ( 2 · ( 𝑀 ↑ 3 ) ) ) )
53 27 29 52 3eqtrd ⊢ ( 𝑀 ∈ ℂ → ( ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) · 𝑀 ) = ( ( ( 𝑀 ↑ 5 ) + 𝑀 ) − ( 2 · ( 𝑀 ↑ 3 ) ) ) )
54 53 oveq2d ⊢ ( 𝑀 ∈ ℂ → ( 8 · ( ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) · 𝑀 ) ) = ( 8 · ( ( ( 𝑀 ↑ 5 ) + 𝑀 ) − ( 2 · ( 𝑀 ↑ 3 ) ) ) ) )
55 8cn ⊢ 8 ∈ ℂ
56 55 a1i ⊢ ( 𝑀 ∈ ℂ → 8 ∈ ℂ )
57 32 9 addcld ⊢ ( 𝑀 ∈ ℂ → ( ( 𝑀 ↑ 5 ) + 𝑀 ) ∈ ℂ )
58 3nn0 ⊢ 3 ∈ ℕ0
59 58 a1i ⊢ ( 𝑀 ∈ ℂ → 3 ∈ ℕ0 )
60 9 59 expcld ⊢ ( 𝑀 ∈ ℂ → ( 𝑀 ↑ 3 ) ∈ ℂ )
61 5 60 mulcld ⊢ ( 𝑀 ∈ ℂ → ( 2 · ( 𝑀 ↑ 3 ) ) ∈ ℂ )
62 56 57 61 subdid ⊢ ( 𝑀 ∈ ℂ → ( 8 · ( ( ( 𝑀 ↑ 5 ) + 𝑀 ) − ( 2 · ( 𝑀 ↑ 3 ) ) ) ) = ( ( 8 · ( ( 𝑀 ↑ 5 ) + 𝑀 ) ) − ( 8 · ( 2 · ( 𝑀 ↑ 3 ) ) ) ) )
63 56 5 60 mulassd ⊢ ( 𝑀 ∈ ℂ → ( ( 8 · 2 ) · ( 𝑀 ↑ 3 ) ) = ( 8 · ( 2 · ( 𝑀 ↑ 3 ) ) ) )
64 63 eqcomd ⊢ ( 𝑀 ∈ ℂ → ( 8 · ( 2 · ( 𝑀 ↑ 3 ) ) ) = ( ( 8 · 2 ) · ( 𝑀 ↑ 3 ) ) )
65 64 oveq2d ⊢ ( 𝑀 ∈ ℂ → ( ( 8 · ( ( 𝑀 ↑ 5 ) + 𝑀 ) ) − ( 8 · ( 2 · ( 𝑀 ↑ 3 ) ) ) ) = ( ( 8 · ( ( 𝑀 ↑ 5 ) + 𝑀 ) ) − ( ( 8 · 2 ) · ( 𝑀 ↑ 3 ) ) ) )
66 54 62 65 3eqtrd ⊢ ( 𝑀 ∈ ℂ → ( 8 · ( ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) · 𝑀 ) ) = ( ( 8 · ( ( 𝑀 ↑ 5 ) + 𝑀 ) ) − ( ( 8 · 2 ) · ( 𝑀 ↑ 3 ) ) ) )
67 56 32 9 adddid ⊢ ( 𝑀 ∈ ℂ → ( 8 · ( ( 𝑀 ↑ 5 ) + 𝑀 ) ) = ( ( 8 · ( 𝑀 ↑ 5 ) ) + ( 8 · 𝑀 ) ) )
68 8t2e16 ⊢ ( 8 · 2 ) = 1 6
69 68 a1i ⊢ ( 𝑀 ∈ ℂ → ( 8 · 2 ) = 1 6 )
70 69 oveq1d ⊢ ( 𝑀 ∈ ℂ → ( ( 8 · 2 ) · ( 𝑀 ↑ 3 ) ) = ( 1 6 · ( 𝑀 ↑ 3 ) ) )
71 67 70 oveq12d ⊢ ( 𝑀 ∈ ℂ → ( ( 8 · ( ( 𝑀 ↑ 5 ) + 𝑀 ) ) − ( ( 8 · 2 ) · ( 𝑀 ↑ 3 ) ) ) = ( ( ( 8 · ( 𝑀 ↑ 5 ) ) + ( 8 · 𝑀 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) )
72 24 66 71 3eqtrd ⊢ ( 𝑀 ∈ ℂ → ( ( 4 · 2 ) · ( ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) · 𝑀 ) ) = ( ( ( 8 · ( 𝑀 ↑ 5 ) ) + ( 8 · 𝑀 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) )
73 56 32 mulcld ⊢ ( 𝑀 ∈ ℂ → ( 8 · ( 𝑀 ↑ 5 ) ) ∈ ℂ )
74 56 9 mulcld ⊢ ( 𝑀 ∈ ℂ → ( 8 · 𝑀 ) ∈ ℂ )
75 1nn0 ⊢ 1 ∈ ℕ0
76 6nn0 ⊢ 6 ∈ ℕ0
77 75 76 deccl ⊢ 1 6 ∈ ℕ0
78 77 nn0cni ⊢ 1 6 ∈ ℂ
79 78 a1i ⊢ ( 𝑀 ∈ ℂ → 1 6 ∈ ℂ )
80 79 60 mulcld ⊢ ( 𝑀 ∈ ℂ → ( 1 6 · ( 𝑀 ↑ 3 ) ) ∈ ℂ )
81 73 74 80 addsubd ⊢ ( 𝑀 ∈ ℂ → ( ( ( 8 · ( 𝑀 ↑ 5 ) ) + ( 8 · 𝑀 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) = ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 8 · 𝑀 ) ) )
82 21 72 81 3eqtrd ⊢ ( 𝑀 ∈ ℂ → ( ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) · ( 2 · 𝑀 ) ) = ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 8 · 𝑀 ) ) )
83 16 17 5 9 mul4d ⊢ ( 𝑀 ∈ ℂ → ( ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) · ( 2 · 𝑀 ) ) = ( ( 3 · 2 ) · ( ( 1 − ( 𝑀 ↑ 2 ) ) · 𝑀 ) ) )
84 3t2e6 ⊢ ( 3 · 2 ) = 6
85 84 a1i ⊢ ( 𝑀 ∈ ℂ → ( 3 · 2 ) = 6 )
86 4 6 9 subdird ⊢ ( 𝑀 ∈ ℂ → ( ( 1 − ( 𝑀 ↑ 2 ) ) · 𝑀 ) = ( ( 1 · 𝑀 ) − ( ( 𝑀 ↑ 2 ) · 𝑀 ) ) )
87 33 49 oveq12d ⊢ ( 𝑀 ∈ ℂ → ( ( 1 · 𝑀 ) − ( ( 𝑀 ↑ 2 ) · 𝑀 ) ) = ( 𝑀 − ( 𝑀 ↑ 3 ) ) )
88 86 87 eqtrd ⊢ ( 𝑀 ∈ ℂ → ( ( 1 − ( 𝑀 ↑ 2 ) ) · 𝑀 ) = ( 𝑀 − ( 𝑀 ↑ 3 ) ) )
89 85 88 oveq12d ⊢ ( 𝑀 ∈ ℂ → ( ( 3 · 2 ) · ( ( 1 − ( 𝑀 ↑ 2 ) ) · 𝑀 ) ) = ( 6 · ( 𝑀 − ( 𝑀 ↑ 3 ) ) ) )
90 6cn ⊢ 6 ∈ ℂ
91 90 a1i ⊢ ( 𝑀 ∈ ℂ → 6 ∈ ℂ )
92 91 9 60 subdid ⊢ ( 𝑀 ∈ ℂ → ( 6 · ( 𝑀 − ( 𝑀 ↑ 3 ) ) ) = ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) )
93 83 89 92 3eqtrd ⊢ ( 𝑀 ∈ ℂ → ( ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) · ( 2 · 𝑀 ) ) = ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) )
94 82 93 oveq12d ⊢ ( 𝑀 ∈ ℂ → ( ( ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) · ( 2 · 𝑀 ) ) − ( ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) · ( 2 · 𝑀 ) ) ) = ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 8 · 𝑀 ) ) − ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) )
95 20 94 eqtrd ⊢ ( 𝑀 ∈ ℂ → ( ( ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) − ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) ) · ( 2 · 𝑀 ) ) = ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 8 · 𝑀 ) ) − ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) )
96 95 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( 4 · ( ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) + ( 𝑀 ↑ 4 ) ) ) − ( 3 · ( 1 − ( 𝑀 ↑ 2 ) ) ) ) · ( 2 · 𝑀 ) ) = ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 8 · 𝑀 ) ) − ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) )
97 1 96 eqtrd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · ( 2 · ( 𝑀 · 𝑁 ) ) ) = ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 8 · 𝑀 ) ) − ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) )