Theorem asinrecl

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

	Ref	Expression
Assertion	asinrecl	$$⊢A\in \left[-1,1\right]\to arcsin\left(A\right)\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		halfpire	$$⊢\frac{\mathrm{\pi }}{2}\in ℝ$$
2	1	renegcli	$$⊢-\frac{\mathrm{\pi }}{2}\in ℝ$$
3		iccssre	$$⊢\left(-\frac{\mathrm{\pi }}{2}\in ℝ\wedge \frac{\mathrm{\pi }}{2}\in ℝ\right)\to \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]\subseteq ℝ$$
4	2 1 3	mp2an	$$⊢\left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]\subseteq ℝ$$
5		asinrebnd	$$⊢A\in \left[-1,1\right]\to arcsin\left(A\right)\in \left[-\frac{\mathrm{\pi }}{2},\frac{\mathrm{\pi }}{2}\right]$$
6	4 5	sselid	$$⊢A\in \left[-1,1\right]\to arcsin\left(A\right)\in ℝ$$