Metamath Proof Explorer

Theorem sincosq3sgn

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

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

Proof

Step Hyp Ref Expression
1 pire 
 |-  _pi e. RR
2 3re 
 |-  3 e. RR
3 halfpire 
 |-  ( _pi / 2 ) e. RR
4 2 3 remulcli 
 |-  ( 3 x. ( _pi / 2 ) ) e. RR
5 rexr 
 |-  ( _pi e. RR -> _pi e. RR* )
6 rexr 
 |-  ( ( 3 x. ( _pi / 2 ) ) e. RR -> ( 3 x. ( _pi / 2 ) ) e. RR* )
7 elioo2 
 |-  ( ( _pi e. RR* /\ ( 3 x. ( _pi / 2 ) ) e. RR* ) -> ( A e. ( _pi (,) ( 3 x. ( _pi / 2 ) ) ) <-> ( A e. RR /\ _pi < A /\ A < ( 3 x. ( _pi / 2 ) ) ) ) )
8 5 6 7 syl2an 
 |-  ( ( _pi e. RR /\ ( 3 x. ( _pi / 2 ) ) e. RR ) -> ( A e. ( _pi (,) ( 3 x. ( _pi / 2 ) ) ) <-> ( A e. RR /\ _pi < A /\ A < ( 3 x. ( _pi / 2 ) ) ) ) )
9 1 4 8 mp2an 
 |-  ( A e. ( _pi (,) ( 3 x. ( _pi / 2 ) ) ) <-> ( A e. RR /\ _pi < A /\ A < ( 3 x. ( _pi / 2 ) ) ) )
10 pidiv2halves 
 |-  ( ( _pi / 2 ) + ( _pi / 2 ) ) = _pi
11 10 breq1i 
 |-  ( ( ( _pi / 2 ) + ( _pi / 2 ) ) < A <-> _pi < A )
12 ltaddsub 
 |-  ( ( ( _pi / 2 ) e. RR /\ ( _pi / 2 ) e. RR /\ A e. RR ) -> ( ( ( _pi / 2 ) + ( _pi / 2 ) ) < A <-> ( _pi / 2 ) < ( A - ( _pi / 2 ) ) ) )
13 3 3 12 mp3an12 
 |-  ( A e. RR -> ( ( ( _pi / 2 ) + ( _pi / 2 ) ) < A <-> ( _pi / 2 ) < ( A - ( _pi / 2 ) ) ) )
14 11 13 bitr3id 
 |-  ( A e. RR -> ( _pi < A <-> ( _pi / 2 ) < ( A - ( _pi / 2 ) ) ) )
15 ltsubadd 
 |-  ( ( A e. RR /\ ( _pi / 2 ) e. RR /\ _pi e. RR ) -> ( ( A - ( _pi / 2 ) ) < _pi <-> A < ( _pi + ( _pi / 2 ) ) ) )
16 3 1 15 mp3an23 
 |-  ( A e. RR -> ( ( A - ( _pi / 2 ) ) < _pi <-> A < ( _pi + ( _pi / 2 ) ) ) )
17 df-3 
 |-  3 = ( 2 + 1 )
18 17 oveq1i 
 |-  ( 3 x. ( _pi / 2 ) ) = ( ( 2 + 1 ) x. ( _pi / 2 ) )
19 2cn 
 |-  2 e. CC
20 ax-1cn 
 |-  1 e. CC
21 3 recni 
 |-  ( _pi / 2 ) e. CC
22 19 20 21 adddiri 
 |-  ( ( 2 + 1 ) x. ( _pi / 2 ) ) = ( ( 2 x. ( _pi / 2 ) ) + ( 1 x. ( _pi / 2 ) ) )
23 1 recni 
 |-  _pi e. CC
24 2ne0 
 |-  2 =/= 0
25 23 19 24 divcan2i 
 |-  ( 2 x. ( _pi / 2 ) ) = _pi
26 21 mullidi 
 |-  ( 1 x. ( _pi / 2 ) ) = ( _pi / 2 )
27 25 26 oveq12i 
 |-  ( ( 2 x. ( _pi / 2 ) ) + ( 1 x. ( _pi / 2 ) ) ) = ( _pi + ( _pi / 2 ) )
28 18 22 27 3eqtrri 
 |-  ( _pi + ( _pi / 2 ) ) = ( 3 x. ( _pi / 2 ) )
29 28 breq2i 
 |-  ( A < ( _pi + ( _pi / 2 ) ) <-> A < ( 3 x. ( _pi / 2 ) ) )
30 16 29 bitr2di 
 |-  ( A e. RR -> ( A < ( 3 x. ( _pi / 2 ) ) <-> ( A - ( _pi / 2 ) ) < _pi ) )
31 14 30 anbi12d 
 |-  ( A e. RR -> ( ( _pi < A /\ A < ( 3 x. ( _pi / 2 ) ) ) <-> ( ( _pi / 2 ) < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < _pi ) ) )
32 resubcl 
 |-  ( ( A e. RR /\ ( _pi / 2 ) e. RR ) -> ( A - ( _pi / 2 ) ) e. RR )
33 3 32 mpan2 
 |-  ( A e. RR -> ( A - ( _pi / 2 ) ) e. RR )
34 sincosq2sgn 
 |-  ( ( A - ( _pi / 2 ) ) e. ( ( _pi / 2 ) (,) _pi ) -> ( 0 < ( sin ` ( A - ( _pi / 2 ) ) ) /\ ( cos ` ( A - ( _pi / 2 ) ) ) < 0 ) )
35 rexr 
 |-  ( ( _pi / 2 ) e. RR -> ( _pi / 2 ) e. RR* )
36 elioo2 
 |-  ( ( ( _pi / 2 ) e. RR* /\ _pi e. RR* ) -> ( ( A - ( _pi / 2 ) ) e. ( ( _pi / 2 ) (,) _pi ) <-> ( ( A - ( _pi / 2 ) ) e. RR /\ ( _pi / 2 ) < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < _pi ) ) )
37 35 5 36 syl2an 
 |-  ( ( ( _pi / 2 ) e. RR /\ _pi e. RR ) -> ( ( A - ( _pi / 2 ) ) e. ( ( _pi / 2 ) (,) _pi ) <-> ( ( A - ( _pi / 2 ) ) e. RR /\ ( _pi / 2 ) < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < _pi ) ) )
38 3 1 37 mp2an 
 |-  ( ( A - ( _pi / 2 ) ) e. ( ( _pi / 2 ) (,) _pi ) <-> ( ( A - ( _pi / 2 ) ) e. RR /\ ( _pi / 2 ) < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < _pi ) )
39 ancom 
 |-  ( ( 0 < ( sin ` ( A - ( _pi / 2 ) ) ) /\ ( cos ` ( A - ( _pi / 2 ) ) ) < 0 ) <-> ( ( cos ` ( A - ( _pi / 2 ) ) ) < 0 /\ 0 < ( sin ` ( A - ( _pi / 2 ) ) ) ) )
40 34 38 39 3imtr3i 
 |-  ( ( ( A - ( _pi / 2 ) ) e. RR /\ ( _pi / 2 ) < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < _pi ) -> ( ( cos ` ( A - ( _pi / 2 ) ) ) < 0 /\ 0 < ( sin ` ( A - ( _pi / 2 ) ) ) ) )
41 33 40 syl3an1 
 |-  ( ( A e. RR /\ ( _pi / 2 ) < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < _pi ) -> ( ( cos ` ( A - ( _pi / 2 ) ) ) < 0 /\ 0 < ( sin ` ( A - ( _pi / 2 ) ) ) ) )
42 41 3expib 
 |-  ( A e. RR -> ( ( ( _pi / 2 ) < ( A - ( _pi / 2 ) ) /\ ( A - ( _pi / 2 ) ) < _pi ) -> ( ( cos ` ( A - ( _pi / 2 ) ) ) < 0 /\ 0 < ( sin ` ( A - ( _pi / 2 ) ) ) ) ) )
43 31 42 sylbid 
 |-  ( A e. RR -> ( ( _pi < A /\ A < ( 3 x. ( _pi / 2 ) ) ) -> ( ( cos ` ( A - ( _pi / 2 ) ) ) < 0 /\ 0 < ( sin ` ( A - ( _pi / 2 ) ) ) ) ) )
44 33 resincld 
 |-  ( A e. RR -> ( sin ` ( A - ( _pi / 2 ) ) ) e. RR )
45 44 lt0neg2d 
 |-  ( A e. RR -> ( 0 < ( sin ` ( A - ( _pi / 2 ) ) ) <-> -u ( sin ` ( A - ( _pi / 2 ) ) ) < 0 ) )
46 45 anbi2d 
 |-  ( A e. RR -> ( ( ( cos ` ( A - ( _pi / 2 ) ) ) < 0 /\ 0 < ( sin ` ( A - ( _pi / 2 ) ) ) ) <-> ( ( cos ` ( A - ( _pi / 2 ) ) ) < 0 /\ -u ( sin ` ( A - ( _pi / 2 ) ) ) < 0 ) ) )
47 43 46 sylibd 
 |-  ( A e. RR -> ( ( _pi < A /\ A < ( 3 x. ( _pi / 2 ) ) ) -> ( ( cos ` ( A - ( _pi / 2 ) ) ) < 0 /\ -u ( sin ` ( A - ( _pi / 2 ) ) ) < 0 ) ) )
48 recn 
 |-  ( A e. RR -> A e. CC )
49 pncan3 
 |-  ( ( ( _pi / 2 ) e. CC /\ A e. CC ) -> ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) = A )
50 21 48 49 sylancr 
 |-  ( A e. RR -> ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) = A )
51 50 fveq2d 
 |-  ( A e. RR -> ( sin ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = ( sin ` A ) )
52 33 recnd 
 |-  ( A e. RR -> ( A - ( _pi / 2 ) ) e. CC )
53 sinhalfpip 
 |-  ( ( A - ( _pi / 2 ) ) e. CC -> ( sin ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = ( cos ` ( A - ( _pi / 2 ) ) ) )
54 52 53 syl 
 |-  ( A e. RR -> ( sin ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = ( cos ` ( A - ( _pi / 2 ) ) ) )
55 51 54 eqtr3d 
 |-  ( A e. RR -> ( sin ` A ) = ( cos ` ( A - ( _pi / 2 ) ) ) )
56 55 breq1d 
 |-  ( A e. RR -> ( ( sin ` A ) < 0 <-> ( cos ` ( A - ( _pi / 2 ) ) ) < 0 ) )
57 50 fveq2d 
 |-  ( A e. RR -> ( cos ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = ( cos ` A ) )
58 coshalfpip 
 |-  ( ( A - ( _pi / 2 ) ) e. CC -> ( cos ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = -u ( sin ` ( A - ( _pi / 2 ) ) ) )
59 52 58 syl 
 |-  ( A e. RR -> ( cos ` ( ( _pi / 2 ) + ( A - ( _pi / 2 ) ) ) ) = -u ( sin ` ( A - ( _pi / 2 ) ) ) )
60 57 59 eqtr3d 
 |-  ( A e. RR -> ( cos ` A ) = -u ( sin ` ( A - ( _pi / 2 ) ) ) )
61 60 breq1d 
 |-  ( A e. RR -> ( ( cos ` A ) < 0 <-> -u ( sin ` ( A - ( _pi / 2 ) ) ) < 0 ) )
62 56 61 anbi12d 
 |-  ( A e. RR -> ( ( ( sin ` A ) < 0 /\ ( cos ` A ) < 0 ) <-> ( ( cos ` ( A - ( _pi / 2 ) ) ) < 0 /\ -u ( sin ` ( A - ( _pi / 2 ) ) ) < 0 ) ) )
63 47 62 sylibrd 
 |-  ( A e. RR -> ( ( _pi < A /\ A < ( 3 x. ( _pi / 2 ) ) ) -> ( ( sin ` A ) < 0 /\ ( cos ` A ) < 0 ) ) )
64 63 3impib 
 |-  ( ( A e. RR /\ _pi < A /\ A < ( 3 x. ( _pi / 2 ) ) ) -> ( ( sin ` A ) < 0 /\ ( cos ` A ) < 0 ) )
65 9 64 sylbi 
 |-  ( A e. ( _pi (,) ( 3 x. ( _pi / 2 ) ) ) -> ( ( sin ` A ) < 0 /\ ( cos ` A ) < 0 ) )