MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  tanord Structured version   Unicode version

Theorem tanord 22653
Description: The tangent function is strictly increasing on its principal domain. (Contributed by Mario Carneiro, 4-Apr-2015.)
Assertion
Ref Expression
tanord  |-  ( ( A  e.  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) )  /\  B  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) ) )  ->  ( A  <  B  <->  ( tan `  A )  <  ( tan `  B ) ) )

Proof of Theorem tanord
Dummy variables  x  y are mutually distinct and distinct from all other variables.
StepHypRef Expression
1 tru 1378 . 2  |- T.
2 fveq2 5859 . . 3  |-  ( x  =  y  ->  ( tan `  x )  =  ( tan `  y
) )
3 fveq2 5859 . . 3  |-  ( x  =  A  ->  ( tan `  x )  =  ( tan `  A
) )
4 fveq2 5859 . . 3  |-  ( x  =  B  ->  ( tan `  x )  =  ( tan `  B
) )
5 ioossre 11577 . . 3  |-  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) ) 
C_  RR
6 elioore 11550 . . . . 5  |-  ( x  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  ->  x  e.  RR )
76recnd 9613 . . . . . 6  |-  ( x  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  ->  x  e.  CC )
86rered 13009 . . . . . . 7  |-  ( x  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  -> 
( Re `  x
)  =  x )
9 id 22 . . . . . . 7  |-  ( x  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  ->  x  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) ) )
108, 9eqeltrd 2550 . . . . . 6  |-  ( x  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  -> 
( Re `  x
)  e.  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) ) )
11 cosne0 22645 . . . . . 6  |-  ( ( x  e.  CC  /\  ( Re `  x )  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) ) )  ->  ( cos `  x
)  =/=  0 )
127, 10, 11syl2anc 661 . . . . 5  |-  ( x  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  -> 
( cos `  x
)  =/=  0 )
136, 12retancld 13732 . . . 4  |-  ( x  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  -> 
( tan `  x
)  e.  RR )
1413adantl 466 . . 3  |-  ( ( T.  /\  x  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) ) )  -> 
( tan `  x
)  e.  RR )
1563ad2ant1 1012 . . . . . . . . . . . 12  |-  ( ( x  e.  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) )  /\  y  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  x  < 
y )  ->  x  e.  RR )
1615adantr 465 . . . . . . . . . . 11  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  x  <  0 )  ->  x  e.  RR )
1716recnd 9613 . . . . . . . . . 10  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  x  <  0 )  ->  x  e.  CC )
1817negnegd 9912 . . . . . . . . 9  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  x  <  0 )  ->  -u -u x  =  x )
1918fveq2d 5863 . . . . . . . 8  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  x  <  0 )  ->  ( tan `  -u -u x )  =  ( tan `  x
) )
2017negcld 9908 . . . . . . . . 9  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  x  <  0 )  ->  -u x  e.  CC )
21 cosneg 13734 . . . . . . . . . . 11  |-  ( x  e.  CC  ->  ( cos `  -u x )  =  ( cos `  x
) )
2217, 21syl 16 . . . . . . . . . 10  |-  ( ( ( 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 994 . . . . . . . . . . 11  |-  ( ( ( 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
) ) )
2423, 12syl 16 . . . . . . . . . 10  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  x  <  0 )  ->  ( cos `  x )  =/=  0 )
2522, 24eqnetrd 2755 . . . . . . . . 9  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  x  <  0 )  ->  ( cos `  -u x )  =/=  0 )
26 tanneg 13735 . . . . . . . . 9  |-  ( (
-u x  e.  CC  /\  ( cos `  -u x
)  =/=  0 )  ->  ( tan `  -u -u x
)  =  -u ( tan `  -u x ) )
2720, 25, 26syl2anc 661 . . . . . . . 8  |-  ( ( ( 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
) )
2819, 27eqtr3d 2505 . . . . . . 7  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  x  <  0 )  ->  ( tan `  x )  = 
-u ( tan `  -u x
) )
2915adantr 465 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  (
x  <  0  /\  0  <  y ) )  ->  x  e.  RR )
3029renegcld 9977 . . . . . . . . . . . 12  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  (
x  <  0  /\  0  <  y ) )  ->  -u x  e.  RR )
3125adantrr 716 . . . . . . . . . . . 12  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  (
x  <  0  /\  0  <  y ) )  ->  ( cos `  -u x
)  =/=  0 )
3230, 31retancld 13732 . . . . . . . . . . 11  |-  ( ( ( 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 )
3332renegcld 9977 . . . . . . . . . 10  |-  ( ( ( 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 9588 . . . . . . . . . 10  |-  ( ( ( 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 992 . . . . . . . . . . . . 13  |-  ( ( x  e.  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) )  /\  y  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  x  < 
y )  ->  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) ) )
365, 35sseldi 3497 . . . . . . . . . . . 12  |-  ( ( x  e.  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) )  /\  y  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  x  < 
y )  ->  y  e.  RR )
3736adantr 465 . . . . . . . . . . 11  |-  ( ( ( 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 995 . . . . . . . . . . . 12  |-  ( ( ( 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 11550 . . . . . . . . . . . . . 14  |-  ( y  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  -> 
y  e.  RR )
4039recnd 9613 . . . . . . . . . . . . 13  |-  ( y  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  -> 
y  e.  CC )
4139rered 13009 . . . . . . . . . . . . . 14  |-  ( y  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  -> 
( Re `  y
)  =  y )
42 id 22 . . . . . . . . . . . . . 14  |-  ( y  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  -> 
y  e.  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) ) )
4341, 42eqeltrd 2550 . . . . . . . . . . . . 13  |-  ( y  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  -> 
( Re `  y
)  e.  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) ) )
44 cosne0 22645 . . . . . . . . . . . . 13  |-  ( ( y  e.  CC  /\  ( Re `  y )  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) ) )  ->  ( cos `  y
)  =/=  0 )
4540, 43, 44syl2anc 661 . . . . . . . . . . . 12  |-  ( y  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  -> 
( cos `  y
)  =/=  0 )
4638, 45syl 16 . . . . . . . . . . 11  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  (
x  <  0  /\  0  <  y ) )  ->  ( cos `  y
)  =/=  0 )
4737, 46retancld 13732 . . . . . . . . . 10  |-  ( ( ( 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 755 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  (
x  <  0  /\  0  <  y ) )  ->  x  <  0
)
4929lt0neg1d 10113 . . . . . . . . . . . . . . 15  |-  ( ( ( 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
) )
5048, 49mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( ( 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 994 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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 11575 . . . . . . . . . . . . . . . . 17  |-  ( x  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  -> 
( -u ( pi  / 
2 )  <  x  /\  x  <  ( pi 
/  2 ) ) )
5351, 52syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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
) ) )
5453simpld 459 . . . . . . . . . . . . . . 15  |-  ( ( ( 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 22585 . . . . . . . . . . . . . . . 16  |-  ( pi 
/  2 )  e.  RR
56 ltnegcon1 10044 . . . . . . . . . . . . . . . 16  |-  ( ( ( pi  /  2
)  e.  RR  /\  x  e.  RR )  ->  ( -u ( pi 
/  2 )  < 
x  <->  -u x  <  (
pi  /  2 ) ) )
5755, 29, 56sylancr 663 . . . . . . . . . . . . . . 15  |-  ( ( ( 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
) ) )
5854, 57mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( ( 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 9631 . . . . . . . . . . . . . . 15  |-  0  e.  RR*
6055rexri 9637 . . . . . . . . . . . . . . 15  |-  ( pi 
/  2 )  e. 
RR*
61 elioo2 11561 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  RR*  /\  (
pi  /  2 )  e.  RR* )  ->  ( -u x  e.  ( 0 (,) ( pi  / 
2 ) )  <->  ( -u x  e.  RR  /\  0  <  -u x  /\  -u x  <  ( pi  /  2
) ) ) )
6259, 60, 61mp2an 672 . . . . . . . . . . . . . 14  |-  ( -u x  e.  ( 0 (,) ( pi  / 
2 ) )  <->  ( -u x  e.  RR  /\  0  <  -u x  /\  -u x  <  ( pi  /  2
) ) )
6330, 50, 58, 62syl3anbrc 1175 . . . . . . . . . . . . 13  |-  ( ( ( 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 22625 . . . . . . . . . . . . 13  |-  ( -u x  e.  ( 0 (,) ( pi  / 
2 ) )  -> 
( tan `  -u x
)  e.  RR+ )
6563, 64syl 16 . . . . . . . . . . . 12  |-  ( ( ( 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+ )
6665rpgt0d 11250 . . . . . . . . . . 11  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  (
x  <  0  /\  0  <  y ) )  ->  0  <  ( tan `  -u x ) )
6732lt0neg2d 10114 . . . . . . . . . . 11  |-  ( ( ( 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 ) )
6866, 67mpbid 210 . . . . . . . . . 10  |-  ( ( ( 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 756 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  (
x  <  0  /\  0  <  y ) )  ->  0  <  y
)
70 eliooord 11575 . . . . . . . . . . . . . . 15  |-  ( y  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  -> 
( -u ( pi  / 
2 )  <  y  /\  y  <  ( pi 
/  2 ) ) )
7138, 70syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( 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
) ) )
7271simprd 463 . . . . . . . . . . . . 13  |-  ( ( ( 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 11561 . . . . . . . . . . . . . 14  |-  ( ( 0  e.  RR*  /\  (
pi  /  2 )  e.  RR* )  ->  (
y  e.  ( 0 (,) ( pi  / 
2 ) )  <->  ( y  e.  RR  /\  0  < 
y  /\  y  <  ( pi  /  2 ) ) ) )
7459, 60, 73mp2an 672 . . . . . . . . . . . . 13  |-  ( y  e.  ( 0 (,) ( pi  /  2
) )  <->  ( y  e.  RR  /\  0  < 
y  /\  y  <  ( pi  /  2 ) ) )
7537, 69, 72, 74syl3anbrc 1175 . . . . . . . . . . . 12  |-  ( ( ( 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 22625 . . . . . . . . . . . 12  |-  ( y  e.  ( 0 (,) ( pi  /  2
) )  ->  ( tan `  y )  e.  RR+ )
7775, 76syl 16 . . . . . . . . . . 11  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  (
x  <  0  /\  0  <  y ) )  ->  ( tan `  y
)  e.  RR+ )
7877rpgt0d 11250 . . . . . . . . . 10  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  (
x  <  0  /\  0  <  y ) )  ->  0  <  ( tan `  y ) )
7933, 34, 47, 68, 78lttrd 9733 . . . . . . . . 9  |-  ( ( ( 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 ) )
8079anassrs 648 . . . . . . . 8  |-  ( ( ( ( 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 996 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  x  <  y )
8215adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  x  e.  RR )
8336adantr 465 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  y  e.  RR )
8482, 83ltnegd 10121 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  (
x  <  y  <->  -u y  <  -u x ) )
8581, 84mpbid 210 . . . . . . . . . . . 12  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  -u y  <  -u x )
8683renegcld 9977 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  -u y  e.  RR )
87 simpr 461 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  y  <_  0 )
8883le0neg1d 10115 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  (
y  <_  0  <->  0  <_  -u y ) )
8987, 88mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  0  <_ 
-u y )
90 simpl2 995 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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
) ) )
9190, 70syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) )
9291simpld 459 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  -u (
pi  /  2 )  <  y )
93 ltnegcon1 10044 . . . . . . . . . . . . . . . 16  |-  ( ( ( pi  /  2
)  e.  RR  /\  y  e.  RR )  ->  ( -u ( pi 
/  2 )  < 
y  <->  -u y  <  (
pi  /  2 ) ) )
9455, 83, 93sylancr 663 . . . . . . . . . . . . . . 15  |-  ( ( ( 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
) ) )
9592, 94mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  -u y  <  ( pi  /  2
) )
96 0re 9587 . . . . . . . . . . . . . . 15  |-  0  e.  RR
97 elico2 11579 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  RR  /\  ( pi  /  2
)  e.  RR* )  ->  ( -u y  e.  ( 0 [,) (
pi  /  2 ) )  <->  ( -u y  e.  RR  /\  0  <_  -u y  /\  -u y  <  ( pi  /  2
) ) ) )
9896, 60, 97mp2an 672 . . . . . . . . . . . . . 14  |-  ( -u y  e.  ( 0 [,) ( pi  / 
2 ) )  <->  ( -u y  e.  RR  /\  0  <_  -u y  /\  -u y  <  ( pi  /  2
) ) )
9986, 89, 95, 98syl3anbrc 1175 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  -u y  e.  ( 0 [,) (
pi  /  2 ) ) )
10082renegcld 9977 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  -u x  e.  RR )
101 simp3 993 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) )  /\  y  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  x  < 
y )  ->  x  <  y )
102 0red 9588 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) )  /\  y  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  x  < 
y )  ->  0  e.  RR )
103 ltletr 9667 . . . . . . . . . . . . . . . . . . 19  |-  ( ( x  e.  RR  /\  y  e.  RR  /\  0  e.  RR )  ->  (
( x  <  y  /\  y  <_  0 )  ->  x  <  0
) )
10415, 36, 102, 103syl3anc 1223 . . . . . . . . . . . . . . . . . 18  |-  ( ( x  e.  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) )  /\  y  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  x  < 
y )  ->  (
( x  <  y  /\  y  <_  0 )  ->  x  <  0
) )
105101, 104mpand 675 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) )  /\  y  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  x  < 
y )  ->  (
y  <_  0  ->  x  <  0 ) )
106105imp 429 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  x  <  0 )
107 ltle 9664 . . . . . . . . . . . . . . . . 17  |-  ( ( x  e.  RR  /\  0  e.  RR )  ->  ( x  <  0  ->  x  <_  0 ) )
10882, 96, 107sylancl 662 . . . . . . . . . . . . . . . 16  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  (
x  <  0  ->  x  <_  0 ) )
109106, 108mpd 15 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  x  <_  0 )
11082le0neg1d 10115 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  (
x  <_  0  <->  0  <_  -u x ) )
111109, 110mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  0  <_ 
-u x )
112 simpl1 994 . . . . . . . . . . . . . . . . 17  |-  ( ( ( 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
) ) )
113112, 52syl 16 . . . . . . . . . . . . . . . 16  |-  ( ( ( 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 ) ) )
114113simpld 459 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  -u (
pi  /  2 )  <  x )
11555, 82, 56sylancr 663 . . . . . . . . . . . . . . 15  |-  ( ( ( 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
) ) )
116114, 115mpbid 210 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  -u x  <  ( pi  /  2
) )
117 elico2 11579 . . . . . . . . . . . . . . 15  |-  ( ( 0  e.  RR  /\  ( pi  /  2
)  e.  RR* )  ->  ( -u x  e.  ( 0 [,) (
pi  /  2 ) )  <->  ( -u x  e.  RR  /\  0  <_  -u x  /\  -u x  <  ( pi  /  2
) ) ) )
11896, 60, 117mp2an 672 . . . . . . . . . . . . . 14  |-  ( -u x  e.  ( 0 [,) ( pi  / 
2 ) )  <->  ( -u x  e.  RR  /\  0  <_  -u x  /\  -u x  <  ( pi  /  2
) ) )
119100, 111, 116, 118syl3anbrc 1175 . . . . . . . . . . . . 13  |-  ( ( ( 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 22652 . . . . . . . . . . . . 13  |-  ( (
-u y  e.  ( 0 [,) ( pi 
/  2 ) )  /\  -u x  e.  ( 0 [,) ( pi 
/  2 ) ) )  ->  ( -u y  <  -u x  <->  ( tan `  -u y )  <  ( tan `  -u x ) ) )
12199, 119, 120syl2anc 661 . . . . . . . . . . . 12  |-  ( ( ( 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 ) ) )
12285, 121mpbid 210 . . . . . . . . . . 11  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  ( tan `  -u y )  < 
( tan `  -u x
) )
12383recnd 9613 . . . . . . . . . . . . . . 15  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  y  e.  CC )
124 cosneg 13734 . . . . . . . . . . . . . . 15  |-  ( y  e.  CC  ->  ( cos `  -u y )  =  ( cos `  y
) )
125123, 124syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  ( cos `  -u y )  =  ( cos `  y
) )
12690, 45syl 16 . . . . . . . . . . . . . 14  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  ( cos `  y )  =/=  0 )
127125, 126eqnetrd 2755 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  ( cos `  -u y )  =/=  0 )
12886, 127retancld 13732 . . . . . . . . . . . 12  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  ( tan `  -u y )  e.  RR )
129106, 25syldan 470 . . . . . . . . . . . . 13  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  ( cos `  -u x )  =/=  0 )
130100, 129retancld 13732 . . . . . . . . . . . 12  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  ( tan `  -u x )  e.  RR )
131128, 130ltnegd 10121 . . . . . . . . . . 11  |-  ( ( ( 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
) ) )
132122, 131mpbid 210 . . . . . . . . . 10  |-  ( ( ( 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
) )
133123negnegd 9912 . . . . . . . . . . . 12  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  -u -u y  =  y )
134133fveq2d 5863 . . . . . . . . . . 11  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  ( tan `  -u -u y )  =  ( tan `  y
) )
135123negcld 9908 . . . . . . . . . . . 12  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  -u y  e.  CC )
136 tanneg 13735 . . . . . . . . . . . 12  |-  ( (
-u y  e.  CC  /\  ( cos `  -u y
)  =/=  0 )  ->  ( tan `  -u -u y
)  =  -u ( tan `  -u y ) )
137135, 127, 136syl2anc 661 . . . . . . . . . . 11  |-  ( ( ( 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
) )
138134, 137eqtr3d 2505 . . . . . . . . . 10  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  ( tan `  y )  = 
-u ( tan `  -u y
) )
139132, 138breqtrrd 4468 . . . . . . . . 9  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  y  <_  0 )  ->  -u ( tan `  -u x )  < 
( tan `  y
) )
140139adantlr 714 . . . . . . . 8  |-  ( ( ( ( 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 9588 . . . . . . . 8  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  x  <  0 )  ->  0  e.  RR )
142 simpl2 995 . . . . . . . . 9  |-  ( ( ( 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
) ) )
1435, 142sseldi 3497 . . . . . . . 8  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  x  <  0 )  ->  y  e.  RR )
14480, 140, 141, 143ltlecasei 9683 . . . . . . 7  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  x  <  0 )  ->  -u ( tan `  -u x )  < 
( tan `  y
) )
14528, 144eqbrtrd 4462 . . . . . 6  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  x  <  0 )  ->  ( tan `  x )  < 
( tan `  y
) )
146 simpl3 996 . . . . . . 7  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  0  <_  x )  ->  x  <  y )
14715adantr 465 . . . . . . . . 9  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  0  <_  x )  ->  x  e.  RR )
148 simpr 461 . . . . . . . . 9  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  0  <_  x )  ->  0  <_  x )
149 simpl1 994 . . . . . . . . . . 11  |-  ( ( ( 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
) ) )
150149, 52syl 16 . . . . . . . . . 10  |-  ( ( ( 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 ) ) )
151150simprd 463 . . . . . . . . 9  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  0  <_  x )  ->  x  <  ( pi  /  2
) )
152 elico2 11579 . . . . . . . . . 10  |-  ( ( 0  e.  RR  /\  ( pi  /  2
)  e.  RR* )  ->  ( x  e.  ( 0 [,) ( pi 
/  2 ) )  <-> 
( x  e.  RR  /\  0  <_  x  /\  x  <  ( pi  / 
2 ) ) ) )
15396, 60, 152mp2an 672 . . . . . . . . 9  |-  ( x  e.  ( 0 [,) ( pi  /  2
) )  <->  ( x  e.  RR  /\  0  <_  x  /\  x  <  (
pi  /  2 ) ) )
154147, 148, 151, 153syl3anbrc 1175 . . . . . . . 8  |-  ( ( ( 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 995 . . . . . . . . . 10  |-  ( ( ( 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
) ) )
1565, 155sseldi 3497 . . . . . . . . 9  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  0  <_  x )  ->  y  e.  RR )
157 0red 9588 . . . . . . . . . 10  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  0  <_  x )  ->  0  e.  RR )
158147, 156, 146ltled 9723 . . . . . . . . . 10  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  0  <_  x )  ->  x  <_  y )
159157, 147, 156, 148, 158letrd 9729 . . . . . . . . 9  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  0  <_  x )  ->  0  <_  y )
160155, 70syl 16 . . . . . . . . . 10  |-  ( ( ( 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 ) ) )
161160simprd 463 . . . . . . . . 9  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  0  <_  x )  ->  y  <  ( pi  /  2
) )
162 elico2 11579 . . . . . . . . . 10  |-  ( ( 0  e.  RR  /\  ( pi  /  2
)  e.  RR* )  ->  ( y  e.  ( 0 [,) ( pi 
/  2 ) )  <-> 
( y  e.  RR  /\  0  <_  y  /\  y  <  ( pi  / 
2 ) ) ) )
16396, 60, 162mp2an 672 . . . . . . . . 9  |-  ( y  e.  ( 0 [,) ( pi  /  2
) )  <->  ( y  e.  RR  /\  0  <_ 
y  /\  y  <  ( pi  /  2 ) ) )
164156, 159, 161, 163syl3anbrc 1175 . . . . . . . 8  |-  ( ( ( 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 22652 . . . . . . . 8  |-  ( ( x  e.  ( 0 [,) ( pi  / 
2 ) )  /\  y  e.  ( 0 [,) ( pi  / 
2 ) ) )  ->  ( x  < 
y  <->  ( tan `  x
)  <  ( tan `  y ) ) )
166154, 164, 165syl2anc 661 . . . . . . 7  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  0  <_  x )  ->  (
x  <  y  <->  ( tan `  x )  <  ( tan `  y ) ) )
167146, 166mpbid 210 . . . . . 6  |-  ( ( ( x  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  y  e.  ( -u ( pi 
/  2 ) (,) ( pi  /  2
) )  /\  x  <  y )  /\  0  <_  x )  ->  ( tan `  x )  < 
( tan `  y
) )
168145, 167, 15, 102ltlecasei 9683 . . . . 5  |-  ( ( x  e.  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) )  /\  y  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) )  /\  x  < 
y )  ->  ( tan `  x )  < 
( tan `  y
) )
1691683expia 1193 . . . 4  |-  ( ( x  e.  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) )  /\  y  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) ) )  ->  (
x  <  y  ->  ( tan `  x )  <  ( tan `  y
) ) )
170169adantl 466 . . 3  |-  ( ( T.  /\  ( x  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  /\  y  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) ) ) )  ->  ( x  <  y  ->  ( tan `  x )  <  ( tan `  y ) ) )
1712, 3, 4, 5, 14, 170ltord1 10070 . 2  |-  ( ( T.  /\  ( A  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) )  /\  B  e.  ( -u (
pi  /  2 ) (,) ( pi  / 
2 ) ) ) )  ->  ( A  <  B  <->  ( tan `  A
)  <  ( tan `  B ) ) )
1721, 171mpan 670 1  |-  ( ( A  e.  ( -u ( pi  /  2
) (,) ( pi 
/  2 ) )  /\  B  e.  (
-u ( pi  / 
2 ) (,) (
pi  /  2 ) ) )  ->  ( A  <  B  <->  ( tan `  A )  <  ( tan `  B ) ) )
Colors of variables: wff setvar class
Syntax hints:    -> wi 4    <-> wb 184    /\ wa 369    /\ w3a 968    = wceq 1374   T. wtru 1375    e. wcel 1762    =/= wne 2657   class class class wbr 4442   ` cfv 5581  (class class class)co 6277   CCcc 9481   RRcr 9482   0cc0 9483   RR*cxr 9618    < clt 9619    <_ cle 9620   -ucneg 9797    / cdiv 10197   2c2 10576   RR+crp 11211   (,)cioo 11520   [,)cico 11522   Recre 12882   cosccos 13653   tanctan 13654   picpi 13655
This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8  ax-gen 1596  ax-4 1607  ax-5 1675  ax-6 1714  ax-7 1734  ax-8 1764  ax-9 1766  ax-10 1781  ax-11 1786  ax-12 1798  ax-13 1963  ax-ext 2440  ax-rep 4553  ax-sep 4563  ax-nul 4571  ax-pow 4620  ax-pr 4681  ax-un 6569  ax-inf2 8049  ax-cnex 9539  ax-resscn 9540  ax-1cn 9541  ax-icn 9542  ax-addcl 9543  ax-addrcl 9544  ax-mulcl 9545  ax-mulrcl 9546  ax-mulcom 9547  ax-addass 9548  ax-mulass 9549  ax-distr 9550  ax-i2m1 9551  ax-1ne0 9552  ax-1rid 9553  ax-rnegex 9554  ax-rrecex 9555  ax-cnre 9556  ax-pre-lttri 9557  ax-pre-lttrn 9558  ax-pre-ltadd 9559  ax-pre-mulgt0 9560  ax-pre-sup 9561  ax-addf 9562  ax-mulf 9563
This theorem depends on definitions:  df-bi 185  df-or 370  df-an 371  df-3or 969  df-3an 970  df-tru 1377  df-fal 1380  df-ex 1592  df-nf 1595  df-sb 1707  df-eu 2274  df-mo 2275  df-clab 2448  df-cleq 2454  df-clel 2457  df-nfc 2612  df-ne 2659  df-nel 2660  df-ral 2814  df-rex 2815  df-reu 2816  df-rmo 2817  df-rab 2818  df-v 3110  df-sbc 3327  df-csb 3431  df-dif 3474  df-un 3476  df-in 3478  df-ss 3485  df-pss 3487  df-nul 3781  df-if 3935  df-pw 4007  df-sn 4023  df-pr 4025  df-tp 4027  df-op 4029  df-uni 4241  df-int 4278  df-iun 4322  df-iin 4323  df-br 4443  df-opab 4501  df-mpt 4502  df-tr 4536  df-eprel 4786  df-id 4790  df-po 4795  df-so 4796  df-fr 4833  df-se 4834  df-we 4835  df-ord 4876  df-on 4877  df-lim 4878  df-suc 4879  df-xp 5000  df-rel 5001  df-cnv 5002  df-co 5003  df-dm 5004  df-rn 5005  df-res 5006  df-ima 5007  df-iota 5544  df-fun 5583  df-fn 5584  df-f 5585  df-f1 5586  df-fo 5587  df-f1o 5588  df-fv 5589  df-isom 5590  df-riota 6238  df-ov 6280  df-oprab 6281  df-mpt2 6282  df-of 6517  df-om 6674  df-1st 6776  df-2nd 6777  df-supp 6894  df-recs 7034  df-rdg 7068  df-1o 7122  df-2o 7123  df-oadd 7126  df-er 7303  df-map 7414  df-pm 7415  df-ixp 7462  df-en 7509  df-dom 7510  df-sdom 7511  df-fin 7512  df-fsupp 7821  df-fi 7862  df-sup 7892  df-oi 7926  df-card 8311  df-cda 8539  df-pnf 9621  df-mnf 9622  df-xr 9623  df-ltxr 9624  df-le 9625  df-sub 9798  df-neg 9799  df-div 10198  df-nn 10528  df-2 10585  df-3 10586  df-4 10587  df-5 10588  df-6 10589  df-7 10590  df-8 10591  df-9 10592  df-10 10593  df-n0 10787  df-z 10856  df-dec 10968  df-uz 11074  df-q 11174  df-rp 11212  df-xneg 11309  df-xadd 11310  df-xmul 11311  df-ioo 11524  df-ioc 11525  df-ico 11526  df-icc 11527  df-fz 11664  df-fzo 11784  df-fl 11888  df-mod 11955  df-seq 12066  df-exp 12125  df-fac 12311  df-bc 12338  df-hash 12363  df-shft 12852  df-cj 12884  df-re 12885  df-im 12886  df-sqr 13020  df-abs 13021  df-limsup 13245  df-clim 13262  df-rlim 13263  df-sum 13460  df-ef 13656  df-sin 13658  df-cos 13659  df-tan 13660  df-pi 13661  df-struct 14483  df-ndx 14484  df-slot 14485  df-base 14486  df-sets 14487  df-ress 14488  df-plusg 14559  df-mulr 14560  df-starv 14561  df-sca 14562  df-vsca 14563  df-ip 14564  df-tset 14565  df-ple 14566  df-ds 14568  df-unif 14569  df-hom 14570  df-cco 14571  df-rest 14669  df-topn 14670  df-0g 14688  df-gsum 14689  df-topgen 14690  df-pt 14691  df-prds 14694  df-xrs 14748  df-qtop 14753  df-imas 14754  df-xps 14756  df-mre 14832  df-mrc 14833  df-acs 14835  df-mnd 15723  df-submnd 15773  df-mulg 15856  df-cntz 16145  df-cmn 16591  df-psmet 18177  df-xmet 18178  df-met 18179  df-bl 18180  df-mopn 18181  df-fbas 18182  df-fg 18183  df-cnfld 18187  df-top 19161  df-bases 19163  df-topon 19164  df-topsp 19165  df-cld 19281  df-ntr 19282  df-cls 19283  df-nei 19360  df-lp 19398  df-perf 19399  df-cn 19489  df-cnp 19490  df-haus 19577  df-tx 19793  df-hmeo 19986  df-fil 20077  df-fm 20169  df-flim 20170  df-flf 20171  df-xms 20553  df-ms 20554  df-tms 20555  df-cncf 21112  df-limc 22000  df-dv 22001
This theorem is referenced by:  atanlogsublem  22969  atanord  22981  basellem4  23080
  Copyright terms: Public domain W3C validator