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

Proof

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