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