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