Theorem sin5t

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

	Ref	Expression
Assertion	sin5t	|- ( A e. CC -> ( sin ` ( 5 x. A ) ) = ( ( ( ; 1 6 x. ( ( sin ` A ) ^ 5 ) ) - ( ; 2 0 x. ( ( sin ` A ) ^ 3 ) ) ) + ( 5 x. ( sin ` A ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		3p2e5	|- ( 3 + 2 ) = 5
2	1	eqcomi	|- 5 = ( 3 + 2 )
3	2	a1i	|- ( A e. CC -> 5 = ( 3 + 2 ) )
4	3	oveq1d	|- ( A e. CC -> ( 5 x. A ) = ( ( 3 + 2 ) x. A ) )
5		3cn	|- 3 e. CC
6	5	a1i	|- ( A e. CC -> 3 e. CC )
7		2cnd	|- ( A e. CC -> 2 e. CC )
8		id	|- ( A e. CC -> A e. CC )
9	6 7 8	adddird	|- ( A e. CC -> ( ( 3 + 2 ) x. A ) = ( ( 3 x. A ) + ( 2 x. A ) ) )
10	4 9	eqtrd	|- ( A e. CC -> ( 5 x. A ) = ( ( 3 x. A ) + ( 2 x. A ) ) )
11	10	fveq2d	|- ( A e. CC -> ( sin ` ( 5 x. A ) ) = ( sin ` ( ( 3 x. A ) + ( 2 x. A ) ) ) )
12	6 8	mulcld	|- ( A e. CC -> ( 3 x. A ) e. CC )
13	7 8	mulcld	|- ( A e. CC -> ( 2 x. A ) e. CC )
14		sinadd	|- ( ( ( 3 x. A ) e. CC /\ ( 2 x. A ) e. CC ) -> ( sin ` ( ( 3 x. A ) + ( 2 x. A ) ) ) = ( ( ( sin ` ( 3 x. A ) ) x. ( cos ` ( 2 x. A ) ) ) + ( ( cos ` ( 3 x. A ) ) x. ( sin ` ( 2 x. A ) ) ) ) )
15	12 13 14	syl2anc	|- ( A e. CC -> ( sin ` ( ( 3 x. A ) + ( 2 x. A ) ) ) = ( ( ( sin ` ( 3 x. A ) ) x. ( cos ` ( 2 x. A ) ) ) + ( ( cos ` ( 3 x. A ) ) x. ( sin ` ( 2 x. A ) ) ) ) )
16		sin3t	|- ( A e. CC -> ( sin ` ( 3 x. A ) ) = ( ( 3 x. ( sin ` A ) ) - ( 4 x. ( ( sin ` A ) ^ 3 ) ) ) )
17		cos2tsin	|- ( A e. CC -> ( cos ` ( 2 x. A ) ) = ( 1 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) )
18	16 17	oveq12d	|- ( A e. CC -> ( ( sin ` ( 3 x. A ) ) x. ( cos ` ( 2 x. A ) ) ) = ( ( ( 3 x. ( sin ` A ) ) - ( 4 x. ( ( sin ` A ) ^ 3 ) ) ) x. ( 1 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) ) )
19		cos3t	|- ( A e. CC -> ( cos ` ( 3 x. A ) ) = ( ( 4 x. ( ( cos ` A ) ^ 3 ) ) - ( 3 x. ( cos ` A ) ) ) )
20		sin2t	|- ( A e. CC -> ( sin ` ( 2 x. A ) ) = ( 2 x. ( ( sin ` A ) x. ( cos ` A ) ) ) )
21	19 20	oveq12d	|- ( A e. CC -> ( ( cos ` ( 3 x. A ) ) x. ( sin ` ( 2 x. A ) ) ) = ( ( ( 4 x. ( ( cos ` A ) ^ 3 ) ) - ( 3 x. ( cos ` A ) ) ) x. ( 2 x. ( ( sin ` A ) x. ( cos ` A ) ) ) ) )
22	18 21	oveq12d	|- ( A e. CC -> ( ( ( sin ` ( 3 x. A ) ) x. ( cos ` ( 2 x. A ) ) ) + ( ( cos ` ( 3 x. A ) ) x. ( sin ` ( 2 x. A ) ) ) ) = ( ( ( ( 3 x. ( sin ` A ) ) - ( 4 x. ( ( sin ` A ) ^ 3 ) ) ) x. ( 1 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) ) + ( ( ( 4 x. ( ( cos ` A ) ^ 3 ) ) - ( 3 x. ( cos ` A ) ) ) x. ( 2 x. ( ( sin ` A ) x. ( cos ` A ) ) ) ) ) )
23	15 22	eqtrd	|- ( A e. CC -> ( sin ` ( ( 3 x. A ) + ( 2 x. A ) ) ) = ( ( ( ( 3 x. ( sin ` A ) ) - ( 4 x. ( ( sin ` A ) ^ 3 ) ) ) x. ( 1 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) ) + ( ( ( 4 x. ( ( cos ` A ) ^ 3 ) ) - ( 3 x. ( cos ` A ) ) ) x. ( 2 x. ( ( sin ` A ) x. ( cos ` A ) ) ) ) ) )
24		coscl	|- ( A e. CC -> ( cos ` A ) e. CC )
25		sincl	|- ( A e. CC -> ( sin ` A ) e. CC )
26	25	sqcld	|- ( A e. CC -> ( ( sin ` A ) ^ 2 ) e. CC )
27	24	sqcld	|- ( A e. CC -> ( ( cos ` A ) ^ 2 ) e. CC )
28		sincossq	|- ( A e. CC -> ( ( ( sin ` A ) ^ 2 ) + ( ( cos ` A ) ^ 2 ) ) = 1 )
29	26 27 28	mvlladdd	|- ( A e. CC -> ( ( cos ` A ) ^ 2 ) = ( 1 - ( ( sin ` A ) ^ 2 ) ) )
30		sin5tlem5	|- ( ( ( cos ` A ) e. CC /\ ( sin ` A ) e. CC /\ ( ( cos ` A ) ^ 2 ) = ( 1 - ( ( sin ` A ) ^ 2 ) ) ) -> ( ( ( ( 3 x. ( sin ` A ) ) - ( 4 x. ( ( sin ` A ) ^ 3 ) ) ) x. ( 1 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) ) + ( ( ( 4 x. ( ( cos ` A ) ^ 3 ) ) - ( 3 x. ( cos ` A ) ) ) x. ( 2 x. ( ( sin ` A ) x. ( cos ` A ) ) ) ) ) = ( ( ( ; 1 6 x. ( ( sin ` A ) ^ 5 ) ) - ( ; 2 0 x. ( ( sin ` A ) ^ 3 ) ) ) + ( 5 x. ( sin ` A ) ) ) )
31	24 25 29 30	syl3anc	|- ( A e. CC -> ( ( ( ( 3 x. ( sin ` A ) ) - ( 4 x. ( ( sin ` A ) ^ 3 ) ) ) x. ( 1 - ( 2 x. ( ( sin ` A ) ^ 2 ) ) ) ) + ( ( ( 4 x. ( ( cos ` A ) ^ 3 ) ) - ( 3 x. ( cos ` A ) ) ) x. ( 2 x. ( ( sin ` A ) x. ( cos ` A ) ) ) ) ) = ( ( ( ; 1 6 x. ( ( sin ` A ) ^ 5 ) ) - ( ; 2 0 x. ( ( sin ` A ) ^ 3 ) ) ) + ( 5 x. ( sin ` A ) ) ) )
32	11 23 31	3eqtrd	|- ( A e. CC -> ( sin ` ( 5 x. A ) ) = ( ( ( ; 1 6 x. ( ( sin ` A ) ^ 5 ) ) - ( ; 2 0 x. ( ( sin ` A ) ^ 3 ) ) ) + ( 5 x. ( sin ` A ) ) ) )