Metamath Proof Explorer

Theorem tanord

Description: The tangent function is strictly increasing on its principal domain. (Contributed by Mario Carneiro, 4-Apr-2015)

Ref Expression
Assertion tanord 
|- ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ B e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( A < B <-> ( tan ` A ) < ( tan ` B ) ) )

Proof

Step Hyp Ref Expression
1 tru 
 |-  T.
2 fveq2 
 |-  ( x = y -> ( tan ` x ) = ( tan ` y ) )
3 fveq2 
 |-  ( x = A -> ( tan ` x ) = ( tan ` A ) )
4 fveq2 
 |-  ( x = B -> ( tan ` x ) = ( tan ` B ) )
5 ioossre 
 |-  ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) C_ RR
6 elioore 
 |-  ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> x e. RR )
7 6 recnd 
 |-  ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> x e. CC )
8 6 rered 
 |-  ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( Re ` x ) = x )
9 id 
 |-  ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
10 8 9 eqeltrd 
 |-  ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( Re ` x ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
11 cosne0 
 |-  ( ( x e. CC /\ ( Re ` x ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` x ) =/= 0 )
12 7 10 11 syl2anc 
 |-  ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( cos ` x ) =/= 0 )
13 6 12 retancld 
 |-  ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( tan ` x ) e. RR )
14 13 adantl 
 |-  ( ( T. /\ x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( tan ` x ) e. RR )
15 6 3ad2ant1 
 |-  ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) -> x e. RR )
16 15 adantr 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) -> x e. RR )
17 16 recnd 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) -> x e. CC )
18 17 negnegd 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) -> -u -u x = x )
19 18 fveq2d 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) -> ( tan ` -u -u x ) = ( tan ` x ) )
20 17 negcld 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) -> -u x e. CC )
21 cosneg 
 |-  ( x e. CC -> ( cos ` -u x ) = ( cos ` x ) )
22 17 21 syl 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) -> ( cos ` -u x ) = ( cos ` x ) )
23 simpl1 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) -> x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
24 23 12 syl 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) -> ( cos ` x ) =/= 0 )
25 22 24 eqnetrd 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) -> ( cos ` -u x ) =/= 0 )
26 tanneg 
 |-  ( ( -u x e. CC /\ ( cos ` -u x ) =/= 0 ) -> ( tan ` -u -u x ) = -u ( tan ` -u x ) )
27 20 25 26 syl2anc 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) -> ( tan ` -u -u x ) = -u ( tan ` -u x ) )
28 19 27 eqtr3d 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) -> ( tan ` x ) = -u ( tan ` -u x ) )
29 15 adantr 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> x e. RR )
30 29 renegcld 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> -u x e. RR )
31 25 adantrr 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> ( cos ` -u x ) =/= 0 )
32 30 31 retancld 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> ( tan ` -u x ) e. RR )
33 32 renegcld 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> -u ( tan ` -u x ) e. RR )
34 0red 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> 0 e. RR )
35 simp2 
 |-  ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) -> y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
36 5 35 sselid 
 |-  ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) -> y e. RR )
37 36 adantr 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> y e. RR )
38 simpl2 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
39 elioore 
 |-  ( y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> y e. RR )
40 39 recnd 
 |-  ( y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> y e. CC )
41 39 rered 
 |-  ( y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( Re ` y ) = y )
42 id 
 |-  ( y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
43 41 42 eqeltrd 
 |-  ( y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( Re ` y ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
44 cosne0 
 |-  ( ( y e. CC /\ ( Re ` y ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( cos ` y ) =/= 0 )
45 40 43 44 syl2anc 
 |-  ( y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( cos ` y ) =/= 0 )
46 38 45 syl 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> ( cos ` y ) =/= 0 )
47 37 46 retancld 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> ( tan ` y ) e. RR )
48 simprl 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> x < 0 )
49 29 lt0neg1d 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> ( x < 0 <-> 0 < -u x ) )
50 48 49 mpbid 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> 0 < -u x )
51 simpl1 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
52 eliooord 
 |-  ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( -u ( _pi / 2 ) < x /\ x < ( _pi / 2 ) ) )
53 51 52 syl 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> ( -u ( _pi / 2 ) < x /\ x < ( _pi / 2 ) ) )
54 53 simpld 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> -u ( _pi / 2 ) < x )
55 halfpire 
 |-  ( _pi / 2 ) e. RR
56 ltnegcon1 
 |-  ( ( ( _pi / 2 ) e. RR /\ x e. RR ) -> ( -u ( _pi / 2 ) < x <-> -u x < ( _pi / 2 ) ) )
57 55 29 56 sylancr 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> ( -u ( _pi / 2 ) < x <-> -u x < ( _pi / 2 ) ) )
58 54 57 mpbid 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> -u x < ( _pi / 2 ) )
59 0xr 
 |-  0 e. RR*
60 55 rexri 
 |-  ( _pi / 2 ) e. RR*
61 elioo2 
 |-  ( ( 0 e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( -u x e. ( 0 (,) ( _pi / 2 ) ) <-> ( -u x e. RR /\ 0 < -u x /\ -u x < ( _pi / 2 ) ) ) )
62 59 60 61 mp2an 
 |-  ( -u x e. ( 0 (,) ( _pi / 2 ) ) <-> ( -u x e. RR /\ 0 < -u x /\ -u x < ( _pi / 2 ) ) )
63 30 50 58 62 syl3anbrc 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> -u x e. ( 0 (,) ( _pi / 2 ) ) )
64 tanrpcl 
 |-  ( -u x e. ( 0 (,) ( _pi / 2 ) ) -> ( tan ` -u x ) e. RR+ )
65 63 64 syl 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> ( tan ` -u x ) e. RR+ )
66 65 rpgt0d 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> 0 < ( tan ` -u x ) )
67 32 lt0neg2d 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> ( 0 < ( tan ` -u x ) <-> -u ( tan ` -u x ) < 0 ) )
68 66 67 mpbid 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> -u ( tan ` -u x ) < 0 )
69 simprr 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> 0 < y )
70 eliooord 
 |-  ( y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( -u ( _pi / 2 ) < y /\ y < ( _pi / 2 ) ) )
71 38 70 syl 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> ( -u ( _pi / 2 ) < y /\ y < ( _pi / 2 ) ) )
72 71 simprd 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> y < ( _pi / 2 ) )
73 elioo2 
 |-  ( ( 0 e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( y e. ( 0 (,) ( _pi / 2 ) ) <-> ( y e. RR /\ 0 < y /\ y < ( _pi / 2 ) ) ) )
74 59 60 73 mp2an 
 |-  ( y e. ( 0 (,) ( _pi / 2 ) ) <-> ( y e. RR /\ 0 < y /\ y < ( _pi / 2 ) ) )
75 37 69 72 74 syl3anbrc 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> y e. ( 0 (,) ( _pi / 2 ) ) )
76 tanrpcl 
 |-  ( y e. ( 0 (,) ( _pi / 2 ) ) -> ( tan ` y ) e. RR+ )
77 75 76 syl 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> ( tan ` y ) e. RR+ )
78 77 rpgt0d 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> 0 < ( tan ` y ) )
79 33 34 47 68 78 lttrd 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ ( x < 0 /\ 0 < y ) ) -> -u ( tan ` -u x ) < ( tan ` y ) )
80 79 anassrs 
 |-  ( ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) /\ 0 < y ) -> -u ( tan ` -u x ) < ( tan ` y ) )
81 simpl3 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> x < y )
82 15 adantr 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> x e. RR )
83 36 adantr 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> y e. RR )
84 82 83 ltnegd 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( x < y <-> -u y < -u x ) )
85 81 84 mpbid 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> -u y < -u x )
86 83 renegcld 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> -u y e. RR )
87 simpr 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> y <_ 0 )
88 83 le0neg1d 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( y <_ 0 <-> 0 <_ -u y ) )
89 87 88 mpbid 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> 0 <_ -u y )
90 simpl2 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
91 90 70 syl 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( -u ( _pi / 2 ) < y /\ y < ( _pi / 2 ) ) )
92 91 simpld 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> -u ( _pi / 2 ) < y )
93 ltnegcon1 
 |-  ( ( ( _pi / 2 ) e. RR /\ y e. RR ) -> ( -u ( _pi / 2 ) < y <-> -u y < ( _pi / 2 ) ) )
94 55 83 93 sylancr 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( -u ( _pi / 2 ) < y <-> -u y < ( _pi / 2 ) ) )
95 92 94 mpbid 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> -u y < ( _pi / 2 ) )
96 0re 
 |-  0 e. RR
97 elico2 
 |-  ( ( 0 e. RR /\ ( _pi / 2 ) e. RR* ) -> ( -u y e. ( 0 [,) ( _pi / 2 ) ) <-> ( -u y e. RR /\ 0 <_ -u y /\ -u y < ( _pi / 2 ) ) ) )
98 96 60 97 mp2an 
 |-  ( -u y e. ( 0 [,) ( _pi / 2 ) ) <-> ( -u y e. RR /\ 0 <_ -u y /\ -u y < ( _pi / 2 ) ) )
99 86 89 95 98 syl3anbrc 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> -u y e. ( 0 [,) ( _pi / 2 ) ) )
100 82 renegcld 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> -u x e. RR )
101 simp3 
 |-  ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) -> x < y )
102 0red 
 |-  ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) -> 0 e. RR )
103 ltletr 
 |-  ( ( x e. RR /\ y e. RR /\ 0 e. RR ) -> ( ( x < y /\ y <_ 0 ) -> x < 0 ) )
104 15 36 102 103 syl3anc 
 |-  ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) -> ( ( x < y /\ y <_ 0 ) -> x < 0 ) )
105 101 104 mpand 
 |-  ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) -> ( y <_ 0 -> x < 0 ) )
106 105 imp 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> x < 0 )
107 ltle 
 |-  ( ( x e. RR /\ 0 e. RR ) -> ( x < 0 -> x <_ 0 ) )
108 82 96 107 sylancl 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( x < 0 -> x <_ 0 ) )
109 106 108 mpd 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> x <_ 0 )
110 82 le0neg1d 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( x <_ 0 <-> 0 <_ -u x ) )
111 109 110 mpbid 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> 0 <_ -u x )
112 simpl1 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
113 112 52 syl 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( -u ( _pi / 2 ) < x /\ x < ( _pi / 2 ) ) )
114 113 simpld 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> -u ( _pi / 2 ) < x )
115 55 82 56 sylancr 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( -u ( _pi / 2 ) < x <-> -u x < ( _pi / 2 ) ) )
116 114 115 mpbid 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> -u x < ( _pi / 2 ) )
117 elico2 
 |-  ( ( 0 e. RR /\ ( _pi / 2 ) e. RR* ) -> ( -u x e. ( 0 [,) ( _pi / 2 ) ) <-> ( -u x e. RR /\ 0 <_ -u x /\ -u x < ( _pi / 2 ) ) ) )
118 96 60 117 mp2an 
 |-  ( -u x e. ( 0 [,) ( _pi / 2 ) ) <-> ( -u x e. RR /\ 0 <_ -u x /\ -u x < ( _pi / 2 ) ) )
119 100 111 116 118 syl3anbrc 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> -u x e. ( 0 [,) ( _pi / 2 ) ) )
120 tanord1 
 |-  ( ( -u y e. ( 0 [,) ( _pi / 2 ) ) /\ -u x e. ( 0 [,) ( _pi / 2 ) ) ) -> ( -u y < -u x <-> ( tan ` -u y ) < ( tan ` -u x ) ) )
121 99 119 120 syl2anc 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( -u y < -u x <-> ( tan ` -u y ) < ( tan ` -u x ) ) )
122 85 121 mpbid 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( tan ` -u y ) < ( tan ` -u x ) )
123 83 recnd 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> y e. CC )
124 cosneg 
 |-  ( y e. CC -> ( cos ` -u y ) = ( cos ` y ) )
125 123 124 syl 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( cos ` -u y ) = ( cos ` y ) )
126 90 45 syl 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( cos ` y ) =/= 0 )
127 125 126 eqnetrd 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( cos ` -u y ) =/= 0 )
128 86 127 retancld 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( tan ` -u y ) e. RR )
129 106 25 syldan 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( cos ` -u x ) =/= 0 )
130 100 129 retancld 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( tan ` -u x ) e. RR )
131 128 130 ltnegd 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( ( tan ` -u y ) < ( tan ` -u x ) <-> -u ( tan ` -u x ) < -u ( tan ` -u y ) ) )
132 122 131 mpbid 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> -u ( tan ` -u x ) < -u ( tan ` -u y ) )
133 123 negnegd 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> -u -u y = y )
134 133 fveq2d 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( tan ` -u -u y ) = ( tan ` y ) )
135 123 negcld 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> -u y e. CC )
136 tanneg 
 |-  ( ( -u y e. CC /\ ( cos ` -u y ) =/= 0 ) -> ( tan ` -u -u y ) = -u ( tan ` -u y ) )
137 135 127 136 syl2anc 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( tan ` -u -u y ) = -u ( tan ` -u y ) )
138 134 137 eqtr3d 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> ( tan ` y ) = -u ( tan ` -u y ) )
139 132 138 breqtrrd 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ y <_ 0 ) -> -u ( tan ` -u x ) < ( tan ` y ) )
140 139 adantlr 
 |-  ( ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) /\ y <_ 0 ) -> -u ( tan ` -u x ) < ( tan ` y ) )
141 0red 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) -> 0 e. RR )
142 simpl2 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) -> y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
143 5 142 sselid 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) -> y e. RR )
144 80 140 141 143 ltlecasei 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) -> -u ( tan ` -u x ) < ( tan ` y ) )
145 28 144 eqbrtrd 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ x < 0 ) -> ( tan ` x ) < ( tan ` y ) )
146 simpl3 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> x < y )
147 15 adantr 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> x e. RR )
148 simpr 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> 0 <_ x )
149 simpl1 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
150 149 52 syl 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> ( -u ( _pi / 2 ) < x /\ x < ( _pi / 2 ) ) )
151 150 simprd 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> x < ( _pi / 2 ) )
152 elico2 
 |-  ( ( 0 e. RR /\ ( _pi / 2 ) e. RR* ) -> ( x e. ( 0 [,) ( _pi / 2 ) ) <-> ( x e. RR /\ 0 <_ x /\ x < ( _pi / 2 ) ) ) )
153 96 60 152 mp2an 
 |-  ( x e. ( 0 [,) ( _pi / 2 ) ) <-> ( x e. RR /\ 0 <_ x /\ x < ( _pi / 2 ) ) )
154 147 148 151 153 syl3anbrc 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> x e. ( 0 [,) ( _pi / 2 ) ) )
155 simpl2 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
156 5 155 sselid 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> y e. RR )
157 0red 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> 0 e. RR )
158 147 156 146 ltled 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> x <_ y )
159 157 147 156 148 158 letrd 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> 0 <_ y )
160 155 70 syl 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> ( -u ( _pi / 2 ) < y /\ y < ( _pi / 2 ) ) )
161 160 simprd 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> y < ( _pi / 2 ) )
162 elico2 
 |-  ( ( 0 e. RR /\ ( _pi / 2 ) e. RR* ) -> ( y e. ( 0 [,) ( _pi / 2 ) ) <-> ( y e. RR /\ 0 <_ y /\ y < ( _pi / 2 ) ) ) )
163 96 60 162 mp2an 
 |-  ( y e. ( 0 [,) ( _pi / 2 ) ) <-> ( y e. RR /\ 0 <_ y /\ y < ( _pi / 2 ) ) )
164 156 159 161 163 syl3anbrc 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> y e. ( 0 [,) ( _pi / 2 ) ) )
165 tanord1 
 |-  ( ( x e. ( 0 [,) ( _pi / 2 ) ) /\ y e. ( 0 [,) ( _pi / 2 ) ) ) -> ( x < y <-> ( tan ` x ) < ( tan ` y ) ) )
166 154 164 165 syl2anc 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> ( x < y <-> ( tan ` x ) < ( tan ` y ) ) )
167 146 166 mpbid 
 |-  ( ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) /\ 0 <_ x ) -> ( tan ` x ) < ( tan ` y ) )
168 145 167 15 102 ltlecasei 
 |-  ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ x < y ) -> ( tan ` x ) < ( tan ` y ) )
169 168 3expia 
 |-  ( ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( x < y -> ( tan ` x ) < ( tan ` y ) ) )
170 169 adantl 
 |-  ( ( T. /\ ( x e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ y e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) ) -> ( x < y -> ( tan ` x ) < ( tan ` y ) ) )
171 2 3 4 5 14 170 ltord1 
 |-  ( ( T. /\ ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ B e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) ) -> ( A < B <-> ( tan ` A ) < ( tan ` B ) ) )
172 1 171 mpan 
 |-  ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) /\ B e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( A < B <-> ( tan ` A ) < ( tan ` B ) ) )