Metamath Proof Explorer

Theorem sin3t

Description: Triple-angle formula for sine, in pure sine form. (Contributed by Ender Ting, 16-Mar-2026)

Ref Expression
Assertion sin3t 
|- ( A e. CC -> ( sin ` ( 3 x. A ) ) = ( ( 3 x. ( sin ` A ) ) - ( 4 x. ( ( sin ` A ) ^ 3 ) ) ) )

Proof

Step Hyp Ref Expression
1 df-3 
 |-  3 = ( 2 + 1 )
2 1 oveq1i 
 |-  ( 3 x. A ) = ( ( 2 + 1 ) x. A )
3 2cnd 
 |-  ( A e. CC -> 2 e. CC )
4 1cnd 
 |-  ( A e. CC -> 1 e. CC )
5 id 
 |-  ( A e. CC -> A e. CC )
6 3 4 5 adddird 
 |-  ( A e. CC -> ( ( 2 + 1 ) x. A ) = ( ( 2 x. A ) + ( 1 x. A ) ) )
7 2 6 eqtrid 
 |-  ( A e. CC -> ( 3 x. A ) = ( ( 2 x. A ) + ( 1 x. A ) ) )
8 7 fveq2d 
 |-  ( A e. CC -> ( sin ` ( 3 x. A ) ) = ( sin ` ( ( 2 x. A ) + ( 1 x. A ) ) ) )
9 3 5 mulcld 
 |-  ( A e. CC -> ( 2 x. A ) e. CC )
10 4 5 mulcld 
 |-  ( A e. CC -> ( 1 x. A ) e. CC )
11 sinadd 
 |-  ( ( ( 2 x. A ) e. CC /\ ( 1 x. A ) e. CC ) -> ( sin ` ( ( 2 x. A ) + ( 1 x. A ) ) ) = ( ( ( sin ` ( 2 x. A ) ) x. ( cos ` ( 1 x. A ) ) ) + ( ( cos ` ( 2 x. A ) ) x. ( sin ` ( 1 x. A ) ) ) ) )
12 9 10 11 syl2anc 
 |-  ( A e. CC -> ( sin ` ( ( 2 x. A ) + ( 1 x. A ) ) ) = ( ( ( sin ` ( 2 x. A ) ) x. ( cos ` ( 1 x. A ) ) ) + ( ( cos ` ( 2 x. A ) ) x. ( sin ` ( 1 x. A ) ) ) ) )
13 sin2t 
 |-  ( A e. CC -> ( sin ` ( 2 x. A ) ) = ( 2 x. ( ( sin ` A ) x. ( cos ` A ) ) ) )
14 13 oveq1d 
 |-  ( A e. CC -> ( ( sin ` ( 2 x. A ) ) x. ( cos ` ( 1 x. A ) ) ) = ( ( 2 x. ( ( sin ` A ) x. ( cos ` A ) ) ) x. ( cos ` ( 1 x. A ) ) ) )
15 sincl 
 |-  ( A e. CC -> ( sin ` A ) e. CC )
16 coscl 
 |-  ( A e. CC -> ( cos ` A ) e. CC )
17 15 16 mulcld 
 |-  ( A e. CC -> ( ( sin ` A ) x. ( cos ` A ) ) e. CC )
18 10 coscld 
 |-  ( A e. CC -> ( cos ` ( 1 x. A ) ) e. CC )
19 3 17 18 mulassd 
 |-  ( A e. CC -> ( ( 2 x. ( ( sin ` A ) x. ( cos ` A ) ) ) x. ( cos ` ( 1 x. A ) ) ) = ( 2 x. ( ( ( sin ` A ) x. ( cos ` A ) ) x. ( cos ` ( 1 x. A ) ) ) ) )
20 mullid 
 |-  ( A e. CC -> ( 1 x. A ) = A )
21 20 fveq2d 
 |-  ( A e. CC -> ( cos ` ( 1 x. A ) ) = ( cos ` A ) )
22 21 oveq2d 
 |-  ( A e. CC -> ( ( ( sin ` A ) x. ( cos ` A ) ) x. ( cos ` ( 1 x. A ) ) ) = ( ( ( sin ` A ) x. ( cos ` A ) ) x. ( cos ` A ) ) )
23 15 16 16 mulassd 
 |-  ( A e. CC -> ( ( ( sin ` A ) x. ( cos ` A ) ) x. ( cos ` A ) ) = ( ( sin ` A ) x. ( ( cos ` A ) x. ( cos ` A ) ) ) )
24 16 sqvald 
 |-  ( A e. CC -> ( ( cos ` A ) ^ 2 ) = ( ( cos ` A ) x. ( cos ` A ) ) )
25 15 sqcld 
 |-  ( A e. CC -> ( ( sin ` A ) ^ 2 ) e. CC )
26 16 sqcld 
 |-  ( A e. CC -> ( ( cos ` A ) ^ 2 ) e. CC )
27 sincossq 
 |-  ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
28 25 26 27 mvlladdd 
 |-  ( A e. CC -> ( ( cos ` A ) ^ 2 ) = ( 1 - ( ( sin ` A ) ^ 2 ) ) )
29 24 28 eqtr3d 
 |-  ( A e. CC -> ( ( cos ` A ) x. ( cos ` A ) ) = ( 1 - ( ( sin ` A ) ^ 2 ) ) )
30 29 oveq2d 
 |-  ( A e. CC -> ( ( sin ` A ) x. ( ( cos ` A ) x. ( cos ` A ) ) ) = ( ( sin ` A ) x. ( 1 - ( ( sin ` A ) ^ 2 ) ) ) )
31 22 23 30 3eqtrd 
 |-  ( A e. CC -> ( ( ( sin ` A ) x. ( cos ` A ) ) x. ( cos ` ( 1 x. A ) ) ) = ( ( sin ` A ) x. ( 1 - ( ( sin ` A ) ^ 2 ) ) ) )
32 31 oveq2d 
 |-  ( A e. CC -> ( 2 x. ( ( ( sin ` A ) x. ( cos ` A ) ) x. ( cos ` ( 1 x. A ) ) ) ) = ( 2 x. ( ( sin ` A ) x. ( 1 - ( ( sin ` A ) ^ 2 ) ) ) ) )
33 15 4 25 subdid 
 |-  ( A e. CC -> ( ( sin ` A ) x. ( 1 - ( ( sin ` A ) ^ 2 ) ) ) = ( ( ( sin ` A ) x. 1 ) - ( ( sin ` A ) x. ( ( sin ` A ) ^ 2 ) ) ) )
34 15 mulridd 
 |-  ( A e. CC -> ( ( sin ` A ) x. 1 ) = ( sin ` A ) )
35 1 a1i 
 |-  ( A e. CC -> 3 = ( 2 + 1 ) )
36 35 oveq2d 
 |-  ( A e. CC -> ( ( sin ` A ) ^ 3 ) = ( ( sin ` A ) ^ ( 2 + 1 ) ) )
37 2nn0 
 |-  2 e. NN0
38 37 a1i 
 |-  ( A e. CC -> 2 e. NN0 )
39 15 38 expp1d 
 |-  ( A e. CC -> ( ( sin ` A ) ^ ( 2 + 1 ) ) = ( ( ( sin ` A ) ^ 2 ) x. ( sin ` A ) ) )
40 25 15 mulcomd 
 |-  ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) x. ( sin ` A ) ) = ( ( sin ` A ) x. ( ( sin ` A ) ^ 2 ) ) )
41 36 39 40 3eqtrrd 
 |-  ( A e. CC -> ( ( sin ` A ) x. ( ( sin ` A ) ^ 2 ) ) = ( ( sin ` A ) ^ 3 ) )
42 34 41 oveq12d 
 |-  ( A e. CC -> ( ( ( sin ` A ) x. 1 ) - ( ( sin ` A ) x. ( ( sin ` A ) ^ 2 ) ) ) = ( ( sin ` A ) - ( ( sin ` A ) ^ 3 ) ) )
43 33 42 eqtrd 
 |-  ( A e. CC -> ( ( sin ` A ) x. ( 1 - ( ( sin ` A ) ^ 2 ) ) ) = ( ( sin ` A ) - ( ( sin ` A ) ^ 3 ) ) )
44 43 oveq2d 
 |-  ( A e. CC -> ( 2 x. ( ( sin ` A ) x. ( 1 - ( ( sin ` A ) ^ 2 ) ) ) ) = ( 2 x. ( ( sin ` A ) - ( ( sin ` A ) ^ 3 ) ) ) )
45 3nn0 
 |-  3 e. NN0
46 45 a1i 
 |-  ( A e. CC -> 3 e. NN0 )
47 15 46 expcld 
 |-  ( A e. CC -> ( ( sin ` A ) ^ 3 ) e. CC )
48 3 15 47 subdid 
 |-  ( A e. CC -> ( 2 x. ( ( sin ` A ) - ( ( sin ` A ) ^ 3 ) ) ) = ( ( 2 x. ( sin ` A ) ) - ( 2 x. ( ( sin ` A ) ^ 3 ) ) ) )
49 32 44 48 3eqtrd 
 |-  ( A e. CC -> ( 2 x. ( ( ( sin ` A ) x. ( cos ` A ) ) x. ( cos ` ( 1 x. A ) ) ) ) = ( ( 2 x. ( sin ` A ) ) - ( 2 x. ( ( sin ` A ) ^ 3 ) ) ) )
50 14 19 49 3eqtrd 
 |-  ( A e. CC -> ( ( sin ` ( 2 x. A ) ) x. ( cos ` ( 1 x. A ) ) ) = ( ( 2 x. ( sin ` A ) ) - ( 2 x. ( ( sin ` A ) ^ 3 ) ) ) )
51 cos2tsin 
 |-  ( A e. CC -> ( cos ` ( 2 x. A ) ) = ( 1 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) )
52 20 fveq2d 
 |-  ( A e. CC -> ( sin ` ( 1 x. A ) ) = ( sin ` A ) )
53 51 52 oveq12d 
 |-  ( A e. CC -> ( ( cos ` ( 2 x. A ) ) x. ( sin ` ( 1 x. A ) ) ) = ( ( 1 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) x. ( sin ` A ) ) )
54 3 25 mulcld 
 |-  ( A e. CC -> ( 2 x. ( ( sin ` A ) ^ 2 ) ) e. CC )
55 4 54 15 subdird 
 |-  ( A e. CC -> ( ( 1 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) x. ( sin ` A ) ) = ( ( 1 x. ( sin ` A ) ) - ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) x. ( sin ` A ) ) ) )
56 53 55 eqtrd 
 |-  ( A e. CC -> ( ( cos ` ( 2 x. A ) ) x. ( sin ` ( 1 x. A ) ) ) = ( ( 1 x. ( sin ` A ) ) - ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) x. ( sin ` A ) ) ) )
57 50 56 oveq12d 
 |-  ( A e. CC -> ( ( ( sin ` ( 2 x. A ) ) x. ( cos ` ( 1 x. A ) ) ) + ( ( cos ` ( 2 x. A ) ) x. ( sin ` ( 1 x. A ) ) ) ) = ( ( ( 2 x. ( sin ` A ) ) - ( 2 x. ( ( sin ` A ) ^ 3 ) ) ) + ( ( 1 x. ( sin ` A ) ) - ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) x. ( sin ` A ) ) ) ) )
58 3 15 mulcld 
 |-  ( A e. CC -> ( 2 x. ( sin ` A ) ) e. CC )
59 4 15 mulcld 
 |-  ( A e. CC -> ( 1 x. ( sin ` A ) ) e. CC )
60 3 47 mulcld 
 |-  ( A e. CC -> ( 2 x. ( ( sin ` A ) ^ 3 ) ) e. CC )
61 54 15 mulcld 
 |-  ( A e. CC -> ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) x. ( sin ` A ) ) e. CC )
62 58 59 60 61 addsub4d 
 |-  ( A e. CC -> ( ( ( 2 x. ( sin ` A ) ) + ( 1 x. ( sin ` A ) ) ) - ( ( 2 x. ( ( sin ` A ) ^ 3 ) ) + ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) x. ( sin ` A ) ) ) ) = ( ( ( 2 x. ( sin ` A ) ) - ( 2 x. ( ( sin ` A ) ^ 3 ) ) ) + ( ( 1 x. ( sin ` A ) ) - ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) x. ( sin ` A ) ) ) ) )
63 3 4 15 adddird 
 |-  ( A e. CC -> ( ( 2 + 1 ) x. ( sin ` A ) ) = ( ( 2 x. ( sin ` A ) ) + ( 1 x. ( sin ` A ) ) ) )
64 2p1e3 
 |-  ( 2 + 1 ) = 3
65 64 a1i 
 |-  ( A e. CC -> ( 2 + 1 ) = 3 )
66 65 oveq1d 
 |-  ( A e. CC -> ( ( 2 + 1 ) x. ( sin ` A ) ) = ( 3 x. ( sin ` A ) ) )
67 63 66 eqtr3d 
 |-  ( A e. CC -> ( ( 2 x. ( sin ` A ) ) + ( 1 x. ( sin ` A ) ) ) = ( 3 x. ( sin ` A ) ) )
68 3 3 47 adddird 
 |-  ( A e. CC -> ( ( 2 + 2 ) x. ( ( sin ` A ) ^ 3 ) ) = ( ( 2 x. ( ( sin ` A ) ^ 3 ) ) + ( 2 x. ( ( sin ` A ) ^ 3 ) ) ) )
69 2p2e4 
 |-  ( 2 + 2 ) = 4
70 69 eqcomi 
 |-  4 = ( 2 + 2 )
71 70 a1i 
 |-  ( A e. CC -> 4 = ( 2 + 2 ) )
72 71 oveq1d 
 |-  ( A e. CC -> ( 4 x. ( ( sin ` A ) ^ 3 ) ) = ( ( 2 + 2 ) x. ( ( sin ` A ) ^ 3 ) ) )
73 3 25 15 mulassd 
 |-  ( A e. CC -> ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) x. ( sin ` A ) ) = ( 2 x. ( ( ( sin ` A ) ^ 2 ) x. ( sin ` A ) ) ) )
74 40 oveq2d 
 |-  ( A e. CC -> ( 2 x. ( ( ( sin ` A ) ^ 2 ) x. ( sin ` A ) ) ) = ( 2 x. ( ( sin ` A ) x. ( ( sin ` A ) ^ 2 ) ) ) )
75 41 oveq2d 
 |-  ( A e. CC -> ( 2 x. ( ( sin ` A ) x. ( ( sin ` A ) ^ 2 ) ) ) = ( 2 x. ( ( sin ` A ) ^ 3 ) ) )
76 73 74 75 3eqtrd 
 |-  ( A e. CC -> ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) x. ( sin ` A ) ) = ( 2 x. ( ( sin ` A ) ^ 3 ) ) )
77 76 oveq2d 
 |-  ( A e. CC -> ( ( 2 x. ( ( sin ` A ) ^ 3 ) ) + ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) x. ( sin ` A ) ) ) = ( ( 2 x. ( ( sin ` A ) ^ 3 ) ) + ( 2 x. ( ( sin ` A ) ^ 3 ) ) ) )
78 68 72 77 3eqtr4rd 
 |-  ( A e. CC -> ( ( 2 x. ( ( sin ` A ) ^ 3 ) ) + ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) x. ( sin ` A ) ) ) = ( 4 x. ( ( sin ` A ) ^ 3 ) ) )
79 67 78 oveq12d 
 |-  ( A e. CC -> ( ( ( 2 x. ( sin ` A ) ) + ( 1 x. ( sin ` A ) ) ) - ( ( 2 x. ( ( sin ` A ) ^ 3 ) ) + ( ( 2 x. ( ( sin ` A ) ^ 2 ) ) x. ( sin ` A ) ) ) ) = ( ( 3 x. ( sin ` A ) ) - ( 4 x. ( ( sin ` A ) ^ 3 ) ) ) )
80 57 62 79 3eqtr2d 
 |-  ( A e. CC -> ( ( ( sin ` ( 2 x. A ) ) x. ( cos ` ( 1 x. A ) ) ) + ( ( cos ` ( 2 x. A ) ) x. ( sin ` ( 1 x. A ) ) ) ) = ( ( 3 x. ( sin ` A ) ) - ( 4 x. ( ( sin ` A ) ^ 3 ) ) ) )
81 8 12 80 3eqtrd 
 |-  ( A e. CC -> ( sin ` ( 3 x. A ) ) = ( ( 3 x. ( sin ` A ) ) - ( 4 x. ( ( sin ` A ) ^ 3 ) ) ) )