sinbnd2

Description: The sine of a real number is in the closed interval from -1 to 1. (Contributed by Mario Carneiro, 12-May-2014)

		Ref	Expression
	Assertion	sinbnd2	$⊢ A \in ℝ \to \sin A \in [- 1, 1]$

Step	Hyp	Ref	Expression
1		resincl	$⊢ A \in ℝ \to \sin A \in ℝ$
2		sinbnd	$⊢ A \in ℝ \to (- 1 \leq \sin A \land \sin A \leq 1)$
3	2	simpld	$⊢ A \in ℝ \to - 1 \leq \sin A$
4	2	simprd	$⊢ A \in ℝ \to \sin A \leq 1$
5		neg1rr	$⊢ - 1 \in ℝ$
6		1re	$⊢ 1 \in ℝ$
7	5 6	elicc2i	$⊢ \sin A \in [- 1, 1] \leftrightarrow (\sin A \in ℝ \land - 1 \leq \sin A \land \sin A \leq 1)$
8	1 3 4 7	syl3anbrc	$⊢ A \in ℝ \to \sin A \in [- 1, 1]$

Metamath Proof Explorer