Description: Bound for the absolute value of the sine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019)
Ref | Expression | ||
---|---|---|---|
Assertion | abssinbd | |- ( A e. RR -> ( abs ` ( sin ` A ) ) <_ 1 ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | sinbnd | |- ( A e. RR -> ( -u 1 <_ ( sin ` A ) /\ ( sin ` A ) <_ 1 ) ) |
|
2 | resincl | |- ( A e. RR -> ( sin ` A ) e. RR ) |
|
3 | 1red | |- ( A e. RR -> 1 e. RR ) |
|
4 | 2 3 | absled | |- ( A e. RR -> ( ( abs ` ( sin ` A ) ) <_ 1 <-> ( -u 1 <_ ( sin ` A ) /\ ( sin ` A ) <_ 1 ) ) ) |
5 | 1 4 | mpbird | |- ( A e. RR -> ( abs ` ( sin ` A ) ) <_ 1 ) |