Metamath Proof Explorer

Theorem coshalfpim

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

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

Proof

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