Metamath Proof Explorer

Theorem sinhalfpim

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

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

Proof

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