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 )