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	⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ( - 1 [,] 1 ) )

Proof

Step	Hyp	Ref	Expression
1		recoscl	⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ℝ )
2		cosbnd	⊢ ( 𝐴 ∈ ℝ → ( - 1 ≤ ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) ≤ 1 ) )
3	2	simpld	⊢ ( 𝐴 ∈ ℝ → - 1 ≤ ( cos ‘ 𝐴 ) )
4	2	simprd	⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ≤ 1 )
5		neg1rr	⊢ - 1 ∈ ℝ
6		1re	⊢ 1 ∈ ℝ
7	5 6	elicc2i	⊢ ( ( cos ‘ 𝐴 ) ∈ ( - 1 [,] 1 ) ↔ ( ( cos ‘ 𝐴 ) ∈ ℝ ∧ - 1 ≤ ( cos ‘ 𝐴 ) ∧ ( cos ‘ 𝐴 ) ≤ 1 ) )
8	1 3 4 7	syl3anbrc	⊢ ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ( - 1 [,] 1 ) )