Theorem sin4lt0

Description: The sine of 4 is negative. (Contributed by Paul Chapman, 19-Jan-2008)

	Ref	Expression
Assertion	sin4lt0	|- ( sin ` 4 ) < 0

Proof

Step	Hyp	Ref	Expression
1		2t2e4	|- ( 2 x. 2 ) = 4
2	1	fveq2i	|- ( sin ` ( 2 x. 2 ) ) = ( sin ` 4 )
3		2cn	|- 2 e. CC
4		sin2t	|- ( 2 e. CC -> ( sin ` ( 2 x. 2 ) ) = ( 2 x. ( ( sin ` 2 ) x. ( cos ` 2 ) ) ) )
5	3 4	ax-mp	|- ( sin ` ( 2 x. 2 ) ) = ( 2 x. ( ( sin ` 2 ) x. ( cos ` 2 ) ) )
6	2 5	eqtr3i	|- ( sin ` 4 ) = ( 2 x. ( ( sin ` 2 ) x. ( cos ` 2 ) ) )
7		sincos2sgn	|- ( 0 < ( sin ` 2 ) /\ ( cos ` 2 ) < 0 )
8	7	simpri	|- ( cos ` 2 ) < 0
9		2re	|- 2 e. RR
10		recoscl	|- ( 2 e. RR -> ( cos ` 2 ) e. RR )
11	9 10	ax-mp	|- ( cos ` 2 ) e. RR
12		0re	|- 0 e. RR
13		resincl	|- ( 2 e. RR -> ( sin ` 2 ) e. RR )
14	9 13	ax-mp	|- ( sin ` 2 ) e. RR
15	7	simpli	|- 0 < ( sin ` 2 )
16	14 15	pm3.2i	|- ( ( sin ` 2 ) e. RR /\ 0 < ( sin ` 2 ) )
17		ltmul2	|- ( ( ( cos ` 2 ) e. RR /\ 0 e. RR /\ ( ( sin ` 2 ) e. RR /\ 0 < ( sin ` 2 ) ) ) -> ( ( cos ` 2 ) < 0 <-> ( ( sin ` 2 ) x. ( cos ` 2 ) ) < ( ( sin ` 2 ) x. 0 ) ) )
18	11 12 16 17	mp3an	|- ( ( cos ` 2 ) < 0 <-> ( ( sin ` 2 ) x. ( cos ` 2 ) ) < ( ( sin ` 2 ) x. 0 ) )
19	8 18	mpbi	|- ( ( sin ` 2 ) x. ( cos ` 2 ) ) < ( ( sin ` 2 ) x. 0 )
20	14	recni	|- ( sin ` 2 ) e. CC
21	20	mul01i	|- ( ( sin ` 2 ) x. 0 ) = 0
22	19 21	breqtri	|- ( ( sin ` 2 ) x. ( cos ` 2 ) ) < 0
23	14 11	remulcli	|- ( ( sin ` 2 ) x. ( cos ` 2 ) ) e. RR
24		2pos	|- 0 < 2
25	9 24	pm3.2i	|- ( 2 e. RR /\ 0 < 2 )
26		ltmul2	|- ( ( ( ( sin ` 2 ) x. ( cos ` 2 ) ) e. RR /\ 0 e. RR /\ ( 2 e. RR /\ 0 < 2 ) ) -> ( ( ( sin ` 2 ) x. ( cos ` 2 ) ) < 0 <-> ( 2 x. ( ( sin ` 2 ) x. ( cos ` 2 ) ) ) < ( 2 x. 0 ) ) )
27	23 12 25 26	mp3an	|- ( ( ( sin ` 2 ) x. ( cos ` 2 ) ) < 0 <-> ( 2 x. ( ( sin ` 2 ) x. ( cos ` 2 ) ) ) < ( 2 x. 0 ) )
28	22 27	mpbi	|- ( 2 x. ( ( sin ` 2 ) x. ( cos ` 2 ) ) ) < ( 2 x. 0 )
29	3	mul01i	|- ( 2 x. 0 ) = 0
30	28 29	breqtri	|- ( 2 x. ( ( sin ` 2 ) x. ( cos ` 2 ) ) ) < 0
31	6 30	eqbrtri	|- ( sin ` 4 ) < 0