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 โ ๐ด ) ) |