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