This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

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 ) ) )