Metamath Proof Explorer


Theorem atanord

Description: The arctangent function is strictly increasing. (Contributed by Mario Carneiro, 5-Apr-2015)

Ref Expression
Assertion atanord
|- ( ( A e. RR /\ B e. RR ) -> ( A < B <-> ( arctan ` A ) < ( arctan ` B ) ) )

Proof

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