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 ( 𝐴 ∈ ℂ → ( sin ‘ ( 3 · 𝐴 ) ) = ( ( 3 · ( sin ‘ 𝐴 ) ) − ( 4 · ( ( sin ‘ 𝐴 ) ↑ 3 ) ) ) )

Proof

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