This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 )