Theorem abscosbd

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

	Ref	Expression
Assertion	abscosbd	$$⊢A\in ℝ\to \left|\cos A\right|\le 1$$

Proof

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