Metamath Proof Explorer

Theorem sincosq1sgn

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

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

Proof

Step Hyp Ref Expression
1 0xr ${⊢}0\in {ℝ}^{*}$
2 halfpire ${⊢}\frac{\mathrm{\pi }}{2}\in ℝ$
3 2 rexri ${⊢}\frac{\mathrm{\pi }}{2}\in {ℝ}^{*}$
4 elioo2 ${⊢}\left(0\in {ℝ}^{*}\wedge \frac{\mathrm{\pi }}{2}\in {ℝ}^{*}\right)\to \left({A}\in \left(0,\frac{\mathrm{\pi }}{2}\right)↔\left({A}\in ℝ\wedge 0<{A}\wedge {A}<\frac{\mathrm{\pi }}{2}\right)\right)$
5 1 3 4 mp2an ${⊢}{A}\in \left(0,\frac{\mathrm{\pi }}{2}\right)↔\left({A}\in ℝ\wedge 0<{A}\wedge {A}<\frac{\mathrm{\pi }}{2}\right)$
6 sincosq1lem ${⊢}\left({A}\in ℝ\wedge 0<{A}\wedge {A}<\frac{\mathrm{\pi }}{2}\right)\to 0<\mathrm{sin}{A}$
7 resubcl ${⊢}\left(\frac{\mathrm{\pi }}{2}\in ℝ\wedge {A}\in ℝ\right)\to \left(\frac{\mathrm{\pi }}{2}\right)-{A}\in ℝ$
8 2 7 mpan ${⊢}{A}\in ℝ\to \left(\frac{\mathrm{\pi }}{2}\right)-{A}\in ℝ$
9 sincosq1lem ${⊢}\left(\left(\frac{\mathrm{\pi }}{2}\right)-{A}\in ℝ\wedge 0<\left(\frac{\mathrm{\pi }}{2}\right)-{A}\wedge \left(\frac{\mathrm{\pi }}{2}\right)-{A}<\frac{\mathrm{\pi }}{2}\right)\to 0<\mathrm{sin}\left(\left(\frac{\mathrm{\pi }}{2}\right)-{A}\right)$
10 8 9 syl3an1 ${⊢}\left({A}\in ℝ\wedge 0<\left(\frac{\mathrm{\pi }}{2}\right)-{A}\wedge \left(\frac{\mathrm{\pi }}{2}\right)-{A}<\frac{\mathrm{\pi }}{2}\right)\to 0<\mathrm{sin}\left(\left(\frac{\mathrm{\pi }}{2}\right)-{A}\right)$
11 10 3expib ${⊢}{A}\in ℝ\to \left(\left(0<\left(\frac{\mathrm{\pi }}{2}\right)-{A}\wedge \left(\frac{\mathrm{\pi }}{2}\right)-{A}<\frac{\mathrm{\pi }}{2}\right)\to 0<\mathrm{sin}\left(\left(\frac{\mathrm{\pi }}{2}\right)-{A}\right)\right)$
12 0re ${⊢}0\in ℝ$
13 ltsub13 ${⊢}\left(0\in ℝ\wedge \frac{\mathrm{\pi }}{2}\in ℝ\wedge {A}\in ℝ\right)\to \left(0<\left(\frac{\mathrm{\pi }}{2}\right)-{A}↔{A}<\left(\frac{\mathrm{\pi }}{2}\right)-0\right)$
14 12 2 13 mp3an12 ${⊢}{A}\in ℝ\to \left(0<\left(\frac{\mathrm{\pi }}{2}\right)-{A}↔{A}<\left(\frac{\mathrm{\pi }}{2}\right)-0\right)$
15 2 recni ${⊢}\frac{\mathrm{\pi }}{2}\in ℂ$
16 15 subid1i ${⊢}\left(\frac{\mathrm{\pi }}{2}\right)-0=\frac{\mathrm{\pi }}{2}$
17 16 breq2i ${⊢}{A}<\left(\frac{\mathrm{\pi }}{2}\right)-0↔{A}<\frac{\mathrm{\pi }}{2}$
18 14 17 syl6bb ${⊢}{A}\in ℝ\to \left(0<\left(\frac{\mathrm{\pi }}{2}\right)-{A}↔{A}<\frac{\mathrm{\pi }}{2}\right)$
19 ltsub23 ${⊢}\left(\frac{\mathrm{\pi }}{2}\in ℝ\wedge {A}\in ℝ\wedge \frac{\mathrm{\pi }}{2}\in ℝ\right)\to \left(\left(\frac{\mathrm{\pi }}{2}\right)-{A}<\frac{\mathrm{\pi }}{2}↔\left(\frac{\mathrm{\pi }}{2}\right)-\left(\frac{\mathrm{\pi }}{2}\right)<{A}\right)$
20 2 2 19 mp3an13 ${⊢}{A}\in ℝ\to \left(\left(\frac{\mathrm{\pi }}{2}\right)-{A}<\frac{\mathrm{\pi }}{2}↔\left(\frac{\mathrm{\pi }}{2}\right)-\left(\frac{\mathrm{\pi }}{2}\right)<{A}\right)$
21 15 subidi ${⊢}\left(\frac{\mathrm{\pi }}{2}\right)-\left(\frac{\mathrm{\pi }}{2}\right)=0$
22 21 breq1i ${⊢}\left(\frac{\mathrm{\pi }}{2}\right)-\left(\frac{\mathrm{\pi }}{2}\right)<{A}↔0<{A}$
23 20 22 syl6bb ${⊢}{A}\in ℝ\to \left(\left(\frac{\mathrm{\pi }}{2}\right)-{A}<\frac{\mathrm{\pi }}{2}↔0<{A}\right)$
24 18 23 anbi12d ${⊢}{A}\in ℝ\to \left(\left(0<\left(\frac{\mathrm{\pi }}{2}\right)-{A}\wedge \left(\frac{\mathrm{\pi }}{2}\right)-{A}<\frac{\mathrm{\pi }}{2}\right)↔\left({A}<\frac{\mathrm{\pi }}{2}\wedge 0<{A}\right)\right)$
25 24 biancomd ${⊢}{A}\in ℝ\to \left(\left(0<\left(\frac{\mathrm{\pi }}{2}\right)-{A}\wedge \left(\frac{\mathrm{\pi }}{2}\right)-{A}<\frac{\mathrm{\pi }}{2}\right)↔\left(0<{A}\wedge {A}<\frac{\mathrm{\pi }}{2}\right)\right)$
26 recn ${⊢}{A}\in ℝ\to {A}\in ℂ$
27 sinhalfpim ${⊢}{A}\in ℂ\to \mathrm{sin}\left(\left(\frac{\mathrm{\pi }}{2}\right)-{A}\right)=\mathrm{cos}{A}$
28 26 27 syl ${⊢}{A}\in ℝ\to \mathrm{sin}\left(\left(\frac{\mathrm{\pi }}{2}\right)-{A}\right)=\mathrm{cos}{A}$
29 28 breq2d ${⊢}{A}\in ℝ\to \left(0<\mathrm{sin}\left(\left(\frac{\mathrm{\pi }}{2}\right)-{A}\right)↔0<\mathrm{cos}{A}\right)$
30 11 25 29 3imtr3d ${⊢}{A}\in ℝ\to \left(\left(0<{A}\wedge {A}<\frac{\mathrm{\pi }}{2}\right)\to 0<\mathrm{cos}{A}\right)$
31 30 3impib ${⊢}\left({A}\in ℝ\wedge 0<{A}\wedge {A}<\frac{\mathrm{\pi }}{2}\right)\to 0<\mathrm{cos}{A}$
32 6 31 jca ${⊢}\left({A}\in ℝ\wedge 0<{A}\wedge {A}<\frac{\mathrm{\pi }}{2}\right)\to \left(0<\mathrm{sin}{A}\wedge 0<\mathrm{cos}{A}\right)$
33 5 32 sylbi ${⊢}{A}\in \left(0,\frac{\mathrm{\pi }}{2}\right)\to \left(0<\mathrm{sin}{A}\wedge 0<\mathrm{cos}{A}\right)$