Metamath Proof Explorer

Theorem asinrebnd

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

Ref Expression
Assertion asinrebnd ⊢ A ∈ − 1 1 → arcsin ⁡ A ∈ − π 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-1 onto − π 2 π 2
3 f1of ⊢ sin ↾ − π 2 π 2 -1 : − 1 1 ⟶ 1-1 onto − π 2 π 2 → sin ↾ − π 2 π 2 -1 : − 1 1 ⟶ − π 2 π 2
4 1 2 3 mp2b ⊢ sin ↾ − π 2 π 2 -1 : − 1 1 ⟶ − π 2 π 2
5 4 ffvelrni ⊢ A ∈ − 1 1 → sin ↾ − π 2 π 2 -1 ⁡ A ∈ − π 2 π 2
6 5 fvresd ⊢ A ∈ − 1 1 → sin ↾ − π 2 π 2 ⁡ sin ↾ − π 2 π 2 -1 ⁡ A = sin ⁡ sin ↾ − π 2 π 2 -1 ⁡ A
7 f1ocnvfv2 ⊢ sin ↾ − π 2 π 2 : − π 2 π 2 ⟶ 1-1 onto − 1 1 ∧ A ∈ − 1 1 → sin ↾ − π 2 π 2 ⁡ sin ↾ − π 2 π 2 -1 ⁡ A = A
8 1 7 mpan ⊢ A ∈ − 1 1 → sin ↾ − π 2 π 2 ⁡ sin ↾ − π 2 π 2 -1 ⁡ A = A
9 6 8 eqtr3d ⊢ A ∈ − 1 1 → sin ⁡ sin ↾ − π 2 π 2 -1 ⁡ A = A
10 9 fveq2d ⊢ A ∈ − 1 1 → arcsin ⁡ sin ⁡ sin ↾ − π 2 π 2 -1 ⁡ A = arcsin ⁡ A
11 reasinsin ⊢ sin ↾ − π 2 π 2 -1 ⁡ A ∈ − π 2 π 2 → arcsin ⁡ sin ⁡ sin ↾ − π 2 π 2 -1 ⁡ A = sin ↾ − π 2 π 2 -1 ⁡ A
12 5 11 syl ⊢ A ∈ − 1 1 → arcsin ⁡ sin ⁡ sin ↾ − π 2 π 2 -1 ⁡ A = sin ↾ − π 2 π 2 -1 ⁡ A
13 10 12 eqtr3d ⊢ A ∈ − 1 1 → arcsin ⁡ A = sin ↾ − π 2 π 2 -1 ⁡ A
14 13 5 eqeltrd ⊢ A ∈ − 1 1 → arcsin ⁡ A ∈ − π 2 π 2