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 eqtr4di ⊢ ( 𝐴 ∈ ℝ → ( ( ( 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 ) )