Theorem sincos2sgn

Description: The signs of the sine and cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008)

	Ref	Expression
Assertion	sincos2sgn	$$⊢\left(0<\sin 2\wedge \cos 2<0\right)$$

Proof

Step	Hyp	Ref	Expression
1		2re	$$⊢2\in ℝ$$
2		2pos	$$⊢0<2$$
3	1	leidi	$$⊢2\le 2$$
4		0xr	$$⊢0\in {ℝ}^{*}$$
5		elioc2	$$⊢\left(0\in {ℝ}^{*}\wedge 2\in ℝ\right)\to \left(2\in \left(0,2\right]\leftrightarrow \left(2\in ℝ\wedge 0<2\wedge 2\le 2\right)\right)$$
6	4 1 5	mp2an	$$⊢2\in \left(0,2\right]\leftrightarrow \left(2\in ℝ\wedge 0<2\wedge 2\le 2\right)$$
7	1 2 3 6	mpbir3an	$$⊢2\in \left(0,2\right]$$
8		sin02gt0	$$⊢2\in \left(0,2\right]\to 0<\sin 2$$
9	7 8	ax-mp	$$⊢0<\sin 2$$
10		cos2bnd	$$⊢\left(-\frac{7}{9}<\cos 2\wedge \cos 2<-\frac{1}{9}\right)$$
11	10	simpri	$$⊢\cos 2<-\frac{1}{9}$$
12		9re	$$⊢9\in ℝ$$
13		9pos	$$⊢0<9$$
14	12 13	recgt0ii	$$⊢0<\frac{1}{9}$$
15	12 13	gt0ne0ii	$$⊢9\ne 0$$
16	12 15	rereccli	$$⊢\frac{1}{9}\in ℝ$$
17		lt0neg2	$$⊢\frac{1}{9}\in ℝ\to \left(0<\frac{1}{9}\leftrightarrow -\frac{1}{9}<0\right)$$
18	16 17	ax-mp	$$⊢0<\frac{1}{9}\leftrightarrow -\frac{1}{9}<0$$
19	14 18	mpbi	$$⊢-\frac{1}{9}<0$$
20		recoscl	$$⊢2\in ℝ\to \cos 2\in ℝ$$
21	1 20	ax-mp	$$⊢\cos 2\in ℝ$$
22	16	renegcli	$$⊢-\frac{1}{9}\in ℝ$$
23		0re	$$⊢0\in ℝ$$
24	21 22 23	lttri	$$⊢\left(\cos 2<-\frac{1}{9}\wedge -\frac{1}{9}<0\right)\to \cos 2<0$$
25	11 19 24	mp2an	$$⊢\cos 2<0$$
26	9 25	pm3.2i	$$⊢\left(0<\sin 2\wedge \cos 2<0\right)$$