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 )