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 
|- ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( ( ( 3 x. M ) - ( 4 x. ( M ^ 3 ) ) ) x. ( 1 - ( 2 x. ( M ^ 2 ) ) ) ) + ( ( ( 4 x. ( N ^ 3 ) ) - ( 3 x. N ) ) x. ( 2 x. ( M x. N ) ) ) ) = ( ( ( ; 1 6 x. ( M ^ 5 ) ) - ( ; 2 0 x. ( M ^ 3 ) ) ) + ( 5 x. M ) ) )

Proof

Step Hyp Ref Expression
1 sin5tlem1 
 |-  ( M e. CC -> ( ( ( 3 x. M ) - ( 4 x. ( M ^ 3 ) ) ) x. ( 1 - ( 2 x. ( M ^ 2 ) ) ) ) = ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) + ( 3 x. M ) ) )
2 1 3ad2ant2 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( ( 3 x. M ) - ( 4 x. ( M ^ 3 ) ) ) x. ( 1 - ( 2 x. ( M ^ 2 ) ) ) ) = ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) + ( 3 x. M ) ) )
3 sin5tlem4 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( ( 4 x. ( N ^ 3 ) ) - ( 3 x. N ) ) x. ( 2 x. ( M x. N ) ) ) = ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 8 x. M ) ) - ( ( 6 x. M ) - ( 6 x. ( M ^ 3 ) ) ) ) )
4 2 3 oveq12d 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( ( ( 3 x. M ) - ( 4 x. ( M ^ 3 ) ) ) x. ( 1 - ( 2 x. ( M ^ 2 ) ) ) ) + ( ( ( 4 x. ( N ^ 3 ) ) - ( 3 x. N ) ) x. ( 2 x. ( M x. N ) ) ) ) = ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) + ( 3 x. M ) ) + ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 8 x. M ) ) - ( ( 6 x. M ) - ( 6 x. ( M ^ 3 ) ) ) ) ) )
5 8cn 
 |-  8 e. CC
6 5 a1i 
 |-  ( M e. CC -> 8 e. CC )
7 id 
 |-  ( M e. CC -> M e. CC )
8 6 7 mulcld 
 |-  ( M e. CC -> ( 8 x. M ) e. CC )
9 6cn 
 |-  6 e. CC
10 9 a1i 
 |-  ( M e. CC -> 6 e. CC )
11 10 7 mulcld 
 |-  ( M e. CC -> ( 6 x. M ) e. CC )
12 8 11 subcld 
 |-  ( M e. CC -> ( ( 8 x. M ) - ( 6 x. M ) ) e. CC )
13 5nn0 
 |-  5 e. NN0
14 13 a1i 
 |-  ( M e. CC -> 5 e. NN0 )
15 7 14 expcld 
 |-  ( M e. CC -> ( M ^ 5 ) e. CC )
16 6 15 mulcld 
 |-  ( M e. CC -> ( 8 x. ( M ^ 5 ) ) e. CC )
17 16nn0 
 |-  ; 1 6 e. NN0
18 17 nn0cni 
 |-  ; 1 6 e. CC
19 18 a1i 
 |-  ( M e. CC -> ; 1 6 e. CC )
20 3nn0 
 |-  3 e. NN0
21 20 a1i 
 |-  ( M e. CC -> 3 e. NN0 )
22 7 21 expcld 
 |-  ( M e. CC -> ( M ^ 3 ) e. CC )
23 19 22 mulcld 
 |-  ( M e. CC -> ( ; 1 6 x. ( M ^ 3 ) ) e. CC )
24 16 23 subcld 
 |-  ( M e. CC -> ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) e. CC )
25 10 22 mulcld 
 |-  ( M e. CC -> ( 6 x. ( M ^ 3 ) ) e. CC )
26 24 25 addcld 
 |-  ( M e. CC -> ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 6 x. ( M ^ 3 ) ) ) e. CC )
27 24 8 addcomd 
 |-  ( M e. CC -> ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 8 x. M ) ) = ( ( 8 x. M ) + ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) ) )
28 27 oveq1d 
 |-  ( M e. CC -> ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 8 x. M ) ) - ( ( 6 x. M ) - ( 6 x. ( M ^ 3 ) ) ) ) = ( ( ( 8 x. M ) + ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) ) - ( ( 6 x. M ) - ( 6 x. ( M ^ 3 ) ) ) ) )
29 8 24 11 25 addsubsub23 
 |-  ( M e. CC -> ( ( ( 8 x. M ) + ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) ) - ( ( 6 x. M ) - ( 6 x. ( M ^ 3 ) ) ) ) = ( ( ( 8 x. M ) - ( 6 x. M ) ) + ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 6 x. ( M ^ 3 ) ) ) ) )
30 28 29 eqtrd 
 |-  ( M e. CC -> ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 8 x. M ) ) - ( ( 6 x. M ) - ( 6 x. ( M ^ 3 ) ) ) ) = ( ( ( 8 x. M ) - ( 6 x. M ) ) + ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 6 x. ( M ^ 3 ) ) ) ) )
31 12 26 30 comraddd 
 |-  ( M e. CC -> ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 8 x. M ) ) - ( ( 6 x. M ) - ( 6 x. ( M ^ 3 ) ) ) ) = ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 6 x. ( M ^ 3 ) ) ) + ( ( 8 x. M ) - ( 6 x. M ) ) ) )
32 31 oveq2d 
 |-  ( M e. CC -> ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) + ( 3 x. M ) ) + ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 8 x. M ) ) - ( ( 6 x. M ) - ( 6 x. ( M ^ 3 ) ) ) ) ) = ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) + ( 3 x. M ) ) + ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 6 x. ( M ^ 3 ) ) ) + ( ( 8 x. M ) - ( 6 x. M ) ) ) ) )
33 10nn 
 |-  ; 1 0 e. NN
34 33 nncni 
 |-  ; 1 0 e. CC
35 34 a1i 
 |-  ( M e. CC -> ; 1 0 e. CC )
36 35 22 mulcld 
 |-  ( M e. CC -> ( ; 1 0 x. ( M ^ 3 ) ) e. CC )
37 16 36 subcld 
 |-  ( M e. CC -> ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) e. CC )
38 3cn 
 |-  3 e. CC
39 38 a1i 
 |-  ( M e. CC -> 3 e. CC )
40 39 7 mulcld 
 |-  ( M e. CC -> ( 3 x. M ) e. CC )
41 37 40 26 12 add4d 
 |-  ( M e. CC -> ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) + ( 3 x. M ) ) + ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 6 x. ( M ^ 3 ) ) ) + ( ( 8 x. M ) - ( 6 x. M ) ) ) ) = ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) + ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 6 x. ( M ^ 3 ) ) ) ) + ( ( 3 x. M ) + ( ( 8 x. M ) - ( 6 x. M ) ) ) ) )
42 16 16 36 36 addsub4d 
 |-  ( M e. CC -> ( ( ( 8 x. ( M ^ 5 ) ) + ( 8 x. ( M ^ 5 ) ) ) - ( ( ; 1 0 x. ( M ^ 3 ) ) + ( ; 1 0 x. ( M ^ 3 ) ) ) ) = ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) + ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) ) )
43 8p8e16 
 |-  ( 8 + 8 ) = ; 1 6
44 43 eqcomi 
 |-  ; 1 6 = ( 8 + 8 )
45 44 a1i 
 |-  ( M e. CC -> ; 1 6 = ( 8 + 8 ) )
46 45 oveq1d 
 |-  ( M e. CC -> ( ; 1 6 x. ( M ^ 5 ) ) = ( ( 8 + 8 ) x. ( M ^ 5 ) ) )
47 6 6 15 adddird 
 |-  ( M e. CC -> ( ( 8 + 8 ) x. ( M ^ 5 ) ) = ( ( 8 x. ( M ^ 5 ) ) + ( 8 x. ( M ^ 5 ) ) ) )
48 46 47 eqtrd 
 |-  ( M e. CC -> ( ; 1 6 x. ( M ^ 5 ) ) = ( ( 8 x. ( M ^ 5 ) ) + ( 8 x. ( M ^ 5 ) ) ) )
49 10p10e20 
 |-  ( ; 1 0 + ; 1 0 ) = ; 2 0
50 49 eqcomi 
 |-  ; 2 0 = ( ; 1 0 + ; 1 0 )
51 50 a1i 
 |-  ( M e. CC -> ; 2 0 = ( ; 1 0 + ; 1 0 ) )
52 51 oveq1d 
 |-  ( M e. CC -> ( ; 2 0 x. ( M ^ 3 ) ) = ( ( ; 1 0 + ; 1 0 ) x. ( M ^ 3 ) ) )
53 35 35 22 adddird 
 |-  ( M e. CC -> ( ( ; 1 0 + ; 1 0 ) x. ( M ^ 3 ) ) = ( ( ; 1 0 x. ( M ^ 3 ) ) + ( ; 1 0 x. ( M ^ 3 ) ) ) )
54 52 53 eqtrd 
 |-  ( M e. CC -> ( ; 2 0 x. ( M ^ 3 ) ) = ( ( ; 1 0 x. ( M ^ 3 ) ) + ( ; 1 0 x. ( M ^ 3 ) ) ) )
55 48 54 oveq12d 
 |-  ( M e. CC -> ( ( ; 1 6 x. ( M ^ 5 ) ) - ( ; 2 0 x. ( M ^ 3 ) ) ) = ( ( ( 8 x. ( M ^ 5 ) ) + ( 8 x. ( M ^ 5 ) ) ) - ( ( ; 1 0 x. ( M ^ 3 ) ) + ( ; 1 0 x. ( M ^ 3 ) ) ) ) )
56 19 10 22 subdird 
 |-  ( M e. CC -> ( ( ; 1 6 - 6 ) x. ( M ^ 3 ) ) = ( ( ; 1 6 x. ( M ^ 3 ) ) - ( 6 x. ( M ^ 3 ) ) ) )
57 56 eqcomd 
 |-  ( M e. CC -> ( ( ; 1 6 x. ( M ^ 3 ) ) - ( 6 x. ( M ^ 3 ) ) ) = ( ( ; 1 6 - 6 ) x. ( M ^ 3 ) ) )
58 57 oveq2d 
 |-  ( M e. CC -> ( ( 8 x. ( M ^ 5 ) ) - ( ( ; 1 6 x. ( M ^ 3 ) ) - ( 6 x. ( M ^ 3 ) ) ) ) = ( ( 8 x. ( M ^ 5 ) ) - ( ( ; 1 6 - 6 ) x. ( M ^ 3 ) ) ) )
59 16 23 25 subsubd 
 |-  ( M e. CC -> ( ( 8 x. ( M ^ 5 ) ) - ( ( ; 1 6 x. ( M ^ 3 ) ) - ( 6 x. ( M ^ 3 ) ) ) ) = ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 6 x. ( M ^ 3 ) ) ) )
60 dec10p 
 |-  ( ; 1 0 + 6 ) = ; 1 6
61 60 eqcomi 
 |-  ; 1 6 = ( ; 1 0 + 6 )
62 61 a1i 
 |-  ( M e. CC -> ; 1 6 = ( ; 1 0 + 6 ) )
63 35 10 62 mvrraddd 
 |-  ( M e. CC -> ( ; 1 6 - 6 ) = ; 1 0 )
64 63 oveq1d 
 |-  ( M e. CC -> ( ( ; 1 6 - 6 ) x. ( M ^ 3 ) ) = ( ; 1 0 x. ( M ^ 3 ) ) )
65 64 oveq2d 
 |-  ( M e. CC -> ( ( 8 x. ( M ^ 5 ) ) - ( ( ; 1 6 - 6 ) x. ( M ^ 3 ) ) ) = ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) )
66 58 59 65 3eqtr3d 
 |-  ( M e. CC -> ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 6 x. ( M ^ 3 ) ) ) = ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) )
67 66 oveq2d 
 |-  ( M e. CC -> ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) + ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 6 x. ( M ^ 3 ) ) ) ) = ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) + ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) ) )
68 42 55 67 3eqtr4rd 
 |-  ( M e. CC -> ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) + ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 6 x. ( M ^ 3 ) ) ) ) = ( ( ; 1 6 x. ( M ^ 5 ) ) - ( ; 2 0 x. ( M ^ 3 ) ) ) )
69 6 10 subcld 
 |-  ( M e. CC -> ( 8 - 6 ) e. CC )
70 39 69 7 adddird 
 |-  ( M e. CC -> ( ( 3 + ( 8 - 6 ) ) x. M ) = ( ( 3 x. M ) + ( ( 8 - 6 ) x. M ) ) )
71 2cn 
 |-  2 e. CC
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 
 |-  ( M e. CC -> ( 3 + ( 8 - 6 ) ) = 5 )
79 78 oveq1d 
 |-  ( M e. CC -> ( ( 3 + ( 8 - 6 ) ) x. M ) = ( 5 x. M ) )
80 6 10 7 subdird 
 |-  ( M e. CC -> ( ( 8 - 6 ) x. M ) = ( ( 8 x. M ) - ( 6 x. M ) ) )
81 80 oveq2d 
 |-  ( M e. CC -> ( ( 3 x. M ) + ( ( 8 - 6 ) x. M ) ) = ( ( 3 x. M ) + ( ( 8 x. M ) - ( 6 x. M ) ) ) )
82 70 79 81 3eqtr3rd 
 |-  ( M e. CC -> ( ( 3 x. M ) + ( ( 8 x. M ) - ( 6 x. M ) ) ) = ( 5 x. M ) )
83 68 82 oveq12d 
 |-  ( M e. CC -> ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) + ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 6 x. ( M ^ 3 ) ) ) ) + ( ( 3 x. M ) + ( ( 8 x. M ) - ( 6 x. M ) ) ) ) = ( ( ( ; 1 6 x. ( M ^ 5 ) ) - ( ; 2 0 x. ( M ^ 3 ) ) ) + ( 5 x. M ) ) )
84 32 41 83 3eqtrd 
 |-  ( M e. CC -> ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) + ( 3 x. M ) ) + ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 8 x. M ) ) - ( ( 6 x. M ) - ( 6 x. ( M ^ 3 ) ) ) ) ) = ( ( ( ; 1 6 x. ( M ^ 5 ) ) - ( ; 2 0 x. ( M ^ 3 ) ) ) + ( 5 x. M ) ) )
85 84 3ad2ant2 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) + ( 3 x. M ) ) + ( ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 8 x. M ) ) - ( ( 6 x. M ) - ( 6 x. ( M ^ 3 ) ) ) ) ) = ( ( ( ; 1 6 x. ( M ^ 5 ) ) - ( ; 2 0 x. ( M ^ 3 ) ) ) + ( 5 x. M ) ) )
86 4 85 eqtrd 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( ( ( 3 x. M ) - ( 4 x. ( M ^ 3 ) ) ) x. ( 1 - ( 2 x. ( M ^ 2 ) ) ) ) + ( ( ( 4 x. ( N ^ 3 ) ) - ( 3 x. N ) ) x. ( 2 x. ( M x. N ) ) ) ) = ( ( ( ; 1 6 x. ( M ^ 5 ) ) - ( ; 2 0 x. ( M ^ 3 ) ) ) + ( 5 x. M ) ) )