Metamath Proof Explorer


Theorem atantanb

Description: Relationship between tangent and arctangent. (Contributed by Mario Carneiro, 5-Apr-2015)

Ref Expression
Assertion atantanb
|- ( ( A e. dom arctan /\ B e. CC /\ ( Re ` B ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( arctan ` A ) = B <-> ( tan ` B ) = A ) )

Proof

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