Theorem sinppi

Description: Sine of a number plus _pi . (Contributed by NM, 10-Aug-2008)

	Ref	Expression
Assertion	sinppi	|- ( A e. CC -> ( sin ` ( A + _pi ) ) = -u ( sin ` A ) )

Proof

Step	Hyp	Ref	Expression
1		picn	|- _pi e. CC
2		sinadd	|- ( ( A e. CC /\ _pi e. CC ) -> ( sin ` ( A + _pi ) ) = ( ( ( sin ` A ) x. ( cos ` _pi ) ) + ( ( cos ` A ) x. ( sin ` _pi ) ) ) )
3	1 2	mpan2	|- ( A e. CC -> ( sin ` ( A + _pi ) ) = ( ( ( sin ` A ) x. ( cos ` _pi ) ) + ( ( cos ` A ) x. ( sin ` _pi ) ) ) )
4		cospi	|- ( cos ` _pi ) = -u 1
5	4	oveq2i	|- ( ( sin ` A ) x. ( cos ` _pi ) ) = ( ( sin ` A ) x. -u 1 )
6		sincl	|- ( A e. CC -> ( sin ` A ) e. CC )
7		neg1cn	|- -u 1 e. CC
8		mulcom	|- ( ( ( sin ` A ) e. CC /\ -u 1 e. CC ) -> ( ( sin ` A ) x. -u 1 ) = ( -u 1 x. ( sin ` A ) ) )
9	7 8	mpan2	|- ( ( sin ` A ) e. CC -> ( ( sin ` A ) x. -u 1 ) = ( -u 1 x. ( sin ` A ) ) )
10		mulm1	|- ( ( sin ` A ) e. CC -> ( -u 1 x. ( sin ` A ) ) = -u ( sin ` A ) )
11	9 10	eqtrd	|- ( ( sin ` A ) e. CC -> ( ( sin ` A ) x. -u 1 ) = -u ( sin ` A ) )
12	6 11	syl	|- ( A e. CC -> ( ( sin ` A ) x. -u 1 ) = -u ( sin ` A ) )
13	5 12	eqtrid	|- ( A e. CC -> ( ( sin ` A ) x. ( cos ` _pi ) ) = -u ( sin ` A ) )
14		sinpi	|- ( sin ` _pi ) = 0
15	14	oveq2i	|- ( ( cos ` A ) x. ( sin ` _pi ) ) = ( ( cos ` A ) x. 0 )
16		coscl	|- ( A e. CC -> ( cos ` A ) e. CC )
17	16	mul01d	|- ( A e. CC -> ( ( cos ` A ) x. 0 ) = 0 )
18	15 17	eqtrid	|- ( A e. CC -> ( ( cos ` A ) x. ( sin ` _pi ) ) = 0 )
19	13 18	oveq12d	|- ( A e. CC -> ( ( ( sin ` A ) x. ( cos ` _pi ) ) + ( ( cos ` A ) x. ( sin ` _pi ) ) ) = ( -u ( sin ` A ) + 0 ) )
20	6	negcld	|- ( A e. CC -> -u ( sin ` A ) e. CC )
21	20	addridd	|- ( A e. CC -> ( -u ( sin ` A ) + 0 ) = -u ( sin ` A ) )
22	19 21	eqtrd	|- ( A e. CC -> ( ( ( sin ` A ) x. ( cos ` _pi ) ) + ( ( cos ` A ) x. ( sin ` _pi ) ) ) = -u ( sin ` A ) )
23	3 22	eqtrd	|- ( A e. CC -> ( sin ` ( A + _pi ) ) = -u ( sin ` A ) )