Theorem coshalfpip

Description: The cosine of _pi / 2 plus a number. (Contributed by Paul Chapman, 24-Jan-2008)

	Ref	Expression
Assertion	coshalfpip	|- ( A e. CC -> ( cos ` ( ( _pi / 2 ) + A ) ) = -u ( sin ` A ) )

Proof

Step	Hyp	Ref	Expression
1		coshalfpi	|- ( cos ` ( _pi / 2 ) ) = 0
2	1	oveq1i	|- ( ( cos ` ( _pi / 2 ) ) x. ( cos ` A ) ) = ( 0 x. ( cos ` A ) )
3		coscl	|- ( A e. CC -> ( cos ` A ) e. CC )
4	3	mul02d	|- ( A e. CC -> ( 0 x. ( cos ` A ) ) = 0 )
5	2 4	eqtrid	|- ( A e. CC -> ( ( cos ` ( _pi / 2 ) ) x. ( cos ` A ) ) = 0 )
6		sinhalfpi	|- ( sin ` ( _pi / 2 ) ) = 1
7	6	oveq1i	|- ( ( sin ` ( _pi / 2 ) ) x. ( sin ` A ) ) = ( 1 x. ( sin ` A ) )
8		sincl	|- ( A e. CC -> ( sin ` A ) e. CC )
9	8	mulid2d	|- ( A e. CC -> ( 1 x. ( sin ` A ) ) = ( sin ` A ) )
10	7 9	eqtrid	|- ( A e. CC -> ( ( sin ` ( _pi / 2 ) ) x. ( sin ` A ) ) = ( sin ` A ) )
11	5 10	oveq12d	|- ( A e. CC -> ( ( ( cos ` ( _pi / 2 ) ) x. ( cos ` A ) ) - ( ( sin ` ( _pi / 2 ) ) x. ( sin ` A ) ) ) = ( 0 - ( sin ` A ) ) )
12		halfpire	|- ( _pi / 2 ) e. RR
13	12	recni	|- ( _pi / 2 ) e. CC
14		cosadd	|- ( ( ( _pi / 2 ) e. CC /\ A e. CC ) -> ( cos ` ( ( _pi / 2 ) + A ) ) = ( ( ( cos ` ( _pi / 2 ) ) x. ( cos ` A ) ) - ( ( sin ` ( _pi / 2 ) ) x. ( sin ` A ) ) ) )
15	13 14	mpan	|- ( A e. CC -> ( cos ` ( ( _pi / 2 ) + A ) ) = ( ( ( cos ` ( _pi / 2 ) ) x. ( cos ` A ) ) - ( ( sin ` ( _pi / 2 ) ) x. ( sin ` A ) ) ) )
16		df-neg	|- -u ( sin ` A ) = ( 0 - ( sin ` A ) )
17	16	a1i	|- ( A e. CC -> -u ( sin ` A ) = ( 0 - ( sin ` A ) ) )
18	11 15 17	3eqtr4d	|- ( A e. CC -> ( cos ` ( ( _pi / 2 ) + A ) ) = -u ( sin ` A ) )