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