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