Theorem cosbnd2

Description: The cosine of a real number is in the closed interval from -1 to 1. (Contributed by Mario Carneiro, 12-May-2014)

	Ref	Expression
Assertion	cosbnd2	|- ( A e. RR -> ( cos ` A ) e. ( -u 1 [,] 1 ) )

Proof

Step	Hyp	Ref	Expression
1		recoscl	|- ( A e. RR -> ( cos ` A ) e. RR )
2		cosbnd	|- ( A e. RR -> ( -u 1 <_ ( cos ` A ) /\ ( cos ` A ) <_ 1 ) )
3	2	simpld	|- ( A e. RR -> -u 1 <_ ( cos ` A ) )
4	2	simprd	|- ( A e. RR -> ( cos ` A ) <_ 1 )
5		neg1rr	|- -u 1 e. RR
6		1re	|- 1 e. RR
7	5 6	elicc2i	|- ( ( cos ` A ) e. ( -u 1 [,] 1 ) <-> ( ( cos ` A ) e. RR /\ -u 1 <_ ( cos ` A ) /\ ( cos ` A ) <_ 1 ) )
8	1 3 4 7	syl3anbrc	|- ( A e. RR -> ( cos ` A ) e. ( -u 1 [,] 1 ) )