Metamath Proof Explorer


Theorem sinhalfpip

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

Ref Expression
Assertion sinhalfpip
|- ( 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 sinadd
 |-  ( ( ( _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 addid1d
 |-  ( A e. CC -> ( ( cos ` A ) + 0 ) = ( cos ` A ) )
17 4 15 16 3eqtrd
 |-  ( A e. CC -> ( sin ` ( ( _pi / 2 ) + A ) ) = ( cos ` A ) )