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

Proof

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