Metamath Proof Explorer

Theorem sincosq4sgn

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

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

Proof

Step Hyp Ref Expression
1 3re 
 |-  3 e. RR
2 halfpire 
 |-  ( _pi / 2 ) e. RR
3 1 2 remulcli 
 |-  ( 3 x. ( _pi / 2 ) ) e. RR
4 3 rexri 
 |-  ( 3 x. ( _pi / 2 ) ) e. RR*
5 2re 
 |-  2 e. RR
6 pire 
 |-  _pi e. RR
7 5 6 remulcli 
 |-  ( 2 x. _pi ) e. RR
8 7 rexri 
 |-  ( 2 x. _pi ) e. RR*
9 elioo2 
 |-  ( ( ( 3 x. ( _pi / 2 ) ) e. RR* /\ ( 2 x. _pi ) e. RR* ) -> ( A e. ( ( 3 x. ( _pi / 2 ) ) (,) ( 2 x. _pi ) ) <-> ( A e. RR /\ ( 3 x. ( _pi / 2 ) ) < A /\ A < ( 2 x. _pi ) ) ) )
10 4 8 9 mp2an 
 |-  ( A e. ( ( 3 x. ( _pi / 2 ) ) (,) ( 2 x. _pi ) ) <-> ( A e. RR /\ ( 3 x. ( _pi / 2 ) ) < A /\ A < ( 2 x. _pi ) ) )
11 df-3 
 |-  3 = ( 2 + 1 )
12 11 oveq1i 
 |-  ( 3 x. ( _pi / 2 ) ) = ( ( 2 + 1 ) x. ( _pi / 2 ) )
13 2cn 
 |-  2 e. CC
14 ax-1cn 
 |-  1 e. CC
15 2 recni 
 |-  ( _pi / 2 ) e. CC
16 13 14 15 adddiri 
 |-  ( ( 2 + 1 ) x. ( _pi / 2 ) ) = ( ( 2 x. ( _pi / 2 ) ) + ( 1 x. ( _pi / 2 ) ) )
17 6 recni 
 |-  _pi e. CC
18 2ne0 
 |-  2 =/= 0
19 17 13 18 divcan2i 
 |-  ( 2 x. ( _pi / 2 ) ) = _pi
20 15 mullidi 
 |-  ( 1 x. ( _pi / 2 ) ) = ( _pi / 2 )
21 19 20 oveq12i 
 |-  ( ( 2 x. ( _pi / 2 ) ) + ( 1 x. ( _pi / 2 ) ) ) = ( _pi + ( _pi / 2 ) )
22 12 16 21 3eqtrri 
 |-  ( _pi + ( _pi / 2 ) ) = ( 3 x. ( _pi / 2 ) )
23 22 breq1i 
 |-  ( ( _pi + ( _pi / 2 ) ) < A <-> ( 3 x. ( _pi / 2 ) ) < A )
24 ltaddsub 
 |-  ( ( _pi e. RR /\ ( _pi / 2 ) e. RR /\ A e. RR ) -> ( ( _pi + ( _pi / 2 ) ) < A <-> _pi < ( A - ( _pi / 2 ) ) ) )
25 6 2 24 mp3an12 
 |-  ( A e. RR -> ( ( _pi + ( _pi / 2 ) ) < A <-> _pi < ( A - ( _pi / 2 ) ) ) )
26 23 25 bitr3id 
 |-  ( A e. RR -> ( ( 3 x. ( _pi / 2 ) ) < A <-> _pi < ( A - ( _pi / 2 ) ) ) )
27 ltsubadd 
 |-  ( ( A e. RR /\ ( _pi / 2 ) e. RR /\ ( 3 x. ( _pi / 2 ) ) e. RR ) -> ( ( A - ( _pi / 2 ) ) < ( 3 x. ( _pi / 2 ) ) <-> A < ( ( 3 x. ( _pi / 2 ) ) + ( _pi / 2 ) ) ) )
28 2 3 27 mp3an23 
 |-  ( A e. RR -> ( ( A - ( _pi / 2 ) ) < ( 3 x. ( _pi / 2 ) ) <-> A < ( ( 3 x. ( _pi / 2 ) ) + ( _pi / 2 ) ) ) )
29 df-4 
 |-  4 = ( 3 + 1 )
30 29 oveq1i 
 |-  ( 4 x. ( _pi / 2 ) ) = ( ( 3 + 1 ) x. ( _pi / 2 ) )
31 1 recni 
 |-  3 e. CC
32 31 14 15 adddiri 
 |-  ( ( 3 + 1 ) x. ( _pi / 2 ) ) = ( ( 3 x. ( _pi / 2 ) ) + ( 1 x. ( _pi / 2 ) ) )
33 20 oveq2i 
 |-  ( ( 3 x. ( _pi / 2 ) ) + ( 1 x. ( _pi / 2 ) ) ) = ( ( 3 x. ( _pi / 2 ) ) + ( _pi / 2 ) )
34 30 32 33 3eqtrri 
 |-  ( ( 3 x. ( _pi / 2 ) ) + ( _pi / 2 ) ) = ( 4 x. ( _pi / 2 ) )
35 4cn 
 |-  4 e. CC
36 2cnne0 
 |-  ( 2 e. CC /\ 2 =/= 0 )
37 div12 
 |-  ( ( 4 e. CC /\ _pi e. CC /\ ( 2 e. CC /\ 2 =/= 0 ) ) -> ( 4 x. ( _pi / 2 ) ) = ( _pi x. ( 4 / 2 ) ) )
38 35 17 36 37 mp3an 
 |-  ( 4 x. ( _pi / 2 ) ) = ( _pi x. ( 4 / 2 ) )
39 4d2e2 
 |-  ( 4 / 2 ) = 2
40 39 oveq2i 
 |-  ( _pi x. ( 4 / 2 ) ) = ( _pi x. 2 )
41 17 13 mulcomi 
 |-  ( _pi x. 2 ) = ( 2 x. _pi )
42 40 41 eqtri 
 |-  ( _pi x. ( 4 / 2 ) ) = ( 2 x. _pi )
43 38 42 eqtri 
 |-  ( 4 x. ( _pi / 2 ) ) = ( 2 x. _pi )
44 34 43 eqtri 
 |-  ( ( 3 x. ( _pi / 2 ) ) + ( _pi / 2 ) ) = ( 2 x. _pi )
45 44 breq2i 
 |-  ( A < ( ( 3 x. ( _pi / 2 ) ) + ( _pi / 2 ) ) <-> A < ( 2 x. _pi ) )
46 28 45 bitr2di 
 |-  ( A e. RR -> ( A < ( 2 x. _pi ) <-> ( A - ( _pi / 2 ) ) < ( 3 x. ( _pi / 2 ) ) ) )
47 26 46 anbi12d 
 |-  ( A e. RR -> ( ( ( 3 x. ( _pi / 2 ) ) < A /\ A < ( 2 x. _pi ) ) <-> ( _pi < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < ( 3 x. ( _pi / 2 ) ) ) ) )
48 resubcl 
 |-  ( ( A e. RR /\ ( _pi / 2 ) e. RR ) -> ( A - ( _pi / 2 ) ) e. RR )
49 2 48 mpan2 
 |-  ( A e. RR -> ( A - ( _pi / 2 ) ) e. RR )
50 6 rexri 
 |-  _pi e. RR*
51 elioo2 
 |-  ( ( _pi e. RR* /\ ( 3 x. ( _pi / 2 ) ) e. RR* ) -> ( ( A - ( _pi / 2 ) ) e. ( _pi (,) ( 3 x. ( _pi / 2 ) ) ) <-> ( ( A - ( _pi / 2 ) ) e. RR /\ _pi < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < ( 3 x. ( _pi / 2 ) ) ) ) )
52 50 4 51 mp2an 
 |-  ( ( A - ( _pi / 2 ) ) e. ( _pi (,) ( 3 x. ( _pi / 2 ) ) ) <-> ( ( A - ( _pi / 2 ) ) e. RR /\ _pi < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < ( 3 x. ( _pi / 2 ) ) ) )
53 sincosq3sgn 
 |-  ( ( A - ( _pi / 2 ) ) e. ( _pi (,) ( 3 x. ( _pi / 2 ) ) ) -> ( ( sin ` ( A - ( _pi / 2 ) ) ) < 0 /\ ( cos ` ( A - ( _pi / 2 ) ) ) < 0 ) )
54 52 53 sylbir 
 |-  ( ( ( A - ( _pi / 2 ) ) e. RR /\ _pi < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < ( 3 x. ( _pi / 2 ) ) ) -> ( ( sin ` ( A - ( _pi / 2 ) ) ) < 0 /\ ( cos ` ( A - ( _pi / 2 ) ) ) < 0 ) )
55 49 54 syl3an1 
 |-  ( ( A e. RR /\ _pi < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < ( 3 x. ( _pi / 2 ) ) ) -> ( ( sin ` ( A - ( _pi / 2 ) ) ) < 0 /\ ( cos ` ( A - ( _pi / 2 ) ) ) < 0 ) )
56 55 3expib 
 |-  ( A e. RR -> ( ( _pi < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < ( 3 x. ( _pi / 2 ) ) ) -> ( ( sin ` ( A - ( _pi / 2 ) ) ) < 0 /\ ( cos ` ( A - ( _pi / 2 ) ) ) < 0 ) ) )
57 47 56 sylbid 
 |-  ( A e. RR -> ( ( ( 3 x. ( _pi / 2 ) ) < A /\ A < ( 2 x. _pi ) ) -> ( ( sin ` ( A - ( _pi / 2 ) ) ) < 0 /\ ( cos ` ( A - ( _pi / 2 ) ) ) < 0 ) ) )
58 49 resincld 
 |-  ( A e. RR -> ( sin ` ( A - ( _pi / 2 ) ) ) e. RR )
59 58 lt0neg1d 
 |-  ( A e. RR -> ( ( sin ` ( A - ( _pi / 2 ) ) ) < 0 <-> 0 < -u ( sin ` ( A - ( _pi / 2 ) ) ) ) )
60 59 anbi1d 
 |-  ( A e. RR -> ( ( ( sin ` ( A - ( _pi / 2 ) ) ) < 0 /\ ( cos ` ( A - ( _pi / 2 ) ) ) < 0 ) <-> ( 0 < -u ( sin ` ( A - ( _pi / 2 ) ) ) /\ ( cos ` ( A - ( _pi / 2 ) ) ) < 0 ) ) )
61 57 60 sylibd 
 |-  ( A e. RR -> ( ( ( 3 x. ( _pi / 2 ) ) < A /\ A < ( 2 x. _pi ) ) -> ( 0 < -u ( sin ` ( A - ( _pi / 2 ) ) ) /\ ( cos ` ( A - ( _pi / 2 ) ) ) < 0 ) ) )
62 recn 
 |-  ( A e. RR -> A e. CC )
63 pncan3 
 |-  ( ( ( _pi / 2 ) e. CC /\ A e. CC ) -> ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) = A )
64 15 62 63 sylancr 
 |-  ( A e. RR -> ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) = A )
65 64 fveq2d 
 |-  ( A e. RR -> ( cos ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = ( cos ` A ) )
66 49 recnd 
 |-  ( A e. RR -> ( A - ( _pi / 2 ) ) e. CC )
67 coshalfpip 
 |-  ( ( A - ( _pi / 2 ) ) e. CC -> ( cos ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = -u ( sin ` ( A - ( _pi / 2 ) ) ) )
68 66 67 syl 
 |-  ( A e. RR -> ( cos ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = -u ( sin ` ( A - ( _pi / 2 ) ) ) )
69 65 68 eqtr3d 
 |-  ( A e. RR -> ( cos ` A ) = -u ( sin ` ( A - ( _pi / 2 ) ) ) )
70 69 breq2d 
 |-  ( A e. RR -> ( 0 < ( cos ` A ) <-> 0 < -u ( sin ` ( A - ( _pi / 2 ) ) ) ) )
71 64 fveq2d 
 |-  ( A e. RR -> ( sin ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = ( sin ` A ) )
72 sinhalfpip 
 |-  ( ( A - ( _pi / 2 ) ) e. CC -> ( sin ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = ( cos ` ( A - ( _pi / 2 ) ) ) )
73 66 72 syl 
 |-  ( A e. RR -> ( sin ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = ( cos ` ( A - ( _pi / 2 ) ) ) )
74 71 73 eqtr3d 
 |-  ( A e. RR -> ( sin ` A ) = ( cos ` ( A - ( _pi / 2 ) ) ) )
75 74 breq1d 
 |-  ( A e. RR -> ( ( sin ` A ) < 0 <-> ( cos ` ( A - ( _pi / 2 ) ) ) < 0 ) )
76 70 75 anbi12d 
 |-  ( A e. RR -> ( ( 0 < ( cos ` A ) /\ ( sin ` A ) < 0 ) <-> ( 0 < -u ( sin ` ( A - ( _pi / 2 ) ) ) /\ ( cos ` ( A - ( _pi / 2 ) ) ) < 0 ) ) )
77 61 76 sylibrd 
 |-  ( A e. RR -> ( ( ( 3 x. ( _pi / 2 ) ) < A /\ A < ( 2 x. _pi ) ) -> ( 0 < ( cos ` A ) /\ ( sin ` A ) < 0 ) ) )
78 77 3impib 
 |-  ( ( A e. RR /\ ( 3 x. ( _pi / 2 ) ) < A /\ A < ( 2 x. _pi ) ) -> ( 0 < ( cos ` A ) /\ ( sin ` A ) < 0 ) )
79 78 ancomd 
 |-  ( ( A e. RR /\ ( 3 x. ( _pi / 2 ) ) < A /\ A < ( 2 x. _pi ) ) -> ( ( sin ` A ) < 0 /\ 0 < ( cos ` A ) ) )
80 10 79 sylbi 
 |-  ( A e. ( ( 3 x. ( _pi / 2 ) ) (,) ( 2 x. _pi ) ) -> ( ( sin ` A ) < 0 /\ 0 < ( cos ` A ) ) )