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 ( ๐ด โˆˆ โ„‚ โ†’ ( sin โ€˜ ( ( ฯ€ / 2 ) + ๐ด ) ) = ( cos โ€˜ ๐ด ) )

Proof

Step Hyp Ref Expression
1 halfpire โŠข ( ฯ€ / 2 ) โˆˆ โ„
2 1 recni โŠข ( ฯ€ / 2 ) โˆˆ โ„‚
3 sinadd โŠข ( ( ( ฯ€ / 2 ) โˆˆ โ„‚ โˆง ๐ด โˆˆ โ„‚ ) โ†’ ( sin โ€˜ ( ( ฯ€ / 2 ) + ๐ด ) ) = ( ( ( sin โ€˜ ( ฯ€ / 2 ) ) ยท ( cos โ€˜ ๐ด ) ) + ( ( cos โ€˜ ( ฯ€ / 2 ) ) ยท ( sin โ€˜ ๐ด ) ) ) )
4 2 3 mpan โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( sin โ€˜ ( ( ฯ€ / 2 ) + ๐ด ) ) = ( ( ( sin โ€˜ ( ฯ€ / 2 ) ) ยท ( cos โ€˜ ๐ด ) ) + ( ( cos โ€˜ ( ฯ€ / 2 ) ) ยท ( sin โ€˜ ๐ด ) ) ) )
5 sinhalfpi โŠข ( sin โ€˜ ( ฯ€ / 2 ) ) = 1
6 5 oveq1i โŠข ( ( sin โ€˜ ( ฯ€ / 2 ) ) ยท ( cos โ€˜ ๐ด ) ) = ( 1 ยท ( cos โ€˜ ๐ด ) )
7 coscl โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( cos โ€˜ ๐ด ) โˆˆ โ„‚ )
8 7 mulid2d โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( 1 ยท ( cos โ€˜ ๐ด ) ) = ( cos โ€˜ ๐ด ) )
9 6 8 eqtrid โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ( sin โ€˜ ( ฯ€ / 2 ) ) ยท ( cos โ€˜ ๐ด ) ) = ( cos โ€˜ ๐ด ) )
10 coshalfpi โŠข ( cos โ€˜ ( ฯ€ / 2 ) ) = 0
11 10 oveq1i โŠข ( ( cos โ€˜ ( ฯ€ / 2 ) ) ยท ( sin โ€˜ ๐ด ) ) = ( 0 ยท ( sin โ€˜ ๐ด ) )
12 sincl โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( sin โ€˜ ๐ด ) โˆˆ โ„‚ )
13 12 mul02d โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( 0 ยท ( sin โ€˜ ๐ด ) ) = 0 )
14 11 13 eqtrid โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ( cos โ€˜ ( ฯ€ / 2 ) ) ยท ( sin โ€˜ ๐ด ) ) = 0 )
15 9 14 oveq12d โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ( ( sin โ€˜ ( ฯ€ / 2 ) ) ยท ( cos โ€˜ ๐ด ) ) + ( ( cos โ€˜ ( ฯ€ / 2 ) ) ยท ( sin โ€˜ ๐ด ) ) ) = ( ( cos โ€˜ ๐ด ) + 0 ) )
16 7 addid1d โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( ( cos โ€˜ ๐ด ) + 0 ) = ( cos โ€˜ ๐ด ) )
17 4 15 16 3eqtrd โŠข ( ๐ด โˆˆ โ„‚ โ†’ ( sin โ€˜ ( ( ฯ€ / 2 ) + ๐ด ) ) = ( cos โ€˜ ๐ด ) )