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⁢π22⁢π→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⁢π22⁢π↔A∈ℝ∧3⁢π2<A∧A<2⁢π
10 4 8 9 mp2an ⊢A∈3⁢π22⁢π↔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 mullidi ⊢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=π⁢42
38 35 17 36 37 mp3an ⊢4⁢π2=π⁢42
39 4d2e2 ⊢42=2
40 39 oveq2i ⊢π⁢42=π⋅2
41 17 13 mulcomi ⊢π⋅2=2⁢π
42 40 41 eqtri ⊢π⁢42=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⁢π22⁢π→sin⁡A<0∧0<cos⁡A