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 
|- ( ( 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 ) ) ) ) )

Proof

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