Step |
Hyp |
Ref |
Expression |
1 |
|
sinasin |
|- ( A e. CC -> ( sin ` ( arcsin ` A ) ) = A ) |
2 |
1
|
3ad2ant1 |
|- ( ( A e. CC /\ B e. CC /\ ( Re ` B ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( sin ` ( arcsin ` A ) ) = A ) |
3 |
|
fveqeq2 |
|- ( ( arcsin ` A ) = B -> ( ( sin ` ( arcsin ` A ) ) = A <-> ( sin ` B ) = A ) ) |
4 |
2 3
|
syl5ibcom |
|- ( ( A e. CC /\ B e. CC /\ ( Re ` B ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( arcsin ` A ) = B -> ( sin ` B ) = A ) ) |
5 |
|
asinsin |
|- ( ( B e. CC /\ ( Re ` B ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( arcsin ` ( sin ` B ) ) = B ) |
6 |
5
|
3adant1 |
|- ( ( A e. CC /\ B e. CC /\ ( Re ` B ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( arcsin ` ( sin ` B ) ) = B ) |
7 |
|
fveqeq2 |
|- ( ( sin ` B ) = A -> ( ( arcsin ` ( sin ` B ) ) = B <-> ( arcsin ` A ) = B ) ) |
8 |
6 7
|
syl5ibcom |
|- ( ( A e. CC /\ B e. CC /\ ( Re ` B ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( sin ` B ) = A -> ( arcsin ` A ) = B ) ) |
9 |
4 8
|
impbid |
|- ( ( A e. CC /\ B e. CC /\ ( Re ` B ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( arcsin ` A ) = B <-> ( sin ` B ) = A ) ) |