Theorem asinrecl

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

	Ref	Expression
Assertion	asinrecl	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( arcsin ‘ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		halfpire	⊢ ( π / 2 ) ∈ ℝ
2	1	renegcli	⊢ - ( π / 2 ) ∈ ℝ
3		iccssre	⊢ ( ( - ( π / 2 ) ∈ ℝ ∧ ( π / 2 ) ∈ ℝ ) → ( - ( π / 2 ) [,] ( π / 2 ) ) ⊆ ℝ )
4	2 1 3	mp2an	⊢ ( - ( π / 2 ) [,] ( π / 2 ) ) ⊆ ℝ
5		asinrebnd	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( arcsin ‘ 𝐴 ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
6	4 5	sselid	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( arcsin ‘ 𝐴 ) ∈ ℝ )