Metamath Proof Explorer

Theorem sincos1sgn

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

Ref Expression
Assertion sincos1sgn 
|- ( 0 < ( sin ` 1 ) /\ 0 < ( cos ` 1 ) )

Proof

Step Hyp Ref Expression
1 1re 
 |-  1 e. RR
2 0lt1 
 |-  0 < 1
3 1le1 
 |-  1 <_ 1
4 0xr 
 |-  0 e. RR*
5 elioc2 
 |-  ( ( 0 e. RR* /\ 1 e. RR ) -> ( 1 e. ( 0 (,] 1 ) <-> ( 1 e. RR /\ 0 < 1 /\ 1 <_ 1 ) ) )
6 4 1 5 mp2an 
 |-  ( 1 e. ( 0 (,] 1 ) <-> ( 1 e. RR /\ 0 < 1 /\ 1 <_ 1 ) )
7 1 2 3 6 mpbir3an 
 |-  1 e. ( 0 (,] 1 )
8 sin01gt0 
 |-  ( 1 e. ( 0 (,] 1 ) -> 0 < ( sin ` 1 ) )
9 cos01gt0 
 |-  ( 1 e. ( 0 (,] 1 ) -> 0 < ( cos ` 1 ) )
10 8 9 jca 
 |-  ( 1 e. ( 0 (,] 1 ) -> ( 0 < ( sin ` 1 ) /\ 0 < ( cos ` 1 ) ) )
11 7 10 ax-mp 
 |-  ( 0 < ( sin ` 1 ) /\ 0 < ( cos ` 1 ) )