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

Metamath Proof Explorer

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