This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 mullidd 
 |-  ( 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 ) )