Theorem sinbnd2

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

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

Proof

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