Metamath Proof Explorer

Theorem sin5t

Description: Five-times-angle formula for sine, in pure sine form. (Contributed by Ender Ting, 17-Apr-2026)

Ref Expression
Assertion sin5t ( 𝐴 ∈ ℂ → ( sin ‘ ( 5 · 𝐴 ) ) = ( ( ( 1 6 · ( ( sin ‘ 𝐴 ) ↑ 5 ) ) − ( 2 0 · ( ( sin ‘ 𝐴 ) ↑ 3 ) ) ) + ( 5 · ( sin ‘ 𝐴 ) ) ) )

Proof

Step Hyp Ref Expression
1 3p2e5 ⊢ ( 3 + 2 ) = 5
2 1 eqcomi ⊢ 5 = ( 3 + 2 )
3 2 a1i ⊢ ( 𝐴 ∈ ℂ → 5 = ( 3 + 2 ) )
4 3 oveq1d ⊢ ( 𝐴 ∈ ℂ → ( 5 · 𝐴 ) = ( ( 3 + 2 ) · 𝐴 ) )
5 3cn ⊢ 3 ∈ ℂ
6 5 a1i ⊢ ( 𝐴 ∈ ℂ → 3 ∈ ℂ )
7 2cnd ⊢ ( 𝐴 ∈ ℂ → 2 ∈ ℂ )
8 id ⊢ ( 𝐴 ∈ ℂ → 𝐴 ∈ ℂ )
9 6 7 8 adddird ⊢ ( 𝐴 ∈ ℂ → ( ( 3 + 2 ) · 𝐴 ) = ( ( 3 · 𝐴 ) + ( 2 · 𝐴 ) ) )
10 4 9 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( 5 · 𝐴 ) = ( ( 3 · 𝐴 ) + ( 2 · 𝐴 ) ) )
11 10 fveq2d ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( 5 · 𝐴 ) ) = ( sin ‘ ( ( 3 · 𝐴 ) + ( 2 · 𝐴 ) ) ) )
12 6 8 mulcld ⊢ ( 𝐴 ∈ ℂ → ( 3 · 𝐴 ) ∈ ℂ )
13 7 8 mulcld ⊢ ( 𝐴 ∈ ℂ → ( 2 · 𝐴 ) ∈ ℂ )
14 sinadd ⊢ ( ( ( 3 · 𝐴 ) ∈ ℂ ∧ ( 2 · 𝐴 ) ∈ ℂ ) → ( sin ‘ ( ( 3 · 𝐴 ) + ( 2 · 𝐴 ) ) ) = ( ( ( sin ‘ ( 3 · 𝐴 ) ) · ( cos ‘ ( 2 · 𝐴 ) ) ) + ( ( cos ‘ ( 3 · 𝐴 ) ) · ( sin ‘ ( 2 · 𝐴 ) ) ) ) )
15 12 13 14 syl2anc ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( ( 3 · 𝐴 ) + ( 2 · 𝐴 ) ) ) = ( ( ( sin ‘ ( 3 · 𝐴 ) ) · ( cos ‘ ( 2 · 𝐴 ) ) ) + ( ( cos ‘ ( 3 · 𝐴 ) ) · ( sin ‘ ( 2 · 𝐴 ) ) ) ) )
16 sin3t ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( 3 · 𝐴 ) ) = ( ( 3 · ( sin ‘ 𝐴 ) ) − ( 4 · ( ( sin ‘ 𝐴 ) ↑ 3 ) ) ) )
17 cos2tsin ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 2 · 𝐴 ) ) = ( 1 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) )
18 16 17 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ ( 3 · 𝐴 ) ) · ( cos ‘ ( 2 · 𝐴 ) ) ) = ( ( ( 3 · ( sin ‘ 𝐴 ) ) − ( 4 · ( ( sin ‘ 𝐴 ) ↑ 3 ) ) ) · ( 1 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) )
19 cos3t ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ ( 3 · 𝐴 ) ) = ( ( 4 · ( ( cos ‘ 𝐴 ) ↑ 3 ) ) − ( 3 · ( cos ‘ 𝐴 ) ) ) )
20 sin2t ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( 2 · 𝐴 ) ) = ( 2 · ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) ) )
21 19 20 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ ( 3 · 𝐴 ) ) · ( sin ‘ ( 2 · 𝐴 ) ) ) = ( ( ( 4 · ( ( cos ‘ 𝐴 ) ↑ 3 ) ) − ( 3 · ( cos ‘ 𝐴 ) ) ) · ( 2 · ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) ) ) )
22 18 21 oveq12d ⊢ ( 𝐴 ∈ ℂ → ( ( ( sin ‘ ( 3 · 𝐴 ) ) · ( cos ‘ ( 2 · 𝐴 ) ) ) + ( ( cos ‘ ( 3 · 𝐴 ) ) · ( sin ‘ ( 2 · 𝐴 ) ) ) ) = ( ( ( ( 3 · ( sin ‘ 𝐴 ) ) − ( 4 · ( ( sin ‘ 𝐴 ) ↑ 3 ) ) ) · ( 1 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) + ( ( ( 4 · ( ( cos ‘ 𝐴 ) ↑ 3 ) ) − ( 3 · ( cos ‘ 𝐴 ) ) ) · ( 2 · ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) ) ) ) )
23 15 22 eqtrd ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( ( 3 · 𝐴 ) + ( 2 · 𝐴 ) ) ) = ( ( ( ( 3 · ( sin ‘ 𝐴 ) ) − ( 4 · ( ( sin ‘ 𝐴 ) ↑ 3 ) ) ) · ( 1 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) + ( ( ( 4 · ( ( cos ‘ 𝐴 ) ↑ 3 ) ) − ( 3 · ( cos ‘ 𝐴 ) ) ) · ( 2 · ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) ) ) ) )
24 coscl ⊢ ( 𝐴 ∈ ℂ → ( cos ‘ 𝐴 ) ∈ ℂ )
25 sincl ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ 𝐴 ) ∈ ℂ )
26 25 sqcld ⊢ ( 𝐴 ∈ ℂ → ( ( sin ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
27 24 sqcld ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℂ )
28 sincossq ⊢ ( 𝐴 ∈ ℂ → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = 1 )
29 26 27 28 mvlladdd ⊢ ( 𝐴 ∈ ℂ → ( ( cos ‘ 𝐴 ) ↑ 2 ) = ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) )
30 sin5tlem5 ⊢ ( ( ( cos ‘ 𝐴 ) ∈ ℂ ∧ ( sin ‘ 𝐴 ) ∈ ℂ ∧ ( ( cos ‘ 𝐴 ) ↑ 2 ) = ( 1 − ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) → ( ( ( ( 3 · ( sin ‘ 𝐴 ) ) − ( 4 · ( ( sin ‘ 𝐴 ) ↑ 3 ) ) ) · ( 1 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) + ( ( ( 4 · ( ( cos ‘ 𝐴 ) ↑ 3 ) ) − ( 3 · ( cos ‘ 𝐴 ) ) ) · ( 2 · ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) ) ) ) = ( ( ( 1 6 · ( ( sin ‘ 𝐴 ) ↑ 5 ) ) − ( 2 0 · ( ( sin ‘ 𝐴 ) ↑ 3 ) ) ) + ( 5 · ( sin ‘ 𝐴 ) ) ) )
31 24 25 29 30 syl3anc ⊢ ( 𝐴 ∈ ℂ → ( ( ( ( 3 · ( sin ‘ 𝐴 ) ) − ( 4 · ( ( sin ‘ 𝐴 ) ↑ 3 ) ) ) · ( 1 − ( 2 · ( ( sin ‘ 𝐴 ) ↑ 2 ) ) ) ) + ( ( ( 4 · ( ( cos ‘ 𝐴 ) ↑ 3 ) ) − ( 3 · ( cos ‘ 𝐴 ) ) ) · ( 2 · ( ( sin ‘ 𝐴 ) · ( cos ‘ 𝐴 ) ) ) ) ) = ( ( ( 1 6 · ( ( sin ‘ 𝐴 ) ↑ 5 ) ) − ( 2 0 · ( ( sin ‘ 𝐴 ) ↑ 3 ) ) ) + ( 5 · ( sin ‘ 𝐴 ) ) ) )
32 11 23 31 3eqtrd ⊢ ( 𝐴 ∈ ℂ → ( sin ‘ ( 5 · 𝐴 ) ) = ( ( ( 1 6 · ( ( sin ‘ 𝐴 ) ↑ 5 ) ) − ( 2 0 · ( ( sin ‘ 𝐴 ) ↑ 3 ) ) ) + ( 5 · ( sin ‘ 𝐴 ) ) ) )