This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem cosbnd2

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

		Ref	Expression
	Assertion	cosbnd2	$⊢ A \in ℝ \to \cos A \in [- 1, 1]$

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