# Metamath Proof Explorer

## Theorem sinbnd

Description: The sine of a real number lies between -1 and 1. Equation 18 of Gleason p. 311. (Contributed by NM, 16-Jan-2006)

Ref Expression
Assertion sinbnd ( 𝐴 ∈ ℝ → ( - 1 ≤ ( sin ‘ 𝐴 ) ∧ ( sin ‘ 𝐴 ) ≤ 1 ) )

### Proof

Step Hyp Ref Expression
1 recoscl ( 𝐴 ∈ ℝ → ( cos ‘ 𝐴 ) ∈ ℝ )
2 1 sqge0d ( 𝐴 ∈ ℝ → 0 ≤ ( ( cos ‘ 𝐴 ) ↑ 2 ) )
3 resincl ( 𝐴 ∈ ℝ → ( sin ‘ 𝐴 ) ∈ ℝ )
4 3 resqcld ( 𝐴 ∈ ℝ → ( ( sin ‘ 𝐴 ) ↑ 2 ) ∈ ℝ )
5 1 resqcld ( 𝐴 ∈ ℝ → ( ( cos ‘ 𝐴 ) ↑ 2 ) ∈ ℝ )
6 4 5 addge01d ( 𝐴 ∈ ℝ → ( 0 ≤ ( ( cos ‘ 𝐴 ) ↑ 2 ) ↔ ( ( sin ‘ 𝐴 ) ↑ 2 ) ≤ ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) ) )
7 2 6 mpbid ( 𝐴 ∈ ℝ → ( ( sin ‘ 𝐴 ) ↑ 2 ) ≤ ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) )
8 recn ( 𝐴 ∈ ℝ → 𝐴 ∈ ℂ )
9 sincossq ( 𝐴 ∈ ℂ → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = 1 )
10 8 9 syl ( 𝐴 ∈ ℝ → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = 1 )
11 sq1 ( 1 ↑ 2 ) = 1
12 10 11 syl6eqr ( 𝐴 ∈ ℝ → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) + ( ( cos ‘ 𝐴 ) ↑ 2 ) ) = ( 1 ↑ 2 ) )
13 7 12 breqtrd ( 𝐴 ∈ ℝ → ( ( sin ‘ 𝐴 ) ↑ 2 ) ≤ ( 1 ↑ 2 ) )
14 1re 1 ∈ ℝ
15 0le1 0 ≤ 1
16 lenegsq ( ( ( sin ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ∧ 0 ≤ 1 ) → ( ( ( sin ‘ 𝐴 ) ≤ 1 ∧ - ( sin ‘ 𝐴 ) ≤ 1 ) ↔ ( ( sin ‘ 𝐴 ) ↑ 2 ) ≤ ( 1 ↑ 2 ) ) )
17 14 15 16 mp3an23 ( ( sin ‘ 𝐴 ) ∈ ℝ → ( ( ( sin ‘ 𝐴 ) ≤ 1 ∧ - ( sin ‘ 𝐴 ) ≤ 1 ) ↔ ( ( sin ‘ 𝐴 ) ↑ 2 ) ≤ ( 1 ↑ 2 ) ) )
18 lenegcon1 ( ( ( sin ‘ 𝐴 ) ∈ ℝ ∧ 1 ∈ ℝ ) → ( - ( sin ‘ 𝐴 ) ≤ 1 ↔ - 1 ≤ ( sin ‘ 𝐴 ) ) )
19 14 18 mpan2 ( ( sin ‘ 𝐴 ) ∈ ℝ → ( - ( sin ‘ 𝐴 ) ≤ 1 ↔ - 1 ≤ ( sin ‘ 𝐴 ) ) )
20 19 anbi2d ( ( sin ‘ 𝐴 ) ∈ ℝ → ( ( ( sin ‘ 𝐴 ) ≤ 1 ∧ - ( sin ‘ 𝐴 ) ≤ 1 ) ↔ ( ( sin ‘ 𝐴 ) ≤ 1 ∧ - 1 ≤ ( sin ‘ 𝐴 ) ) ) )
21 17 20 bitr3d ( ( sin ‘ 𝐴 ) ∈ ℝ → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) ≤ ( 1 ↑ 2 ) ↔ ( ( sin ‘ 𝐴 ) ≤ 1 ∧ - 1 ≤ ( sin ‘ 𝐴 ) ) ) )
22 3 21 syl ( 𝐴 ∈ ℝ → ( ( ( sin ‘ 𝐴 ) ↑ 2 ) ≤ ( 1 ↑ 2 ) ↔ ( ( sin ‘ 𝐴 ) ≤ 1 ∧ - 1 ≤ ( sin ‘ 𝐴 ) ) ) )
23 13 22 mpbid ( 𝐴 ∈ ℝ → ( ( sin ‘ 𝐴 ) ≤ 1 ∧ - 1 ≤ ( sin ‘ 𝐴 ) ) )
24 23 ancomd ( 𝐴 ∈ ℝ → ( - 1 ≤ ( sin ‘ 𝐴 ) ∧ ( sin ‘ 𝐴 ) ≤ 1 ) )