sincos1sgn

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

		Ref	Expression
	Assertion	sincos1sgn	$⊢ (0 < \sin 1 \land 0 < \cos 1)$

Step	Hyp	Ref	Expression
1		1re	$⊢ 1 \in ℝ$
2		0lt1	$⊢ 0 < 1$
3		1le1	$⊢ 1 \leq 1$
4		0xr	$⊢ 0 \in ℝ^{*}$
5		elioc2	$⊢ (0 \in ℝ^{*} \land 1 \in ℝ) \to (1 \in (0, 1] \leftrightarrow (1 \in ℝ \land 0 < 1 \land 1 \leq 1))$
6	4 1 5	mp2an	$⊢ 1 \in (0, 1] \leftrightarrow (1 \in ℝ \land 0 < 1 \land 1 \leq 1)$
7	1 2 3 6	mpbir3an	$⊢ 1 \in (0, 1]$
8		sin01gt0	$⊢ 1 \in (0, 1] \to 0 < \sin 1$
9		cos01gt0	$⊢ 1 \in (0, 1] \to 0 < \cos 1$
10	8 9	jca	$⊢ 1 \in (0, 1] \to (0 < \sin 1 \land 0 < \cos 1)$
11	7 10	ax-mp	$⊢ (0 < \sin 1 \land 0 < \cos 1)$

Metamath Proof Explorer