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 ) ) |