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 1nn0 
 |-  1 e. NN0
18 6nn0 
 |-  6 e. NN0
19 17 18 deccl 
 |-  ; 1 6 e. NN0
20 19 nn0cni 
 |-  ; 1 6 e. CC
21 20 a1i 
 |-  ( M e. CC -> ; 1 6 e. CC )
22 3nn0 
 |-  3 e. NN0
23 22 a1i 
 |-  ( M e. CC -> 3 e. NN0 )
24 7 23 expcld 
 |-  ( M e. CC -> ( M ^ 3 ) e. CC )
25 21 24 mulcld 
 |-  ( M e. CC -> ( ; 1 6 x. ( M ^ 3 ) ) e. CC )
26 16 25 subcld 
 |-  ( M e. CC -> ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) e. CC )
27 10 24 mulcld 
 |-  ( M e. CC -> ( 6 x. ( M ^ 3 ) ) e. CC )
28 26 27 addcld 
 |-  ( M e. CC -> ( ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 6 x. ( M ^ 3 ) ) ) + ( 6 x. ( M ^ 3 ) ) ) e. CC )
29 26 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 ) ) ) ) )
30 29 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 ) ) ) ) )
31 8 26 11 27 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 ) ) ) ) )
32 30 31 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 ) ) ) ) )
33 12 28 32 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 ) ) ) )
34 33 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 ) ) ) ) )
35 10nn 
 |-  ; 1 0 e. NN
36 35 nncni 
 |-  ; 1 0 e. CC
37 36 a1i 
 |-  ( M e. CC -> ; 1 0 e. CC )
38 37 24 mulcld 
 |-  ( M e. CC -> ( ; 1 0 x. ( M ^ 3 ) ) e. CC )
39 16 38 subcld 
 |-  ( M e. CC -> ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) e. CC )
40 3cn 
 |-  3 e. CC
41 40 a1i 
 |-  ( M e. CC -> 3 e. CC )
42 41 7 mulcld 
 |-  ( M e. CC -> ( 3 x. M ) e. CC )
43 39 42 28 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 ) ) ) ) )
44 16 16 38 38 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 ) ) ) ) )
45 8p8e16 
 |-  ( 8 + 8 ) = ; 1 6
46 45 eqcomi 
 |-  ; 1 6 = ( 8 + 8 )
47 46 a1i 
 |-  ( M e. CC -> ; 1 6 = ( 8 + 8 ) )
48 47 oveq1d 
 |-  ( M e. CC -> ( ; 1 6 x. ( M ^ 5 ) ) = ( ( 8 + 8 ) x. ( M ^ 5 ) ) )
49 6 6 15 adddird 
 |-  ( M e. CC -> ( ( 8 + 8 ) x. ( M ^ 5 ) ) = ( ( 8 x. ( M ^ 5 ) ) + ( 8 x. ( M ^ 5 ) ) ) )
50 48 49 eqtrd 
 |-  ( M e. CC -> ( ; 1 6 x. ( M ^ 5 ) ) = ( ( 8 x. ( M ^ 5 ) ) + ( 8 x. ( M ^ 5 ) ) ) )
51 10p10e20 
 |-  ( ; 1 0 + ; 1 0 ) = ; 2 0
52 51 eqcomi 
 |-  ; 2 0 = ( ; 1 0 + ; 1 0 )
53 52 a1i 
 |-  ( M e. CC -> ; 2 0 = ( ; 1 0 + ; 1 0 ) )
54 53 oveq1d 
 |-  ( M e. CC -> ( ; 2 0 x. ( M ^ 3 ) ) = ( ( ; 1 0 + ; 1 0 ) x. ( M ^ 3 ) ) )
55 37 37 24 adddird 
 |-  ( M e. CC -> ( ( ; 1 0 + ; 1 0 ) x. ( M ^ 3 ) ) = ( ( ; 1 0 x. ( M ^ 3 ) ) + ( ; 1 0 x. ( M ^ 3 ) ) ) )
56 54 55 eqtrd 
 |-  ( M e. CC -> ( ; 2 0 x. ( M ^ 3 ) ) = ( ( ; 1 0 x. ( M ^ 3 ) ) + ( ; 1 0 x. ( M ^ 3 ) ) ) )
57 50 56 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 ) ) ) ) )
58 21 10 24 subdird 
 |-  ( M e. CC -> ( ( ; 1 6 - 6 ) x. ( M ^ 3 ) ) = ( ( ; 1 6 x. ( M ^ 3 ) ) - ( 6 x. ( M ^ 3 ) ) ) )
59 58 eqcomd 
 |-  ( M e. CC -> ( ( ; 1 6 x. ( M ^ 3 ) ) - ( 6 x. ( M ^ 3 ) ) ) = ( ( ; 1 6 - 6 ) x. ( M ^ 3 ) ) )
60 59 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 ) ) ) )
61 16 25 27 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 ) ) ) )
62 dec10p 
 |-  ( ; 1 0 + 6 ) = ; 1 6
63 62 eqcomi 
 |-  ; 1 6 = ( ; 1 0 + 6 )
64 63 a1i 
 |-  ( M e. CC -> ; 1 6 = ( ; 1 0 + 6 ) )
65 37 10 64 mvrraddd 
 |-  ( M e. CC -> ( ; 1 6 - 6 ) = ; 1 0 )
66 65 oveq1d 
 |-  ( M e. CC -> ( ( ; 1 6 - 6 ) x. ( M ^ 3 ) ) = ( ; 1 0 x. ( M ^ 3 ) ) )
67 66 oveq2d 
 |-  ( M e. CC -> ( ( 8 x. ( M ^ 5 ) ) - ( ( ; 1 6 - 6 ) x. ( M ^ 3 ) ) ) = ( ( 8 x. ( M ^ 5 ) ) - ( ; 1 0 x. ( M ^ 3 ) ) ) )
68 60 61 67 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 ) ) ) )
69 68 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 ) ) ) ) )
70 44 57 69 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 ) ) ) )
71 6 10 subcld 
 |-  ( M e. CC -> ( 8 - 6 ) e. CC )
72 41 71 7 adddird 
 |-  ( M e. CC -> ( ( 3 + ( 8 - 6 ) ) x. M ) = ( ( 3 x. M ) + ( ( 8 - 6 ) x. M ) ) )
73 2cn 
 |-  2 e. CC
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 
 |-  ( M e. CC -> ( 3 + ( 8 - 6 ) ) = 5 )
81 80 oveq1d 
 |-  ( M e. CC -> ( ( 3 + ( 8 - 6 ) ) x. M ) = ( 5 x. M ) )
82 6 10 7 subdird 
 |-  ( M e. CC -> ( ( 8 - 6 ) x. M ) = ( ( 8 x. M ) - ( 6 x. M ) ) )
83 82 oveq2d 
 |-  ( M e. CC -> ( ( 3 x. M ) + ( ( 8 - 6 ) x. M ) ) = ( ( 3 x. M ) + ( ( 8 x. M ) - ( 6 x. M ) ) ) )
84 72 81 83 3eqtr3rd 
 |-  ( M e. CC -> ( ( 3 x. M ) + ( ( 8 x. M ) - ( 6 x. M ) ) ) = ( 5 x. M ) )
85 70 84 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 ) ) )
86 34 43 85 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 ) ) )
87 86 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 ) ) )
88 4 87 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 ) ) )