Theorem asinrecl

Description: The arcsine function is real in its principal domain. (Contributed by Mario Carneiro, 2-Apr-2015)

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

Proof

Step	Hyp	Ref	Expression
1		halfpire	|- ( _pi / 2 ) e. RR
2	1	renegcli	|- -u ( _pi / 2 ) e. RR
3		iccssre	|- ( ( -u ( _pi / 2 ) e. RR /\ ( _pi / 2 ) e. RR ) -> ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) C_ RR )
4	2 1 3	mp2an	|- ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) C_ RR
5		asinrebnd	|- ( A e. ( -u 1 [,] 1 ) -> ( arcsin ` A ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
6	4 5	sselid	|- ( A e. ( -u 1 [,] 1 ) -> ( arcsin ` A ) e. RR )