# Metamath Proof Explorer

## Theorem sincosq2sgn

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

Ref Expression
Assertion sincosq2sgn ${⊢}{A}\in \left(\frac{\mathrm{\pi }}{2},\mathrm{\pi }\right)\to \left(0<\mathrm{sin}{A}\wedge \mathrm{cos}{A}<0\right)$

### Proof

Step Hyp Ref Expression
1 halfpire ${⊢}\frac{\mathrm{\pi }}{2}\in ℝ$
2 pire ${⊢}\mathrm{\pi }\in ℝ$
3 rexr ${⊢}\frac{\mathrm{\pi }}{2}\in ℝ\to \frac{\mathrm{\pi }}{2}\in {ℝ}^{*}$
4 rexr ${⊢}\mathrm{\pi }\in ℝ\to \mathrm{\pi }\in {ℝ}^{*}$
5 elioo2 ${⊢}\left(\frac{\mathrm{\pi }}{2}\in {ℝ}^{*}\wedge \mathrm{\pi }\in {ℝ}^{*}\right)\to \left({A}\in \left(\frac{\mathrm{\pi }}{2},\mathrm{\pi }\right)↔\left({A}\in ℝ\wedge \frac{\mathrm{\pi }}{2}<{A}\wedge {A}<\mathrm{\pi }\right)\right)$
6 3 4 5 syl2an ${⊢}\left(\frac{\mathrm{\pi }}{2}\in ℝ\wedge \mathrm{\pi }\in ℝ\right)\to \left({A}\in \left(\frac{\mathrm{\pi }}{2},\mathrm{\pi }\right)↔\left({A}\in ℝ\wedge \frac{\mathrm{\pi }}{2}<{A}\wedge {A}<\mathrm{\pi }\right)\right)$
7 1 2 6 mp2an ${⊢}{A}\in \left(\frac{\mathrm{\pi }}{2},\mathrm{\pi }\right)↔\left({A}\in ℝ\wedge \frac{\mathrm{\pi }}{2}<{A}\wedge {A}<\mathrm{\pi }\right)$
8 resubcl ${⊢}\left({A}\in ℝ\wedge \frac{\mathrm{\pi }}{2}\in ℝ\right)\to {A}-\left(\frac{\mathrm{\pi }}{2}\right)\in ℝ$
9 1 8 mpan2 ${⊢}{A}\in ℝ\to {A}-\left(\frac{\mathrm{\pi }}{2}\right)\in ℝ$
10 0xr ${⊢}0\in {ℝ}^{*}$
11 1 rexri ${⊢}\frac{\mathrm{\pi }}{2}\in {ℝ}^{*}$
12 elioo2 ${⊢}\left(0\in {ℝ}^{*}\wedge \frac{\mathrm{\pi }}{2}\in {ℝ}^{*}\right)\to \left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\in \left(0,\frac{\mathrm{\pi }}{2}\right)↔\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\in ℝ\wedge 0<{A}-\left(\frac{\mathrm{\pi }}{2}\right)\wedge {A}-\left(\frac{\mathrm{\pi }}{2}\right)<\frac{\mathrm{\pi }}{2}\right)\right)$
13 10 11 12 mp2an ${⊢}{A}-\left(\frac{\mathrm{\pi }}{2}\right)\in \left(0,\frac{\mathrm{\pi }}{2}\right)↔\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\in ℝ\wedge 0<{A}-\left(\frac{\mathrm{\pi }}{2}\right)\wedge {A}-\left(\frac{\mathrm{\pi }}{2}\right)<\frac{\mathrm{\pi }}{2}\right)$
14 sincosq1sgn ${⊢}{A}-\left(\frac{\mathrm{\pi }}{2}\right)\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(0<\mathrm{sin}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)\wedge 0<\mathrm{cos}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)\right)$
15 13 14 sylbir ${⊢}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\in ℝ\wedge 0<{A}-\left(\frac{\mathrm{\pi }}{2}\right)\wedge {A}-\left(\frac{\mathrm{\pi }}{2}\right)<\frac{\mathrm{\pi }}{2}\right)\to \left(0<\mathrm{sin}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)\wedge 0<\mathrm{cos}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)\right)$
16 9 15 syl3an1 ${⊢}\left({A}\in ℝ\wedge 0<{A}-\left(\frac{\mathrm{\pi }}{2}\right)\wedge {A}-\left(\frac{\mathrm{\pi }}{2}\right)<\frac{\mathrm{\pi }}{2}\right)\to \left(0<\mathrm{sin}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)\wedge 0<\mathrm{cos}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)\right)$
17 16 3expib ${⊢}{A}\in ℝ\to \left(\left(0<{A}-\left(\frac{\mathrm{\pi }}{2}\right)\wedge {A}-\left(\frac{\mathrm{\pi }}{2}\right)<\frac{\mathrm{\pi }}{2}\right)\to \left(0<\mathrm{sin}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)\wedge 0<\mathrm{cos}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)\right)\right)$
18 0re ${⊢}0\in ℝ$
19 ltsub13 ${⊢}\left(0\in ℝ\wedge {A}\in ℝ\wedge \frac{\mathrm{\pi }}{2}\in ℝ\right)\to \left(0<{A}-\left(\frac{\mathrm{\pi }}{2}\right)↔\frac{\mathrm{\pi }}{2}<{A}-0\right)$
20 18 1 19 mp3an13 ${⊢}{A}\in ℝ\to \left(0<{A}-\left(\frac{\mathrm{\pi }}{2}\right)↔\frac{\mathrm{\pi }}{2}<{A}-0\right)$
21 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
22 21 subid1d ${⊢}{A}\in ℝ\to {A}-0={A}$
23 22 breq2d ${⊢}{A}\in ℝ\to \left(\frac{\mathrm{\pi }}{2}<{A}-0↔\frac{\mathrm{\pi }}{2}<{A}\right)$
24 20 23 bitrd ${⊢}{A}\in ℝ\to \left(0<{A}-\left(\frac{\mathrm{\pi }}{2}\right)↔\frac{\mathrm{\pi }}{2}<{A}\right)$
25 ltsubadd ${⊢}\left({A}\in ℝ\wedge \frac{\mathrm{\pi }}{2}\in ℝ\wedge \frac{\mathrm{\pi }}{2}\in ℝ\right)\to \left({A}-\left(\frac{\mathrm{\pi }}{2}\right)<\frac{\mathrm{\pi }}{2}↔{A}<\left(\frac{\mathrm{\pi }}{2}\right)+\left(\frac{\mathrm{\pi }}{2}\right)\right)$
26 1 1 25 mp3an23 ${⊢}{A}\in ℝ\to \left({A}-\left(\frac{\mathrm{\pi }}{2}\right)<\frac{\mathrm{\pi }}{2}↔{A}<\left(\frac{\mathrm{\pi }}{2}\right)+\left(\frac{\mathrm{\pi }}{2}\right)\right)$
27 pidiv2halves ${⊢}\left(\frac{\mathrm{\pi }}{2}\right)+\left(\frac{\mathrm{\pi }}{2}\right)=\mathrm{\pi }$
28 27 breq2i ${⊢}{A}<\left(\frac{\mathrm{\pi }}{2}\right)+\left(\frac{\mathrm{\pi }}{2}\right)↔{A}<\mathrm{\pi }$
29 26 28 syl6bb ${⊢}{A}\in ℝ\to \left({A}-\left(\frac{\mathrm{\pi }}{2}\right)<\frac{\mathrm{\pi }}{2}↔{A}<\mathrm{\pi }\right)$
30 24 29 anbi12d ${⊢}{A}\in ℝ\to \left(\left(0<{A}-\left(\frac{\mathrm{\pi }}{2}\right)\wedge {A}-\left(\frac{\mathrm{\pi }}{2}\right)<\frac{\mathrm{\pi }}{2}\right)↔\left(\frac{\mathrm{\pi }}{2}<{A}\wedge {A}<\mathrm{\pi }\right)\right)$
31 9 resincld ${⊢}{A}\in ℝ\to \mathrm{sin}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)\in ℝ$
32 31 lt0neg2d ${⊢}{A}\in ℝ\to \left(0<\mathrm{sin}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)↔-\mathrm{sin}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)<0\right)$
33 32 anbi1d ${⊢}{A}\in ℝ\to \left(\left(0<\mathrm{sin}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)\wedge 0<\mathrm{cos}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)\right)↔\left(-\mathrm{sin}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)<0\wedge 0<\mathrm{cos}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)\right)\right)$
34 17 30 33 3imtr3d ${⊢}{A}\in ℝ\to \left(\left(\frac{\mathrm{\pi }}{2}<{A}\wedge {A}<\mathrm{\pi }\right)\to \left(-\mathrm{sin}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)<0\wedge 0<\mathrm{cos}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)\right)\right)$
35 1 recni ${⊢}\frac{\mathrm{\pi }}{2}\in ℂ$
36 pncan3 ${⊢}\left(\frac{\mathrm{\pi }}{2}\in ℂ\wedge {A}\in ℂ\right)\to \left(\frac{\mathrm{\pi }}{2}\right)+{A}-\left(\frac{\mathrm{\pi }}{2}\right)={A}$
37 35 21 36 sylancr ${⊢}{A}\in ℝ\to \left(\frac{\mathrm{\pi }}{2}\right)+{A}-\left(\frac{\mathrm{\pi }}{2}\right)={A}$
38 37 fveq2d ${⊢}{A}\in ℝ\to \mathrm{cos}\left(\left(\frac{\mathrm{\pi }}{2}\right)+{A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)=\mathrm{cos}{A}$
39 9 recnd ${⊢}{A}\in ℝ\to {A}-\left(\frac{\mathrm{\pi }}{2}\right)\in ℂ$
40 coshalfpip ${⊢}{A}-\left(\frac{\mathrm{\pi }}{2}\right)\in ℂ\to \mathrm{cos}\left(\left(\frac{\mathrm{\pi }}{2}\right)+{A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)=-\mathrm{sin}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)$
41 39 40 syl ${⊢}{A}\in ℝ\to \mathrm{cos}\left(\left(\frac{\mathrm{\pi }}{2}\right)+{A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)=-\mathrm{sin}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)$
42 38 41 eqtr3d ${⊢}{A}\in ℝ\to \mathrm{cos}{A}=-\mathrm{sin}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)$
43 42 breq1d ${⊢}{A}\in ℝ\to \left(\mathrm{cos}{A}<0↔-\mathrm{sin}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)<0\right)$
44 37 fveq2d ${⊢}{A}\in ℝ\to \mathrm{sin}\left(\left(\frac{\mathrm{\pi }}{2}\right)+{A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)=\mathrm{sin}{A}$
45 sinhalfpip ${⊢}{A}-\left(\frac{\mathrm{\pi }}{2}\right)\in ℂ\to \mathrm{sin}\left(\left(\frac{\mathrm{\pi }}{2}\right)+{A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)=\mathrm{cos}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)$
46 39 45 syl ${⊢}{A}\in ℝ\to \mathrm{sin}\left(\left(\frac{\mathrm{\pi }}{2}\right)+{A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)=\mathrm{cos}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)$
47 44 46 eqtr3d ${⊢}{A}\in ℝ\to \mathrm{sin}{A}=\mathrm{cos}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)$
48 47 breq2d ${⊢}{A}\in ℝ\to \left(0<\mathrm{sin}{A}↔0<\mathrm{cos}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)\right)$
49 43 48 anbi12d ${⊢}{A}\in ℝ\to \left(\left(\mathrm{cos}{A}<0\wedge 0<\mathrm{sin}{A}\right)↔\left(-\mathrm{sin}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)<0\wedge 0<\mathrm{cos}\left({A}-\left(\frac{\mathrm{\pi }}{2}\right)\right)\right)\right)$
50 34 49 sylibrd ${⊢}{A}\in ℝ\to \left(\left(\frac{\mathrm{\pi }}{2}<{A}\wedge {A}<\mathrm{\pi }\right)\to \left(\mathrm{cos}{A}<0\wedge 0<\mathrm{sin}{A}\right)\right)$
51 50 3impib ${⊢}\left({A}\in ℝ\wedge \frac{\mathrm{\pi }}{2}<{A}\wedge {A}<\mathrm{\pi }\right)\to \left(\mathrm{cos}{A}<0\wedge 0<\mathrm{sin}{A}\right)$
52 51 ancomd ${⊢}\left({A}\in ℝ\wedge \frac{\mathrm{\pi }}{2}<{A}\wedge {A}<\mathrm{\pi }\right)\to \left(0<\mathrm{sin}{A}\wedge \mathrm{cos}{A}<0\right)$
53 7 52 sylbi ${⊢}{A}\in \left(\frac{\mathrm{\pi }}{2},\mathrm{\pi }\right)\to \left(0<\mathrm{sin}{A}\wedge \mathrm{cos}{A}<0\right)$