Metamath Proof Explorer

Theorem sin5tlem1

Description: Lemma 1 for quintupled angle sine calculation, expanding triple-angle sine times double-angle cosine. (Contributed by Ender Ting, 16-Mar-2026)

Ref Expression
Assertion sin5tlem1 
|- ( N e. CC -> ( ( ( 3 x. N ) - ( 4 x. ( N ^ 3 ) ) ) x. ( 1 - ( 2 x. ( N ^ 2 ) ) ) ) = ( ( ( 8 x. ( N ^ 5 ) ) - ( ; 1 0 x. ( N ^ 3 ) ) ) + ( 3 x. N ) ) )

Proof

Step Hyp Ref Expression
1 3cn 
 |-  3 e. CC
2 1 a1i 
 |-  ( N e. CC -> 3 e. CC )
3 id 
 |-  ( N e. CC -> N e. CC )
4 2 3 mulcld 
 |-  ( N e. CC -> ( 3 x. N ) e. CC )
5 4cn 
 |-  4 e. CC
6 5 a1i 
 |-  ( N e. CC -> 4 e. CC )
7 3nn0 
 |-  3 e. NN0
8 7 a1i 
 |-  ( N e. CC -> 3 e. NN0 )
9 3 8 expcld 
 |-  ( N e. CC -> ( N ^ 3 ) e. CC )
10 6 9 mulcld 
 |-  ( N e. CC -> ( 4 x. ( N ^ 3 ) ) e. CC )
11 1cnd 
 |-  ( N e. CC -> 1 e. CC )
12 2cnd 
 |-  ( N e. CC -> 2 e. CC )
13 sqcl 
 |-  ( N e. CC -> ( N ^ 2 ) e. CC )
14 12 13 mulcld 
 |-  ( N e. CC -> ( 2 x. ( N ^ 2 ) ) e. CC )
15 4 10 11 14 mulsubd 
 |-  ( N e. CC -> ( ( ( 3 x. N ) - ( 4 x. ( N ^ 3 ) ) ) x. ( 1 - ( 2 x. ( N ^ 2 ) ) ) ) = ( ( ( ( 3 x. N ) x. 1 ) + ( ( 2 x. ( N ^ 2 ) ) x. ( 4 x. ( N ^ 3 ) ) ) ) - ( ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) + ( 1 x. ( 4 x. ( N ^ 3 ) ) ) ) ) )
16 4 11 mulcld 
 |-  ( N e. CC -> ( ( 3 x. N ) x. 1 ) e. CC )
17 14 10 mulcld 
 |-  ( N e. CC -> ( ( 2 x. ( N ^ 2 ) ) x. ( 4 x. ( N ^ 3 ) ) ) e. CC )
18 16 17 addcomd 
 |-  ( N e. CC -> ( ( ( 3 x. N ) x. 1 ) + ( ( 2 x. ( N ^ 2 ) ) x. ( 4 x. ( N ^ 3 ) ) ) ) = ( ( ( 2 x. ( N ^ 2 ) ) x. ( 4 x. ( N ^ 3 ) ) ) + ( ( 3 x. N ) x. 1 ) ) )
19 18 oveq1d 
 |-  ( N e. CC -> ( ( ( ( 3 x. N ) x. 1 ) + ( ( 2 x. ( N ^ 2 ) ) x. ( 4 x. ( N ^ 3 ) ) ) ) - ( ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) + ( 1 x. ( 4 x. ( N ^ 3 ) ) ) ) ) = ( ( ( ( 2 x. ( N ^ 2 ) ) x. ( 4 x. ( N ^ 3 ) ) ) + ( ( 3 x. N ) x. 1 ) ) - ( ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) + ( 1 x. ( 4 x. ( N ^ 3 ) ) ) ) ) )
20 4 14 mulcld 
 |-  ( N e. CC -> ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) e. CC )
21 11 10 mulcld 
 |-  ( N e. CC -> ( 1 x. ( 4 x. ( N ^ 3 ) ) ) e. CC )
22 20 21 addcld 
 |-  ( N e. CC -> ( ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) + ( 1 x. ( 4 x. ( N ^ 3 ) ) ) ) e. CC )
23 17 16 22 addsubd 
 |-  ( N e. CC -> ( ( ( ( 2 x. ( N ^ 2 ) ) x. ( 4 x. ( N ^ 3 ) ) ) + ( ( 3 x. N ) x. 1 ) ) - ( ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) + ( 1 x. ( 4 x. ( N ^ 3 ) ) ) ) ) = ( ( ( ( 2 x. ( N ^ 2 ) ) x. ( 4 x. ( N ^ 3 ) ) ) - ( ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) + ( 1 x. ( 4 x. ( N ^ 3 ) ) ) ) ) + ( ( 3 x. N ) x. 1 ) ) )
24 19 23 eqtrd 
 |-  ( N e. CC -> ( ( ( ( 3 x. N ) x. 1 ) + ( ( 2 x. ( N ^ 2 ) ) x. ( 4 x. ( N ^ 3 ) ) ) ) - ( ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) + ( 1 x. ( 4 x. ( N ^ 3 ) ) ) ) ) = ( ( ( ( 2 x. ( N ^ 2 ) ) x. ( 4 x. ( N ^ 3 ) ) ) - ( ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) + ( 1 x. ( 4 x. ( N ^ 3 ) ) ) ) ) + ( ( 3 x. N ) x. 1 ) ) )
25 12 13 6 9 mul4d 
 |-  ( N e. CC -> ( ( 2 x. ( N ^ 2 ) ) x. ( 4 x. ( N ^ 3 ) ) ) = ( ( 2 x. 4 ) x. ( ( N ^ 2 ) x. ( N ^ 3 ) ) ) )
26 2t4e8 
 |-  ( 2 x. 4 ) = 8
27 26 a1i 
 |-  ( N e. CC -> ( 2 x. 4 ) = 8 )
28 2nn0 
 |-  2 e. NN0
29 28 a1i 
 |-  ( N e. CC -> 2 e. NN0 )
30 3 8 29 expaddd 
 |-  ( N e. CC -> ( N ^ ( 2 + 3 ) ) = ( ( N ^ 2 ) x. ( N ^ 3 ) ) )
31 2cn 
 |-  2 e. CC
32 3p2e5 
 |-  ( 3 + 2 ) = 5
33 1 31 32 addcomli 
 |-  ( 2 + 3 ) = 5
34 33 oveq2i 
 |-  ( N ^ ( 2 + 3 ) ) = ( N ^ 5 )
35 30 34 eqtr3di 
 |-  ( N e. CC -> ( ( N ^ 2 ) x. ( N ^ 3 ) ) = ( N ^ 5 ) )
36 27 35 oveq12d 
 |-  ( N e. CC -> ( ( 2 x. 4 ) x. ( ( N ^ 2 ) x. ( N ^ 3 ) ) ) = ( 8 x. ( N ^ 5 ) ) )
37 25 36 eqtrd 
 |-  ( N e. CC -> ( ( 2 x. ( N ^ 2 ) ) x. ( 4 x. ( N ^ 3 ) ) ) = ( 8 x. ( N ^ 5 ) ) )
38 2 3 12 13 mul4d 
 |-  ( N e. CC -> ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) = ( ( 3 x. 2 ) x. ( N x. ( N ^ 2 ) ) ) )
39 3t2e6 
 |-  ( 3 x. 2 ) = 6
40 39 a1i 
 |-  ( N e. CC -> ( 3 x. 2 ) = 6 )
41 df-3 
 |-  3 = ( 2 + 1 )
42 41 oveq2i 
 |-  ( N ^ 3 ) = ( N ^ ( 2 + 1 ) )
43 3 29 expp1d 
 |-  ( N e. CC -> ( N ^ ( 2 + 1 ) ) = ( ( N ^ 2 ) x. N ) )
44 13 3 mulcomd 
 |-  ( N e. CC -> ( ( N ^ 2 ) x. N ) = ( N x. ( N ^ 2 ) ) )
45 43 44 eqtrd 
 |-  ( N e. CC -> ( N ^ ( 2 + 1 ) ) = ( N x. ( N ^ 2 ) ) )
46 42 45 eqtr2id 
 |-  ( N e. CC -> ( N x. ( N ^ 2 ) ) = ( N ^ 3 ) )
47 40 46 oveq12d 
 |-  ( N e. CC -> ( ( 3 x. 2 ) x. ( N x. ( N ^ 2 ) ) ) = ( 6 x. ( N ^ 3 ) ) )
48 38 47 eqtrd 
 |-  ( N e. CC -> ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) = ( 6 x. ( N ^ 3 ) ) )
49 10 mullidd 
 |-  ( N e. CC -> ( 1 x. ( 4 x. ( N ^ 3 ) ) ) = ( 4 x. ( N ^ 3 ) ) )
50 48 49 oveq12d 
 |-  ( N e. CC -> ( ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) + ( 1 x. ( 4 x. ( N ^ 3 ) ) ) ) = ( ( 6 x. ( N ^ 3 ) ) + ( 4 x. ( N ^ 3 ) ) ) )
51 6cn 
 |-  6 e. CC
52 51 a1i 
 |-  ( N e. CC -> 6 e. CC )
53 52 6 9 adddird 
 |-  ( N e. CC -> ( ( 6 + 4 ) x. ( N ^ 3 ) ) = ( ( 6 x. ( N ^ 3 ) ) + ( 4 x. ( N ^ 3 ) ) ) )
54 6p4e10 
 |-  ( 6 + 4 ) = ; 1 0
55 54 a1i 
 |-  ( N e. CC -> ( 6 + 4 ) = ; 1 0 )
56 55 oveq1d 
 |-  ( N e. CC -> ( ( 6 + 4 ) x. ( N ^ 3 ) ) = ( ; 1 0 x. ( N ^ 3 ) ) )
57 50 53 56 3eqtr2d 
 |-  ( N e. CC -> ( ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) + ( 1 x. ( 4 x. ( N ^ 3 ) ) ) ) = ( ; 1 0 x. ( N ^ 3 ) ) )
58 37 57 oveq12d 
 |-  ( N e. CC -> ( ( ( 2 x. ( N ^ 2 ) ) x. ( 4 x. ( N ^ 3 ) ) ) - ( ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) + ( 1 x. ( 4 x. ( N ^ 3 ) ) ) ) ) = ( ( 8 x. ( N ^ 5 ) ) - ( ; 1 0 x. ( N ^ 3 ) ) ) )
59 4 mulridd 
 |-  ( N e. CC -> ( ( 3 x. N ) x. 1 ) = ( 3 x. N ) )
60 58 59 oveq12d 
 |-  ( N e. CC -> ( ( ( ( 2 x. ( N ^ 2 ) ) x. ( 4 x. ( N ^ 3 ) ) ) - ( ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) + ( 1 x. ( 4 x. ( N ^ 3 ) ) ) ) ) + ( ( 3 x. N ) x. 1 ) ) = ( ( ( 8 x. ( N ^ 5 ) ) - ( ; 1 0 x. ( N ^ 3 ) ) ) + ( 3 x. N ) ) )
61 15 24 60 3eqtrd 
 |-  ( N e. CC -> ( ( ( 3 x. N ) - ( 4 x. ( N ^ 3 ) ) ) x. ( 1 - ( 2 x. ( N ^ 2 ) ) ) ) = ( ( ( 8 x. ( N ^ 5 ) ) - ( ; 1 0 x. ( N ^ 3 ) ) ) + ( 3 x. N ) ) )