Metamath Proof Explorer

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 ⊢ A ∈ ℝ → sin ⁡ A ∈ − 1 1

Proof

Step Hyp Ref Expression
1 resincl ⊢ A ∈ ℝ → sin ⁡ A ∈ ℝ
2 sinbnd ⊢ A ∈ ℝ → − 1 ≤ sin ⁡ A ∧ sin ⁡ A ≤ 1
3 2 simpld ⊢ A ∈ ℝ → − 1 ≤ sin ⁡ A
4 2 simprd ⊢ A ∈ ℝ → sin ⁡ A ≤ 1
5 neg1rr ⊢ − 1 ∈ ℝ
6 1re ⊢ 1 ∈ ℝ
7 5 6 elicc2i ⊢ sin ⁡ A ∈ − 1 1 ↔ sin ⁡ A ∈ ℝ ∧ − 1 ≤ sin ⁡ A ∧ sin ⁡ A ≤ 1
8 1 3 4 7 syl3anbrc ⊢ A ∈ ℝ → sin ⁡ A ∈ − 1 1