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\cdot 2=4$$
2	1	fveq2i	$$⊢\sin 2\cdot 2=\sin 4$$
3		2cn	$$⊢2\in ℂ$$
4		sin2t	$$⊢2\in ℂ\to \sin 2\cdot 2=2\sin 2\cos 2$$
5	3 4	ax-mp	$$⊢\sin 2\cdot 2=2\sin 2\cos 2$$
6	2 5	eqtr3i	$$⊢\sin 4=2\sin 2\cos 2$$
7		sincos2sgn	$$⊢\left(0<\sin 2\wedge \cos 2<0\right)$$
8	7	simpri	$$⊢\cos 2<0$$
9		2re	$$⊢2\in ℝ$$
10		recoscl	$$⊢2\in ℝ\to \cos 2\in ℝ$$
11	9 10	ax-mp	$$⊢\cos 2\in ℝ$$
12		0re	$$⊢0\in ℝ$$
13		resincl	$$⊢2\in ℝ\to \sin 2\in ℝ$$
14	9 13	ax-mp	$$⊢\sin 2\in ℝ$$
15	7	simpli	$$⊢0<\sin 2$$
16	14 15	pm3.2i	$$⊢\left(\sin 2\in ℝ\wedge 0<\sin 2\right)$$
17		ltmul2	$$⊢\left(\cos 2\in ℝ\wedge 0\in ℝ\wedge \left(\sin 2\in ℝ\wedge 0<\sin 2\right)\right)\to \left(\cos 2<0\leftrightarrow \sin 2\cos 2<\sin 2\cdot 0\right)$$
18	11 12 16 17	mp3an	$$⊢\cos 2<0\leftrightarrow \sin 2\cos 2<\sin 2\cdot 0$$
19	8 18	mpbi	$$⊢\sin 2\cos 2<\sin 2\cdot 0$$
20	14	recni	$$⊢\sin 2\in ℂ$$
21	20	mul01i	$$⊢\sin 2\cdot 0=0$$
22	19 21	breqtri	$$⊢\sin 2\cos 2<0$$
23	14 11	remulcli	$$⊢\sin 2\cos 2\in ℝ$$
24		2pos	$$⊢0<2$$
25	9 24	pm3.2i	$$⊢\left(2\in ℝ\wedge 0<2\right)$$
26		ltmul2	$$⊢\left(\sin 2\cos 2\in ℝ\wedge 0\in ℝ\wedge \left(2\in ℝ\wedge 0<2\right)\right)\to \left(\sin 2\cos 2<0\leftrightarrow 2\sin 2\cos 2<2\cdot 0\right)$$
27	23 12 25 26	mp3an	$$⊢\sin 2\cos 2<0\leftrightarrow 2\sin 2\cos 2<2\cdot 0$$
28	22 27	mpbi	$$⊢2\sin 2\cos 2<2\cdot 0$$
29	3	mul01i	$$⊢2\cdot 0=0$$
30	28 29	breqtri	$$⊢2\sin 2\cos 2<0$$
31	6 30	eqbrtri	$$⊢\sin 4<0$$