Metamath Proof Explorer


Theorem abssinbd

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 )

Proof

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 )