Theorem abscosbd

Description: Bound for the absolute value of the cosine of a real number. (Contributed by Glauco Siliprandi, 11-Dec-2019)

	Ref	Expression
Assertion	abscosbd	|- ( A e. RR -> ( abs ` ( cos ` A ) ) <_ 1 )

Proof

Step	Hyp	Ref	Expression
1		cosbnd	|- ( A e. RR -> ( -u 1 <_ ( cos ` A ) /\ ( cos ` A ) <_ 1 ) )
2		recoscl	|- ( A e. RR -> ( cos ` A ) e. RR )
3		1red	|- ( A e. RR -> 1 e. RR )
4	2 3	absled	|- ( A e. RR -> ( ( abs ` ( cos ` A ) ) <_ 1 <-> ( -u 1 <_ ( cos ` A ) /\ ( cos ` A ) <_ 1 ) ) )
5	1 4	mpbird	|- ( A e. RR -> ( abs ` ( cos ` A ) ) <_ 1 )