Metamath Proof Explorer

Theorem sin5tlem5

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)

Ref Expression
Assertion sin5tlem5 ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( ( 3 · 𝑀 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) · ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) ) + ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · ( 2 · ( 𝑀 · 𝑁 ) ) ) ) = ( ( ( 1 6 · ( 𝑀 ↑ 5 ) ) − ( 2 0 · ( 𝑀 ↑ 3 ) ) ) + ( 5 · 𝑀 ) ) )

Proof

Step Hyp Ref Expression
1 sin5tlem1 ⊢ ( 𝑀 ∈ ℂ → ( ( ( 3 · 𝑀 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) · ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) ) = ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) + ( 3 · 𝑀 ) ) )
2 1 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( 3 · 𝑀 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) · ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) ) = ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) + ( 3 · 𝑀 ) ) )
3 sin5tlem4 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · ( 2 · ( 𝑀 · 𝑁 ) ) ) = ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 8 · 𝑀 ) ) − ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) )
4 2 3 oveq12d ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( ( 3 · 𝑀 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) · ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) ) + ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · ( 2 · ( 𝑀 · 𝑁 ) ) ) ) = ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) + ( 3 · 𝑀 ) ) + ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 8 · 𝑀 ) ) − ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) ) )
5 8cn ⊢ 8 ∈ ℂ
6 5 a1i ⊢ ( 𝑀 ∈ ℂ → 8 ∈ ℂ )
7 id ⊢ ( 𝑀 ∈ ℂ → 𝑀 ∈ ℂ )
8 6 7 mulcld ⊢ ( 𝑀 ∈ ℂ → ( 8 · 𝑀 ) ∈ ℂ )
9 6cn ⊢ 6 ∈ ℂ
10 9 a1i ⊢ ( 𝑀 ∈ ℂ → 6 ∈ ℂ )
11 10 7 mulcld ⊢ ( 𝑀 ∈ ℂ → ( 6 · 𝑀 ) ∈ ℂ )
12 8 11 subcld ⊢ ( 𝑀 ∈ ℂ → ( ( 8 · 𝑀 ) − ( 6 · 𝑀 ) ) ∈ ℂ )
13 5nn0 ⊢ 5 ∈ ℕ0
14 13 a1i ⊢ ( 𝑀 ∈ ℂ → 5 ∈ ℕ0 )
15 7 14 expcld ⊢ ( 𝑀 ∈ ℂ → ( 𝑀 ↑ 5 ) ∈ ℂ )
16 6 15 mulcld ⊢ ( 𝑀 ∈ ℂ → ( 8 · ( 𝑀 ↑ 5 ) ) ∈ ℂ )
17 1nn0 ⊢ 1 ∈ ℕ0
18 6nn0 ⊢ 6 ∈ ℕ0
19 17 18 deccl ⊢ 1 6 ∈ ℕ0
20 19 nn0cni ⊢ 1 6 ∈ ℂ
21 20 a1i ⊢ ( 𝑀 ∈ ℂ → 1 6 ∈ ℂ )
22 3nn0 ⊢ 3 ∈ ℕ0
23 22 a1i ⊢ ( 𝑀 ∈ ℂ → 3 ∈ ℕ0 )
24 7 23 expcld ⊢ ( 𝑀 ∈ ℂ → ( 𝑀 ↑ 3 ) ∈ ℂ )
25 21 24 mulcld ⊢ ( 𝑀 ∈ ℂ → ( 1 6 · ( 𝑀 ↑ 3 ) ) ∈ ℂ )
26 16 25 subcld ⊢ ( 𝑀 ∈ ℂ → ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) ∈ ℂ )
27 10 24 mulcld ⊢ ( 𝑀 ∈ ℂ → ( 6 · ( 𝑀 ↑ 3 ) ) ∈ ℂ )
28 26 27 addcld ⊢ ( 𝑀 ∈ ℂ → ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 6 · ( 𝑀 ↑ 3 ) ) ) ∈ ℂ )
29 26 8 addcomd ⊢ ( 𝑀 ∈ ℂ → ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 8 · 𝑀 ) ) = ( ( 8 · 𝑀 ) + ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) ) )
30 29 oveq1d ⊢ ( 𝑀 ∈ ℂ → ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 8 · 𝑀 ) ) − ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) = ( ( ( 8 · 𝑀 ) + ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) ) − ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) )
31 8 26 11 27 addsubsub23 ⊢ ( 𝑀 ∈ ℂ → ( ( ( 8 · 𝑀 ) + ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) ) − ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) = ( ( ( 8 · 𝑀 ) − ( 6 · 𝑀 ) ) + ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 6 · ( 𝑀 ↑ 3 ) ) ) ) )
32 30 31 eqtrd ⊢ ( 𝑀 ∈ ℂ → ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 8 · 𝑀 ) ) − ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) = ( ( ( 8 · 𝑀 ) − ( 6 · 𝑀 ) ) + ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 6 · ( 𝑀 ↑ 3 ) ) ) ) )
33 12 28 32 comraddd ⊢ ( 𝑀 ∈ ℂ → ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 8 · 𝑀 ) ) − ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) = ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 6 · ( 𝑀 ↑ 3 ) ) ) + ( ( 8 · 𝑀 ) − ( 6 · 𝑀 ) ) ) )
34 33 oveq2d ⊢ ( 𝑀 ∈ ℂ → ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) + ( 3 · 𝑀 ) ) + ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 8 · 𝑀 ) ) − ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) ) = ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) + ( 3 · 𝑀 ) ) + ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 6 · ( 𝑀 ↑ 3 ) ) ) + ( ( 8 · 𝑀 ) − ( 6 · 𝑀 ) ) ) ) )
35 10nn ⊢ 1 0 ∈ ℕ
36 35 nncni ⊢ 1 0 ∈ ℂ
37 36 a1i ⊢ ( 𝑀 ∈ ℂ → 1 0 ∈ ℂ )
38 37 24 mulcld ⊢ ( 𝑀 ∈ ℂ → ( 1 0 · ( 𝑀 ↑ 3 ) ) ∈ ℂ )
39 16 38 subcld ⊢ ( 𝑀 ∈ ℂ → ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) ∈ ℂ )
40 3cn ⊢ 3 ∈ ℂ
41 40 a1i ⊢ ( 𝑀 ∈ ℂ → 3 ∈ ℂ )
42 41 7 mulcld ⊢ ( 𝑀 ∈ ℂ → ( 3 · 𝑀 ) ∈ ℂ )
43 39 42 28 12 add4d ⊢ ( 𝑀 ∈ ℂ → ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) + ( 3 · 𝑀 ) ) + ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 6 · ( 𝑀 ↑ 3 ) ) ) + ( ( 8 · 𝑀 ) − ( 6 · 𝑀 ) ) ) ) = ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) + ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 6 · ( 𝑀 ↑ 3 ) ) ) ) + ( ( 3 · 𝑀 ) + ( ( 8 · 𝑀 ) − ( 6 · 𝑀 ) ) ) ) )
44 16 16 38 38 addsub4d ⊢ ( 𝑀 ∈ ℂ → ( ( ( 8 · ( 𝑀 ↑ 5 ) ) + ( 8 · ( 𝑀 ↑ 5 ) ) ) − ( ( 1 0 · ( 𝑀 ↑ 3 ) ) + ( 1 0 · ( 𝑀 ↑ 3 ) ) ) ) = ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) + ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) ) )
45 8p8e16 ⊢ ( 8 + 8 ) = 1 6
46 45 eqcomi ⊢ 1 6 = ( 8 + 8 )
47 46 a1i ⊢ ( 𝑀 ∈ ℂ → 1 6 = ( 8 + 8 ) )
48 47 oveq1d ⊢ ( 𝑀 ∈ ℂ → ( 1 6 · ( 𝑀 ↑ 5 ) ) = ( ( 8 + 8 ) · ( 𝑀 ↑ 5 ) ) )
49 6 6 15 adddird ⊢ ( 𝑀 ∈ ℂ → ( ( 8 + 8 ) · ( 𝑀 ↑ 5 ) ) = ( ( 8 · ( 𝑀 ↑ 5 ) ) + ( 8 · ( 𝑀 ↑ 5 ) ) ) )
50 48 49 eqtrd ⊢ ( 𝑀 ∈ ℂ → ( 1 6 · ( 𝑀 ↑ 5 ) ) = ( ( 8 · ( 𝑀 ↑ 5 ) ) + ( 8 · ( 𝑀 ↑ 5 ) ) ) )
51 10p10e20 ⊢ ( 1 0 + 1 0 ) = 2 0
52 51 eqcomi ⊢ 2 0 = ( 1 0 + 1 0 )
53 52 a1i ⊢ ( 𝑀 ∈ ℂ → 2 0 = ( 1 0 + 1 0 ) )
54 53 oveq1d ⊢ ( 𝑀 ∈ ℂ → ( 2 0 · ( 𝑀 ↑ 3 ) ) = ( ( 1 0 + 1 0 ) · ( 𝑀 ↑ 3 ) ) )
55 37 37 24 adddird ⊢ ( 𝑀 ∈ ℂ → ( ( 1 0 + 1 0 ) · ( 𝑀 ↑ 3 ) ) = ( ( 1 0 · ( 𝑀 ↑ 3 ) ) + ( 1 0 · ( 𝑀 ↑ 3 ) ) ) )
56 54 55 eqtrd ⊢ ( 𝑀 ∈ ℂ → ( 2 0 · ( 𝑀 ↑ 3 ) ) = ( ( 1 0 · ( 𝑀 ↑ 3 ) ) + ( 1 0 · ( 𝑀 ↑ 3 ) ) ) )
57 50 56 oveq12d ⊢ ( 𝑀 ∈ ℂ → ( ( 1 6 · ( 𝑀 ↑ 5 ) ) − ( 2 0 · ( 𝑀 ↑ 3 ) ) ) = ( ( ( 8 · ( 𝑀 ↑ 5 ) ) + ( 8 · ( 𝑀 ↑ 5 ) ) ) − ( ( 1 0 · ( 𝑀 ↑ 3 ) ) + ( 1 0 · ( 𝑀 ↑ 3 ) ) ) ) )
58 21 10 24 subdird ⊢ ( 𝑀 ∈ ℂ → ( ( 1 6 − 6 ) · ( 𝑀 ↑ 3 ) ) = ( ( 1 6 · ( 𝑀 ↑ 3 ) ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) )
59 58 eqcomd ⊢ ( 𝑀 ∈ ℂ → ( ( 1 6 · ( 𝑀 ↑ 3 ) ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) = ( ( 1 6 − 6 ) · ( 𝑀 ↑ 3 ) ) )
60 59 oveq2d ⊢ ( 𝑀 ∈ ℂ → ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( ( 1 6 · ( 𝑀 ↑ 3 ) ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) = ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( ( 1 6 − 6 ) · ( 𝑀 ↑ 3 ) ) ) )
61 16 25 27 subsubd ⊢ ( 𝑀 ∈ ℂ → ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( ( 1 6 · ( 𝑀 ↑ 3 ) ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) = ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 6 · ( 𝑀 ↑ 3 ) ) ) )
62 dec10p ⊢ ( 1 0 + 6 ) = 1 6
63 62 eqcomi ⊢ 1 6 = ( 1 0 + 6 )
64 63 a1i ⊢ ( 𝑀 ∈ ℂ → 1 6 = ( 1 0 + 6 ) )
65 37 10 64 mvrraddd ⊢ ( 𝑀 ∈ ℂ → ( 1 6 − 6 ) = 1 0 )
66 65 oveq1d ⊢ ( 𝑀 ∈ ℂ → ( ( 1 6 − 6 ) · ( 𝑀 ↑ 3 ) ) = ( 1 0 · ( 𝑀 ↑ 3 ) ) )
67 66 oveq2d ⊢ ( 𝑀 ∈ ℂ → ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( ( 1 6 − 6 ) · ( 𝑀 ↑ 3 ) ) ) = ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) )
68 60 61 67 3eqtr3d ⊢ ( 𝑀 ∈ ℂ → ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 6 · ( 𝑀 ↑ 3 ) ) ) = ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) )
69 68 oveq2d ⊢ ( 𝑀 ∈ ℂ → ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) + ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 6 · ( 𝑀 ↑ 3 ) ) ) ) = ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) + ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) ) )
70 44 57 69 3eqtr4rd ⊢ ( 𝑀 ∈ ℂ → ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) + ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 6 · ( 𝑀 ↑ 3 ) ) ) ) = ( ( 1 6 · ( 𝑀 ↑ 5 ) ) − ( 2 0 · ( 𝑀 ↑ 3 ) ) ) )
71 6 10 subcld ⊢ ( 𝑀 ∈ ℂ → ( 8 − 6 ) ∈ ℂ )
72 41 71 7 adddird ⊢ ( 𝑀 ∈ ℂ → ( ( 3 + ( 8 − 6 ) ) · 𝑀 ) = ( ( 3 · 𝑀 ) + ( ( 8 − 6 ) · 𝑀 ) ) )
73 2cn ⊢ 2 ∈ ℂ
74 6p2e8 ⊢ ( 6 + 2 ) = 8
75 74 eqcomi ⊢ 8 = ( 6 + 2 )
76 9 73 75 mvrladdi ⊢ ( 8 − 6 ) = 2
77 76 oveq2i ⊢ ( 3 + ( 8 − 6 ) ) = ( 3 + 2 )
78 3p2e5 ⊢ ( 3 + 2 ) = 5
79 77 78 eqtri ⊢ ( 3 + ( 8 − 6 ) ) = 5
80 79 a1i ⊢ ( 𝑀 ∈ ℂ → ( 3 + ( 8 − 6 ) ) = 5 )
81 80 oveq1d ⊢ ( 𝑀 ∈ ℂ → ( ( 3 + ( 8 − 6 ) ) · 𝑀 ) = ( 5 · 𝑀 ) )
82 6 10 7 subdird ⊢ ( 𝑀 ∈ ℂ → ( ( 8 − 6 ) · 𝑀 ) = ( ( 8 · 𝑀 ) − ( 6 · 𝑀 ) ) )
83 82 oveq2d ⊢ ( 𝑀 ∈ ℂ → ( ( 3 · 𝑀 ) + ( ( 8 − 6 ) · 𝑀 ) ) = ( ( 3 · 𝑀 ) + ( ( 8 · 𝑀 ) − ( 6 · 𝑀 ) ) ) )
84 72 81 83 3eqtr3rd ⊢ ( 𝑀 ∈ ℂ → ( ( 3 · 𝑀 ) + ( ( 8 · 𝑀 ) − ( 6 · 𝑀 ) ) ) = ( 5 · 𝑀 ) )
85 70 84 oveq12d ⊢ ( 𝑀 ∈ ℂ → ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) + ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 6 · ( 𝑀 ↑ 3 ) ) ) ) + ( ( 3 · 𝑀 ) + ( ( 8 · 𝑀 ) − ( 6 · 𝑀 ) ) ) ) = ( ( ( 1 6 · ( 𝑀 ↑ 5 ) ) − ( 2 0 · ( 𝑀 ↑ 3 ) ) ) + ( 5 · 𝑀 ) ) )
86 34 43 85 3eqtrd ⊢ ( 𝑀 ∈ ℂ → ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) + ( 3 · 𝑀 ) ) + ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 8 · 𝑀 ) ) − ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) ) = ( ( ( 1 6 · ( 𝑀 ↑ 5 ) ) − ( 2 0 · ( 𝑀 ↑ 3 ) ) ) + ( 5 · 𝑀 ) ) )
87 86 3ad2ant2 ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 0 · ( 𝑀 ↑ 3 ) ) ) + ( 3 · 𝑀 ) ) + ( ( ( ( 8 · ( 𝑀 ↑ 5 ) ) − ( 1 6 · ( 𝑀 ↑ 3 ) ) ) + ( 8 · 𝑀 ) ) − ( ( 6 · 𝑀 ) − ( 6 · ( 𝑀 ↑ 3 ) ) ) ) ) = ( ( ( 1 6 · ( 𝑀 ↑ 5 ) ) − ( 2 0 · ( 𝑀 ↑ 3 ) ) ) + ( 5 · 𝑀 ) ) )
88 4 87 eqtrd ⊢ ( ( 𝑁 ∈ ℂ ∧ 𝑀 ∈ ℂ ∧ ( 𝑁 ↑ 2 ) = ( 1 − ( 𝑀 ↑ 2 ) ) ) → ( ( ( ( 3 · 𝑀 ) − ( 4 · ( 𝑀 ↑ 3 ) ) ) · ( 1 − ( 2 · ( 𝑀 ↑ 2 ) ) ) ) + ( ( ( 4 · ( 𝑁 ↑ 3 ) ) − ( 3 · 𝑁 ) ) · ( 2 · ( 𝑀 · 𝑁 ) ) ) ) = ( ( ( 1 6 · ( 𝑀 ↑ 5 ) ) − ( 2 0 · ( 𝑀 ↑ 3 ) ) ) + ( 5 · 𝑀 ) ) )