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 3 π 2 2 π sin A < 0 0 < cos A

Proof

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