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