Metamath Proof Explorer

Theorem sin5tlem3

Description: Lemma 3 for quintupled angle sine calculation, multiplicating triple angle cosine by double angle sine. (Contributed by Ender Ting, 16-Apr-2026)

Ref Expression
Assertion 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 ) ) )

Proof

Step Hyp Ref Expression
1 simp2 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> M e. CC )
2 simp1 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> N e. CC )
3 1 2 mulcomd 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( M x. N ) = ( N x. M ) )
4 3 oveq2d 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( 2 x. ( M x. N ) ) = ( 2 x. ( N x. M ) ) )
5 2cnd 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> 2 e. CC )
6 5 2 1 mul12d 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( 2 x. ( N x. M ) ) = ( N x. ( 2 x. M ) ) )
7 4 6 eqtrd 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( 2 x. ( M x. N ) ) = ( N x. ( 2 x. M ) ) )
8 7 oveq2d 
 |-  ( ( 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. ( N ^ 3 ) ) - ( 3 x. N ) ) x. ( N x. ( 2 x. M ) ) ) )
9 4cn 
 |-  4 e. CC
10 9 a1i 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> 4 e. CC )
11 3nn0 
 |-  3 e. NN0
12 11 a1i 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> 3 e. NN0 )
13 2 12 expcld 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( N ^ 3 ) e. CC )
14 10 13 mulcld 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( 4 x. ( N ^ 3 ) ) e. CC )
15 3cn 
 |-  3 e. CC
16 15 a1i 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> 3 e. CC )
17 16 2 mulcld 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( 3 x. N ) e. CC )
18 14 17 subcld 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( 4 x. ( N ^ 3 ) ) - ( 3 x. N ) ) e. CC )
19 5 1 mulcld 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( 2 x. M ) e. CC )
20 18 2 19 mulassd 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( ( ( 4 x. ( N ^ 3 ) ) - ( 3 x. N ) ) x. N ) x. ( 2 x. M ) ) = ( ( ( 4 x. ( N ^ 3 ) ) - ( 3 x. N ) ) x. ( N x. ( 2 x. M ) ) ) )
21 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 ) ) ) ) )
22 21 oveq1d 
 |-  ( ( N e. CC /\ M e. CC /\ ( N ^ 2 ) = ( 1 - ( M ^ 2 ) ) ) -> ( ( ( ( 4 x. ( N ^ 3 ) ) - ( 3 x. N ) ) x. N ) x. ( 2 x. M ) ) = ( ( ( 4 x. ( ( 1 - ( 2 x. ( M ^ 2 ) ) ) + ( M ^ 4 ) ) ) - ( 3 x. ( 1 - ( M ^ 2 ) ) ) ) x. ( 2 x. M ) ) )
23 8 20 22 3eqtr2d 
 |-  ( ( 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 ) ) )