Metamath Proof Explorer

Theorem sin5tlem2

Description: Lemma 2 for quintupled angle sine calculation, multiplicating triple angle cosine by cosine straight and converting into sine. (Contributed by Ender Ting, 16-Apr-2026)

Ref Expression
Assertion sin5tlem2 
|- ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( ( 4 x. ( N ^ 3 ) ) - ( 3 x. N ) ) x. N ) = ( ( 4 x. ( ( 1 - ( 2 x. ( M ^ 2 ) ) ) + ( M ^ 4 ) ) ) - ( 3 x. ( 1 - ( M ^ 2 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 4cn 
 |-  4 e. CC
2 1 a1i 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> 4 e. CC )
3 simp1 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> N e. CC )
4 3nn0 
 |-  3 e. NN0
5 4 a1i 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> 3 e. NN0 )
6 3 5 expcld 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( N ^ 3 ) e. CC )
7 2 6 mulcld 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( 4 x. ( N ^ 3 ) ) e. CC )
8 3cn 
 |-  3 e. CC
9 8 a1i 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> 3 e. CC )
10 9 3 mulcld 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( 3 x. N ) e. CC )
11 7 10 3 subdird 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( ( 4 x. ( N ^ 3 ) ) - ( 3 x. N ) ) x. N ) = ( ( ( 4 x. ( N ^ 3 ) ) x. N ) - ( ( 3 x. N ) x. N ) ) )
12 2 6 3 mulassd 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( 4 x. ( N ^ 3 ) ) x. N ) = ( 4 x. ( ( N ^ 3 ) x. N ) ) )
13 2t2e4 
 |-  ( 2 x. 2 ) = 4
14 df-4 
 |-  4 = ( 3 + 1 )
15 13 14 eqtri 
 |-  ( 2 x. 2 ) = ( 3 + 1 )
16 15 a1i 
 |-  ( N e. CC -> ( 2 x. 2 ) = ( 3 + 1 ) )
17 16 oveq2d 
 |-  ( N e. CC -> ( N ^ ( 2 x. 2 ) ) = ( N ^ ( 3 + 1 ) ) )
18 id 
 |-  ( N e. CC -> N e. CC )
19 2nn0 
 |-  2 e. NN0
20 19 a1i 
 |-  ( N e. CC -> 2 e. NN0 )
21 18 20 20 expmuld 
 |-  ( N e. CC -> ( N ^ ( 2 x. 2 ) ) = ( ( N ^ 2 ) ^ 2 ) )
22 4 a1i 
 |-  ( N e. CC -> 3 e. NN0 )
23 18 22 expp1d 
 |-  ( N e. CC -> ( N ^ ( 3 + 1 ) ) = ( ( N ^ 3 ) x. N ) )
24 17 21 23 3eqtr3rd 
 |-  ( N e. CC -> ( ( N ^ 3 ) x. N ) = ( ( N ^ 2 ) ^ 2 ) )
25 24 3ad2ant1 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( N ^ 3 ) x. N ) = ( ( N ^ 2 ) ^ 2 ) )
26 25 oveq2d 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( 4 x. ( ( N ^ 3 ) x. N ) ) = ( 4 x. ( ( N ^ 2 ) ^ 2 ) ) )
27 oveq1 
 |-  ( ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) -> ( ( N ^ 2 ) ^ 2 ) = ( ( 1 - ( M ^ 2 ) ) ^ 2 ) )
28 27 oveq2d 
 |-  ( ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) -> ( 4 x. ( ( N ^ 2 ) ^ 2 ) ) = ( 4 x. ( ( 1 - ( M ^ 2 ) ) ^ 2 ) ) )
29 28 3ad2ant3 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( 4 x. ( ( N ^ 2 ) ^ 2 ) ) = ( 4 x. ( ( 1 - ( M ^ 2 ) ) ^ 2 ) ) )
30 12 26 29 3eqtrd 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( 4 x. ( N ^ 3 ) ) x. N ) = ( 4 x. ( ( 1 - ( M ^ 2 ) ) ^ 2 ) ) )
31 1cnd 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> 1 e. CC )
32 simp2 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> M e. CC )
33 19 a1i 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> 2 e. NN0 )
34 32 33 expcld 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( M ^ 2 ) e. CC )
35 binom2sub 
 |-  ( ( 1 e. CC /\ ( M ^ 2 ) e. CC ) -> ( ( 1 - ( M ^ 2 ) ) ^ 2 ) = ( ( ( 1 ^ 2 ) - ( 2 x. ( 1 x. ( M ^ 2 ) ) ) ) + ( ( M ^ 2 ) ^ 2 ) ) )
36 31 34 35 syl2anc 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( 1 - ( M ^ 2 ) ) ^ 2 ) = ( ( ( 1 ^ 2 ) - ( 2 x. ( 1 x. ( M ^ 2 ) ) ) ) + ( ( M ^ 2 ) ^ 2 ) ) )
37 sq1 
 |-  ( 1 ^ 2 ) = 1
38 37 a1i 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( 1 ^ 2 ) = 1 )
39 34 mullidd 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( 1 x. ( M ^ 2 ) ) = ( M ^ 2 ) )
40 39 oveq2d 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( 2 x. ( 1 x. ( M ^ 2 ) ) ) = ( 2 x. ( M ^ 2 ) ) )
41 38 40 oveq12d 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( 1 ^ 2 ) - ( 2 x. ( 1 x. ( M ^ 2 ) ) ) ) = ( 1 - ( 2 x. ( M ^ 2 ) ) ) )
42 13 eqcomi 
 |-  4 = ( 2 x. 2 )
43 42 a1i 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> 4 = ( 2 x. 2 ) )
44 43 oveq2d 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( M ^ 4 ) = ( M ^ ( 2 x. 2 ) ) )
45 32 33 33 expmuld 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( M ^ ( 2 x. 2 ) ) = ( ( M ^ 2 ) ^ 2 ) )
46 44 45 eqtr2d 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( M ^ 2 ) ^ 2 ) = ( M ^ 4 ) )
47 41 46 oveq12d 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( ( 1 ^ 2 ) - ( 2 x. ( 1 x. ( M ^ 2 ) ) ) ) + ( ( M ^ 2 ) ^ 2 ) ) = ( ( 1 - ( 2 x. ( M ^ 2 ) ) ) + ( M ^ 4 ) ) )
48 36 47 eqtrd 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( 1 - ( M ^ 2 ) ) ^ 2 ) = ( ( 1 - ( 2 x. ( M ^ 2 ) ) ) + ( M ^ 4 ) ) )
49 48 oveq2d 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( 4 x. ( ( 1 - ( M ^ 2 ) ) ^ 2 ) ) = ( 4 x. ( ( 1 - ( 2 x. ( M ^ 2 ) ) ) + ( M ^ 4 ) ) ) )
50 30 49 eqtrd 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( 4 x. ( N ^ 3 ) ) x. N ) = ( 4 x. ( ( 1 - ( 2 x. ( M ^ 2 ) ) ) + ( M ^ 4 ) ) ) )
51 9 3 3 mulassd 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( 3 x. N ) x. N ) = ( 3 x. ( N x. N ) ) )
52 sqval 
 |-  ( N e. CC -> ( N ^ 2 ) = ( N x. N ) )
53 52 eqcomd 
 |-  ( N e. CC -> ( N x. N ) = ( N ^ 2 ) )
54 53 3ad2ant1 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( N x. N ) = ( N ^ 2 ) )
55 54 oveq2d 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( 3 x. ( N x. N ) ) = ( 3 x. ( N ^ 2 ) ) )
56 oveq2 
 |-  ( ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) -> ( 3 x. ( N ^ 2 ) ) = ( 3 x. ( 1 - ( M ^ 2 ) ) ) )
57 56 3ad2ant3 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( 3 x. ( N ^ 2 ) ) = ( 3 x. ( 1 - ( M ^ 2 ) ) ) )
58 51 55 57 3eqtrd 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( 3 x. N ) x. N ) = ( 3 x. ( 1 - ( M ^ 2 ) ) ) )
59 50 58 oveq12d 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( ( 4 x. ( N ^ 3 ) ) x. N ) - ( ( 3 x. N ) x. N ) ) = ( ( 4 x. ( ( 1 - ( 2 x. ( M ^ 2 ) ) ) + ( M ^ 4 ) ) ) - ( 3 x. ( 1 - ( M ^ 2 ) ) ) ) )
60 11 59 eqtrd 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( ( 4 x. ( N ^ 3 ) ) - ( 3 x. N ) ) x. N ) = ( ( 4 x. ( ( 1 - ( 2 x. ( M ^ 2 ) ) ) + ( M ^ 4 ) ) ) - ( 3 x. ( 1 - ( M ^ 2 ) ) ) ) )