Theorem sincos2sgn

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

	Ref	Expression
Assertion	sincos2sgn	|- ( 0 < ( sin ` 2 ) /\ ( cos ` 2 ) < 0 )

Proof

Step	Hyp	Ref	Expression
1		2re	|- 2 e. RR
2		2pos	|- 0 < 2
3	1	leidi	|- 2 <_ 2
4		0xr	|- 0 e. RR*
5		elioc2	|- ( ( 0 e. RR* /\ 2 e. RR ) -> ( 2 e. ( 0 (,] 2 ) <-> ( 2 e. RR /\ 0 < 2 /\ 2 <_ 2 ) ) )
6	4 1 5	mp2an	|- ( 2 e. ( 0 (,] 2 ) <-> ( 2 e. RR /\ 0 < 2 /\ 2 <_ 2 ) )
7	1 2 3 6	mpbir3an	|- 2 e. ( 0 (,] 2 )
8		sin02gt0	|- ( 2 e. ( 0 (,] 2 ) -> 0 < ( sin ` 2 ) )
9	7 8	ax-mp	|- 0 < ( sin ` 2 )
10		cos2bnd	|- ( -u ( 7 / 9 ) < ( cos ` 2 ) /\ ( cos ` 2 ) < -u ( 1 / 9 ) )
11	10	simpri	|- ( cos ` 2 ) < -u ( 1 / 9 )
12		9re	|- 9 e. RR
13		9pos	|- 0 < 9
14	12 13	recgt0ii	|- 0 < ( 1 / 9 )
15	12 13	gt0ne0ii	|- 9 =/= 0
16	12 15	rereccli	|- ( 1 / 9 ) e. RR
17		lt0neg2	|- ( ( 1 / 9 ) e. RR -> ( 0 < ( 1 / 9 ) <-> -u ( 1 / 9 ) < 0 ) )
18	16 17	ax-mp	|- ( 0 < ( 1 / 9 ) <-> -u ( 1 / 9 ) < 0 )
19	14 18	mpbi	|- -u ( 1 / 9 ) < 0
20		recoscl	|- ( 2 e. RR -> ( cos ` 2 ) e. RR )
21	1 20	ax-mp	|- ( cos ` 2 ) e. RR
22	16	renegcli	|- -u ( 1 / 9 ) e. RR
23		0re	|- 0 e. RR
24	21 22 23	lttri	|- ( ( ( cos ` 2 ) < -u ( 1 / 9 ) /\ -u ( 1 / 9 ) < 0 ) -> ( cos ` 2 ) < 0 )
25	11 19 24	mp2an	|- ( cos ` 2 ) < 0
26	9 25	pm3.2i	|- ( 0 < ( sin ` 2 ) /\ ( cos ` 2 ) < 0 )