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⁡A2
3 resincl ⊢A∈ℝ→sin⁡A∈ℝ
4 3 resqcld ⊢A∈ℝ→sin⁡A2∈ℝ
5 1 resqcld ⊢A∈ℝ→cos⁡A2∈ℝ
6 4 5 addge01d ⊢A∈ℝ→0≤cos⁡A2↔sin⁡A2≤sin⁡A2+cos⁡A2
7 2 6 mpbid ⊢A∈ℝ→sin⁡A2≤sin⁡A2+cos⁡A2
8 recn ⊢A∈ℝ→A∈ℂ
9 sincossq ⊢A∈ℂ→sin⁡A2+cos⁡A2=1
10 8 9 syl ⊢A∈ℝ→sin⁡A2+cos⁡A2=1
11 sq1 ⊢12=1
12 10 11 eqtr4di ⊢A∈ℝ→sin⁡A2+cos⁡A2=12
13 7 12 breqtrd ⊢A∈ℝ→sin⁡A2≤12
14 1re ⊢1∈ℝ
15 0le1 ⊢0≤1
16 lenegsq ⊢sin⁡A∈ℝ∧1∈ℝ∧0≤1→sin⁡A≤1∧−sin⁡A≤1↔sin⁡A2≤12
17 14 15 16 mp3an23 ⊢sin⁡A∈ℝ→sin⁡A≤1∧−sin⁡A≤1↔sin⁡A2≤12
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⁡A2≤12↔sin⁡A≤1∧−1≤sin⁡A
22 3 21 syl ⊢A∈ℝ→sin⁡A2≤12↔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