Metamath Proof Explorer

Theorem asinrebnd

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

Ref Expression
Assertion asinrebnd ⊢A∈−11→arcsin⁡A∈−π2π2

Proof

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