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

Metamath Proof Explorer

Theorem sincos2sgn

Description: The signs of the sine and cosine of 2. (Contributed by Paul Chapman, 19-Jan-2008)

Ref Expression
Assertion sincos2sgn ( 0 < ( sin ‘ 2 ) ∧ ( cos ‘ 2 ) < 0 )

Proof

Step Hyp Ref Expression
1 2re ⊢ 2 ∈ ℝ
2 2pos ⊢ 0 < 2
3 1 leidi ⊢ 2 ≤ 2
4 0xr ⊢ 0 ∈ ℝ*
5 elioc2 ⊢ ( ( 0 ∈ ℝ* ∧ 2 ∈ ℝ ) → ( 2 ∈ ( 0 (,] 2 ) ↔ ( 2 ∈ ℝ ∧ 0 < 2 ∧ 2 ≤ 2 ) ) )
6 4 1 5 mp2an ⊢ ( 2 ∈ ( 0 (,] 2 ) ↔ ( 2 ∈ ℝ ∧ 0 < 2 ∧ 2 ≤ 2 ) )
7 1 2 3 6 mpbir3an ⊢ 2 ∈ ( 0 (,] 2 )
8 sin02gt0 ⊢ ( 2 ∈ ( 0 (,] 2 ) → 0 < ( sin ‘ 2 ) )
9 7 8 ax-mp ⊢ 0 < ( sin ‘ 2 )
10 cos2bnd ⊢ ( - ( 7 / 9 ) < ( cos ‘ 2 ) ∧ ( cos ‘ 2 ) < - ( 1 / 9 ) )
11 10 simpri ⊢ ( cos ‘ 2 ) < - ( 1 / 9 )
12 9re ⊢ 9 ∈ ℝ
13 9pos ⊢ 0 < 9
14 12 13 recgt0ii ⊢ 0 < ( 1 / 9 )
15 12 13 gt0ne0ii ⊢ 9 ≠ 0
16 12 15 rereccli ⊢ ( 1 / 9 ) ∈ ℝ
17 lt0neg2 ⊢ ( ( 1 / 9 ) ∈ ℝ → ( 0 < ( 1 / 9 ) ↔ - ( 1 / 9 ) < 0 ) )
18 16 17 ax-mp ⊢ ( 0 < ( 1 / 9 ) ↔ - ( 1 / 9 ) < 0 )
19 14 18 mpbi ⊢ - ( 1 / 9 ) < 0
20 recoscl ⊢ ( 2 ∈ ℝ → ( cos ‘ 2 ) ∈ ℝ )
21 1 20 ax-mp ⊢ ( cos ‘ 2 ) ∈ ℝ
22 16 renegcli ⊢ - ( 1 / 9 ) ∈ ℝ
23 0re ⊢ 0 ∈ ℝ
24 21 22 23 lttri ⊢ ( ( ( cos ‘ 2 ) < - ( 1 / 9 ) ∧ - ( 1 / 9 ) < 0 ) → ( cos ‘ 2 ) < 0 )
25 11 19 24 mp2an ⊢ ( cos ‘ 2 ) < 0
26 9 25 pm3.2i ⊢ ( 0 < ( sin ‘ 2 ) ∧ ( cos ‘ 2 ) < 0 )