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

Metamath Proof Explorer

Theorem sinq34lt0t

Description: The sine of a number strictly between _pi and 2 x. _pi is negative. (Contributed by NM, 17-Aug-2008)

Ref Expression
Assertion sinq34lt0t 
|- ( A e. ( _pi (,) ( 2 x. _pi ) ) -> ( sin ` A ) < 0 )

Proof

Step Hyp Ref Expression
1 elioore 
 |-  ( A e. ( _pi (,) ( 2 x. _pi ) ) -> A e. RR )
2 picn 
 |-  _pi e. CC
3 2 addlidi 
 |-  ( 0 + _pi ) = _pi
4 3 eqcomi 
 |-  _pi = ( 0 + _pi )
5 2 2timesi 
 |-  ( 2 x. _pi ) = ( _pi + _pi )
6 4 5 oveq12i 
 |-  ( _pi (,) ( 2 x. _pi ) ) = ( ( 0 + _pi ) (,) ( _pi + _pi ) )
7 6 eleq2i 
 |-  ( A e. ( _pi (,) ( 2 x. _pi ) ) <-> A e. ( ( 0 + _pi ) (,) ( _pi + _pi ) ) )
8 pire 
 |-  _pi e. RR
9 0re 
 |-  0 e. RR
10 iooshf 
 |-  ( ( ( A e. RR /\ _pi e. RR ) /\ ( 0 e. RR /\ _pi e. RR ) ) -> ( ( A - _pi ) e. ( 0 (,) _pi ) <-> A e. ( ( 0 + _pi ) (,) ( _pi + _pi ) ) ) )
11 9 8 10 mpanr12 
 |-  ( ( A e. RR /\ _pi e. RR ) -> ( ( A - _pi ) e. ( 0 (,) _pi ) <-> A e. ( ( 0 + _pi ) (,) ( _pi + _pi ) ) ) )
12 8 11 mpan2 
 |-  ( A e. RR -> ( ( A - _pi ) e. ( 0 (,) _pi ) <-> A e. ( ( 0 + _pi ) (,) ( _pi + _pi ) ) ) )
13 7 12 bitr4id 
 |-  ( A e. RR -> ( A e. ( _pi (,) ( 2 x. _pi ) ) <-> ( A - _pi ) e. ( 0 (,) _pi ) ) )
14 1 13 syl 
 |-  ( A e. ( _pi (,) ( 2 x. _pi ) ) -> ( A e. ( _pi (,) ( 2 x. _pi ) ) <-> ( A - _pi ) e. ( 0 (,) _pi ) ) )
15 14 ibi 
 |-  ( A e. ( _pi (,) ( 2 x. _pi ) ) -> ( A - _pi ) e. ( 0 (,) _pi ) )
16 sinq12gt0 
 |-  ( ( A - _pi ) e. ( 0 (,) _pi ) -> 0 < ( sin ` ( A - _pi ) ) )
17 15 16 syl 
 |-  ( A e. ( _pi (,) ( 2 x. _pi ) ) -> 0 < ( sin ` ( A - _pi ) ) )
18 1 recnd 
 |-  ( A e. ( _pi (,) ( 2 x. _pi ) ) -> A e. CC )
19 sinmpi 
 |-  ( A e. CC -> ( sin ` ( A - _pi ) ) = -u ( sin ` A ) )
20 18 19 syl 
 |-  ( A e. ( _pi (,) ( 2 x. _pi ) ) -> ( sin ` ( A - _pi ) ) = -u ( sin ` A ) )
21 17 20 breqtrd 
 |-  ( A e. ( _pi (,) ( 2 x. _pi ) ) -> 0 < -u ( sin ` A ) )
22 1 resincld 
 |-  ( A e. ( _pi (,) ( 2 x. _pi ) ) -> ( sin ` A ) e. RR )
23 22 lt0neg1d 
 |-  ( A e. ( _pi (,) ( 2 x. _pi ) ) -> ( ( sin ` A ) < 0 <-> 0 < -u ( sin ` A ) ) )
24 21 23 mpbird 
 |-  ( A e. ( _pi (,) ( 2 x. _pi ) ) -> ( sin ` A ) < 0 )