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 )