Metamath Proof Explorer

Theorem sincosq2sgn

Description: The signs of the sine and cosine functions in the second quadrant. (Contributed by Paul Chapman, 24-Jan-2008)

Ref Expression
Assertion sincosq2sgn 
|- ( A e. ( ( _pi / 2 ) (,) _pi ) -> ( 0 < ( sin ` A ) /\ ( cos ` A ) < 0 ) )

Proof

Step Hyp Ref Expression
1 halfpire 
 |-  ( _pi / 2 ) e. RR
2 pire 
 |-  _pi e. RR
3 rexr 
 |-  ( ( _pi / 2 ) e. RR -> ( _pi / 2 ) e. RR* )
4 rexr 
 |-  ( _pi e. RR -> _pi e. RR* )
5 elioo2 
 |-  ( ( ( _pi / 2 ) e. RR* /\ _pi e. RR* ) -> ( A e. ( ( _pi / 2 ) (,) _pi ) <-> ( A e. RR /\ ( _pi / 2 ) < A /\ A < _pi ) ) )
6 3 4 5 syl2an 
 |-  ( ( ( _pi / 2 ) e. RR /\ _pi e. RR ) -> ( A e. ( ( _pi / 2 ) (,) _pi ) <-> ( A e. RR /\ ( _pi / 2 ) < A /\ A < _pi ) ) )
7 1 2 6 mp2an 
 |-  ( A e. ( ( _pi / 2 ) (,) _pi ) <-> ( A e. RR /\ ( _pi / 2 ) < A /\ A < _pi ) )
8 resubcl 
 |-  ( ( A e. RR /\ ( _pi / 2 ) e. RR ) -> ( A - ( _pi / 2 ) ) e. RR )
9 1 8 mpan2 
 |-  ( A e. RR -> ( A - ( _pi / 2 ) ) e. RR )
10 0xr 
 |-  0 e. RR*
11 1 rexri 
 |-  ( _pi / 2 ) e. RR*
12 elioo2 
 |-  ( ( 0 e. RR* /\ ( _pi / 2 ) e. RR* ) -> ( ( A - ( _pi / 2 ) ) e. ( 0 (,) ( _pi / 2 ) ) <-> ( ( A - ( _pi / 2 ) ) e. RR /\ 0 < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < ( _pi / 2 ) ) ) )
13 10 11 12 mp2an 
 |-  ( ( A - ( _pi / 2 ) ) e. ( 0 (,) ( _pi / 2 ) ) <-> ( ( A - ( _pi / 2 ) ) e. RR /\ 0 < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < ( _pi / 2 ) ) )
14 sincosq1sgn 
 |-  ( ( A - ( _pi / 2 ) ) e. ( 0 (,) ( _pi / 2 ) ) -> ( 0 < ( sin ` ( A - ( _pi / 2 ) ) ) /\ 0 < ( cos ` ( A - ( _pi / 2 ) ) ) ) )
15 13 14 sylbir 
 |-  ( ( ( A - ( _pi / 2 ) ) e. RR /\ 0 < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < ( _pi / 2 ) ) -> ( 0 < ( sin ` ( A - ( _pi / 2 ) ) ) /\ 0 < ( cos ` ( A - ( _pi / 2 ) ) ) ) )
16 9 15 syl3an1 
 |-  ( ( A e. RR /\ 0 < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < ( _pi / 2 ) ) -> ( 0 < ( sin ` ( A - ( _pi / 2 ) ) ) /\ 0 < ( cos ` ( A - ( _pi / 2 ) ) ) ) )
17 16 3expib 
 |-  ( A e. RR -> ( ( 0 < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < ( _pi / 2 ) ) -> ( 0 < ( sin ` ( A - ( _pi / 2 ) ) ) /\ 0 < ( cos ` ( A - ( _pi / 2 ) ) ) ) ) )
18 0re 
 |-  0 e. RR
19 ltsub13 
 |-  ( ( 0 e. RR /\ A e. RR /\ ( _pi / 2 ) e. RR ) -> ( 0 < ( A - ( _pi / 2 ) ) <-> ( _pi / 2 ) < ( A - 0 ) ) )
20 18 1 19 mp3an13 
 |-  ( A e. RR -> ( 0 < ( A - ( _pi / 2 ) ) <-> ( _pi / 2 ) < ( A - 0 ) ) )
21 recn 
 |-  ( A e. RR -> A e. CC )
22 21 subid1d 
 |-  ( A e. RR -> ( A - 0 ) = A )
23 22 breq2d 
 |-  ( A e. RR -> ( ( _pi / 2 ) < ( A - 0 ) <-> ( _pi / 2 ) < A ) )
24 20 23 bitrd 
 |-  ( A e. RR -> ( 0 < ( A - ( _pi / 2 ) ) <-> ( _pi / 2 ) < A ) )
25 ltsubadd 
 |-  ( ( A e. RR /\ ( _pi / 2 ) e. RR /\ ( _pi / 2 ) e. RR ) -> ( ( A - ( _pi / 2 ) ) < ( _pi / 2 ) <-> A < ( ( _pi / 2 ) + ( _pi / 2 ) ) ) )
26 1 1 25 mp3an23 
 |-  ( A e. RR -> ( ( A - ( _pi / 2 ) ) < ( _pi / 2 ) <-> A < ( ( _pi / 2 ) + ( _pi / 2 ) ) ) )
27 pidiv2halves 
 |-  ( ( _pi / 2 ) + ( _pi / 2 ) ) = _pi
28 27 breq2i 
 |-  ( A < ( ( _pi / 2 ) + ( _pi / 2 ) ) <-> A < _pi )
29 26 28 syl6bb 
 |-  ( A e. RR -> ( ( A - ( _pi / 2 ) ) < ( _pi / 2 ) <-> A < _pi ) )
30 24 29 anbi12d 
 |-  ( A e. RR -> ( ( 0 < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < ( _pi / 2 ) ) <-> ( ( _pi / 2 ) < A /\ A < _pi ) ) )
31 9 resincld 
 |-  ( A e. RR -> ( sin ` ( A - ( _pi / 2 ) ) ) e. RR )
32 31 lt0neg2d 
 |-  ( A e. RR -> ( 0 < ( sin ` ( A - ( _pi / 2 ) ) ) <-> -u ( sin ` ( A - ( _pi / 2 ) ) ) < 0 ) )
33 32 anbi1d 
 |-  ( A e. RR -> ( ( 0 < ( sin ` ( A - ( _pi / 2 ) ) ) /\ 0 < ( cos ` ( A - ( _pi / 2 ) ) ) ) <-> ( -u ( sin ` ( A - ( _pi / 2 ) ) ) < 0 /\ 0 < ( cos ` ( A - ( _pi / 2 ) ) ) ) ) )
34 17 30 33 3imtr3d 
 |-  ( A e. RR -> ( ( ( _pi / 2 ) < A /\ A < _pi ) -> ( -u ( sin ` ( A - ( _pi / 2 ) ) ) < 0 /\ 0 < ( cos ` ( A - ( _pi / 2 ) ) ) ) ) )
35 1 recni 
 |-  ( _pi / 2 ) e. CC
36 pncan3 
 |-  ( ( ( _pi / 2 ) e. CC /\ A e. CC ) -> ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) = A )
37 35 21 36 sylancr 
 |-  ( A e. RR -> ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) = A )
38 37 fveq2d 
 |-  ( A e. RR -> ( cos ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = ( cos ` A ) )
39 9 recnd 
 |-  ( A e. RR -> ( A - ( _pi / 2 ) ) e. CC )
40 coshalfpip 
 |-  ( ( A - ( _pi / 2 ) ) e. CC -> ( cos ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = -u ( sin ` ( A - ( _pi / 2 ) ) ) )
41 39 40 syl 
 |-  ( A e. RR -> ( cos ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = -u ( sin ` ( A - ( _pi / 2 ) ) ) )
42 38 41 eqtr3d 
 |-  ( A e. RR -> ( cos ` A ) = -u ( sin ` ( A - ( _pi / 2 ) ) ) )
43 42 breq1d 
 |-  ( A e. RR -> ( ( cos ` A ) < 0 <-> -u ( sin ` ( A - ( _pi / 2 ) ) ) < 0 ) )
44 37 fveq2d 
 |-  ( A e. RR -> ( sin ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = ( sin ` A ) )
45 sinhalfpip 
 |-  ( ( A - ( _pi / 2 ) ) e. CC -> ( sin ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = ( cos ` ( A - ( _pi / 2 ) ) ) )
46 39 45 syl 
 |-  ( A e. RR -> ( sin ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = ( cos ` ( A - ( _pi / 2 ) ) ) )
47 44 46 eqtr3d 
 |-  ( A e. RR -> ( sin ` A ) = ( cos ` ( A - ( _pi / 2 ) ) ) )
48 47 breq2d 
 |-  ( A e. RR -> ( 0 < ( sin ` A ) <-> 0 < ( cos ` ( A - ( _pi / 2 ) ) ) ) )
49 43 48 anbi12d 
 |-  ( A e. RR -> ( ( ( cos ` A ) < 0 /\ 0 < ( sin ` A ) ) <-> ( -u ( sin ` ( A - ( _pi / 2 ) ) ) < 0 /\ 0 < ( cos ` ( A - ( _pi / 2 ) ) ) ) ) )
50 34 49 sylibrd 
 |-  ( A e. RR -> ( ( ( _pi / 2 ) < A /\ A < _pi ) -> ( ( cos ` A ) < 0 /\ 0 < ( sin ` A ) ) ) )
51 50 3impib 
 |-  ( ( A e. RR /\ ( _pi / 2 ) < A /\ A < _pi ) -> ( ( cos ` A ) < 0 /\ 0 < ( sin ` A ) ) )
52 51 ancomd 
 |-  ( ( A e. RR /\ ( _pi / 2 ) < A /\ A < _pi ) -> ( 0 < ( sin ` A ) /\ ( cos ` A ) < 0 ) )
53 7 52 sylbi 
 |-  ( A e. ( ( _pi / 2 ) (,) _pi ) -> ( 0 < ( sin ` A ) /\ ( cos ` A ) < 0 ) )