Metamath Proof Explorer

Theorem acoscosb

Description: Relationship between cosine and arccosine. (Contributed by Mario Carneiro, 2-Apr-2015)

Ref Expression
Assertion acoscosb 
|- ( ( A e. CC /\ B e. CC /\ ( Re ` B ) e. ( 0 (,) _pi ) ) -> ( ( arccos ` A ) = B <-> ( cos ` B ) = A ) )

Proof

Step Hyp Ref Expression
1 cosacos 
 |-  ( A e. CC -> ( cos ` ( arccos ` A ) ) = A )
2 1 3ad2ant1 
 |-  ( ( A e. CC /\ B e. CC /\ ( Re ` B ) e. ( 0 (,) _pi ) ) -> ( cos ` ( arccos ` A ) ) = A )
3 fveqeq2 
 |-  ( ( arccos ` A ) = B -> ( ( cos ` ( arccos ` A ) ) = A <-> ( cos ` B ) = A ) )
4 2 3 syl5ibcom 
 |-  ( ( A e. CC /\ B e. CC /\ ( Re ` B ) e. ( 0 (,) _pi ) ) -> ( ( arccos ` A ) = B -> ( cos ` B ) = A ) )
5 acoscos 
 |-  ( ( B e. CC /\ ( Re ` B ) e. ( 0 (,) _pi ) ) -> ( arccos ` ( cos ` B ) ) = B )
6 5 3adant1 
 |-  ( ( A e. CC /\ B e. CC /\ ( Re ` B ) e. ( 0 (,) _pi ) ) -> ( arccos ` ( cos ` B ) ) = B )
7 fveqeq2 
 |-  ( ( cos ` B ) = A -> ( ( arccos ` ( cos ` B ) ) = B <-> ( arccos ` A ) = B ) )
8 6 7 syl5ibcom 
 |-  ( ( A e. CC /\ B e. CC /\ ( Re ` B ) e. ( 0 (,) _pi ) ) -> ( ( cos ` B ) = A -> ( arccos ` A ) = B ) )
9 4 8 impbid 
 |-  ( ( A e. CC /\ B e. CC /\ ( Re ` B ) e. ( 0 (,) _pi ) ) -> ( ( arccos ` A ) = B <-> ( cos ` B ) = A ) )