Theorem abssinbd

Description: Bound for the absolute value of the sine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	abssinbd	$$⊢A\in ℝ\to \left|\sin A\right|\le 1$$

Proof

Step	Hyp	Ref	Expression
1		sinbnd	$$⊢A\in ℝ\to \left(-1\le \sin A\wedge \sin A\le 1\right)$$
2		resincl	$$⊢A\in ℝ\to \sin A\in ℝ$$
3		1red	$$⊢A\in ℝ\to 1\in ℝ$$
4	2 3	absled	$$⊢A\in ℝ\to \left(\left|\sin A\right|\le 1\leftrightarrow \left(-1\le \sin A\wedge \sin A\le 1\right)\right)$$
5	1 4	mpbird	$$⊢A\in ℝ\to \left|\sin A\right|\le 1$$