Step |
Hyp |
Ref |
Expression |
1 |
|
atanbnd |
|- ( A e. RR -> ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) |
2 |
|
atanbnd |
|- ( B e. RR -> ( arctan ` B ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) |
3 |
|
tanord |
|- ( ( ( arctan ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ ( arctan ` B ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( ( arctan ` A ) < ( arctan ` B ) <-> ( tan ` ( arctan ` A ) ) < ( tan ` ( arctan ` B ) ) ) ) |
4 |
1 2 3
|
syl2an |
|- ( ( A e. RR /\ B e. RR ) -> ( ( arctan ` A ) < ( arctan ` B ) <-> ( tan ` ( arctan ` A ) ) < ( tan ` ( arctan ` B ) ) ) ) |
5 |
|
atanre |
|- ( A e. RR -> A e. dom arctan ) |
6 |
|
tanatan |
|- ( A e. dom arctan -> ( tan ` ( arctan ` A ) ) = A ) |
7 |
5 6
|
syl |
|- ( A e. RR -> ( tan ` ( arctan ` A ) ) = A ) |
8 |
|
atanre |
|- ( B e. RR -> B e. dom arctan ) |
9 |
|
tanatan |
|- ( B e. dom arctan -> ( tan ` ( arctan ` B ) ) = B ) |
10 |
8 9
|
syl |
|- ( B e. RR -> ( tan ` ( arctan ` B ) ) = B ) |
11 |
7 10
|
breqan12d |
|- ( ( A e. RR /\ B e. RR ) -> ( ( tan ` ( arctan ` A ) ) < ( tan ` ( arctan ` B ) ) <-> A < B ) ) |
12 |
4 11
|
bitr2d |
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( arctan ` A ) < ( arctan ` B ) ) ) |