Theorem asinrebnd

Description: Bounds on the arcsine function. (Contributed by Mario Carneiro, 2-Apr-2015)

	Ref	Expression
Assertion	asinrebnd	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( arcsin ‘ 𝐴 ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )

Proof

Step	Hyp	Ref	Expression
1		resinf1o	⊢ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) : ( - ( π / 2 ) [,] ( π / 2 ) ) –1-1-onto→ ( - 1 [,] 1 )
2		f1ocnv	⊢ ( ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) : ( - ( π / 2 ) [,] ( π / 2 ) ) –1-1-onto→ ( - 1 [,] 1 ) → ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) : ( - 1 [,] 1 ) –1-1-onto→ ( - ( π / 2 ) [,] ( π / 2 ) ) )
3		f1of	⊢ ( ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) : ( - 1 [,] 1 ) –1-1-onto→ ( - ( π / 2 ) [,] ( π / 2 ) ) → ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) : ( - 1 [,] 1 ) ⟶ ( - ( π / 2 ) [,] ( π / 2 ) ) )
4	1 2 3	mp2b	⊢ ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) : ( - 1 [,] 1 ) ⟶ ( - ( π / 2 ) [,] ( π / 2 ) )
5	4	ffvelcdmi	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ 𝐴 ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )
6	5	fvresd	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ ( ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ 𝐴 ) ) = ( sin ‘ ( ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ 𝐴 ) ) )
7		f1ocnvfv2	⊢ ( ( ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) : ( - ( π / 2 ) [,] ( π / 2 ) ) –1-1-onto→ ( - 1 [,] 1 ) ∧ 𝐴 ∈ ( - 1 [,] 1 ) ) → ( ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ ( ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ 𝐴 ) ) = 𝐴 )
8	1 7	mpan	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ ( ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ 𝐴 ) ) = 𝐴 )
9	6 8	eqtr3d	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( sin ‘ ( ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ 𝐴 ) ) = 𝐴 )
10	9	fveq2d	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( arcsin ‘ ( sin ‘ ( ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ 𝐴 ) ) ) = ( arcsin ‘ 𝐴 ) )
11		reasinsin	⊢ ( ( ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ 𝐴 ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( arcsin ‘ ( sin ‘ ( ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ 𝐴 ) ) ) = ( ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ 𝐴 ) )
12	5 11	syl	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( arcsin ‘ ( sin ‘ ( ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ 𝐴 ) ) ) = ( ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ 𝐴 ) )
13	10 12	eqtr3d	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( arcsin ‘ 𝐴 ) = ( ◡ ( sin ↾ ( - ( π / 2 ) [,] ( π / 2 ) ) ) ‘ 𝐴 ) )
14	13 5	eqeltrd	⊢ ( 𝐴 ∈ ( - 1 [,] 1 ) → ( arcsin ‘ 𝐴 ) ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) )