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 5 2timesi 
 |-  ( 2 x. 4 ) = ( 4 + 4 )
27 4p4e8 
 |-  ( 4 + 4 ) = 8
28 26 27 eqtri 
 |-  ( 2 x. 4 ) = 8
29 28 a1i 
 |-  ( N e. CC -> ( 2 x. 4 ) = 8 )
30 2nn0 
 |-  2 e. NN0
31 30 a1i 
 |-  ( N e. CC -> 2 e. NN0 )
32 3 8 31 expaddd 
 |-  ( N e. CC -> ( N ^ ( 2 + 3 ) ) = ( ( N ^ 2 ) x. ( N ^ 3 ) ) )
33 2cn 
 |-  2 e. CC
34 3p2e5 
 |-  ( 3 + 2 ) = 5
35 1 33 34 addcomli 
 |-  ( 2 + 3 ) = 5
36 35 oveq2i 
 |-  ( N ^ ( 2 + 3 ) ) = ( N ^ 5 )
37 32 36 eqtr3di 
 |-  ( N e. CC -> ( ( N ^ 2 ) x. ( N ^ 3 ) ) = ( N ^ 5 ) )
38 29 37 oveq12d 
 |-  ( N e. CC -> ( ( 2 x. 4 ) x. ( ( N ^ 2 ) x. ( N ^ 3 ) ) ) = ( 8 x. ( N ^ 5 ) ) )
39 25 38 eqtrd 
 |-  ( N e. CC -> ( ( 2 x. ( N ^ 2 ) ) x. ( 4 x. ( N ^ 3 ) ) ) = ( 8 x. ( N ^ 5 ) ) )
40 2 3 12 13 mul4d 
 |-  ( N e. CC -> ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) = ( ( 3 x. 2 ) x. ( N x. ( N ^ 2 ) ) ) )
41 3t2e6 
 |-  ( 3 x. 2 ) = 6
42 41 a1i 
 |-  ( N e. CC -> ( 3 x. 2 ) = 6 )
43 df-3 
 |-  3 = ( 2 + 1 )
44 43 oveq2i 
 |-  ( N ^ 3 ) = ( N ^ ( 2 + 1 ) )
45 3 31 expp1d 
 |-  ( N e. CC -> ( N ^ ( 2 + 1 ) ) = ( ( N ^ 2 ) x. N ) )
46 13 3 mulcomd 
 |-  ( N e. CC -> ( ( N ^ 2 ) x. N ) = ( N x. ( N ^ 2 ) ) )
47 45 46 eqtrd 
 |-  ( N e. CC -> ( N ^ ( 2 + 1 ) ) = ( N x. ( N ^ 2 ) ) )
48 44 47 eqtr2id 
 |-  ( N e. CC -> ( N x. ( N ^ 2 ) ) = ( N ^ 3 ) )
49 42 48 oveq12d 
 |-  ( N e. CC -> ( ( 3 x. 2 ) x. ( N x. ( N ^ 2 ) ) ) = ( 6 x. ( N ^ 3 ) ) )
50 40 49 eqtrd 
 |-  ( N e. CC -> ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) = ( 6 x. ( N ^ 3 ) ) )
51 10 mullidd 
 |-  ( N e. CC -> ( 1 x. ( 4 x. ( N ^ 3 ) ) ) = ( 4 x. ( N ^ 3 ) ) )
52 50 51 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 ) ) ) )
53 6cn 
 |-  6 e. CC
54 53 a1i 
 |-  ( N e. CC -> 6 e. CC )
55 54 6 9 adddird 
 |-  ( N e. CC -> ( ( 6 + 4 ) x. ( N ^ 3 ) ) = ( ( 6 x. ( N ^ 3 ) ) + ( 4 x. ( N ^ 3 ) ) ) )
56 6p4e10 
 |-  ( 6 + 4 ) = ; 1 0
57 56 a1i 
 |-  ( N e. CC -> ( 6 + 4 ) = ; 1 0 )
58 57 oveq1d 
 |-  ( N e. CC -> ( ( 6 + 4 ) x. ( N ^ 3 ) ) = ( ; 1 0 x. ( N ^ 3 ) ) )
59 52 55 58 3eqtr2d 
 |-  ( N e. CC -> ( ( ( 3 x. N ) x. ( 2 x. ( N ^ 2 ) ) ) + ( 1 x. ( 4 x. ( N ^ 3 ) ) ) ) = ( ; 1 0 x. ( N ^ 3 ) ) )
60 39 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 ) ) ) ) ) = ( ( 8 x. ( N ^ 5 ) ) - ( ; 1 0 x. ( N ^ 3 ) ) ) )
61 4 mulridd 
 |-  ( N e. CC -> ( ( 3 x. N ) x. 1 ) = ( 3 x. N ) )
62 60 61 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 ) ) )
63 15 24 62 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 ) ) )