Metamath Proof Explorer

Theorem asinrebnd

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

Ref Expression
Assertion asinrebnd 
|- ( A e. ( -u 1 [,] 1 ) -> ( arcsin ` A ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )

Proof

Step Hyp Ref Expression
1 resinf1o 
 |-  ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 )
2 f1ocnv 
 |-  ( ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 ) -> `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) : ( -u 1 [,] 1 ) -1-1-onto-> ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
3 f1of 
 |-  ( `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) : ( -u 1 [,] 1 ) -1-1-onto-> ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) : ( -u 1 [,] 1 ) --> ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
4 1 2 3 mp2b 
 |-  `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) : ( -u 1 [,] 1 ) --> ( -u ( _pi / 2 ) [,] ( _pi / 2 ) )
5 4 ffvelcdmi 
 |-  ( A e. ( -u 1 [,] 1 ) -> ( `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` A ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
6 5 fvresd 
 |-  ( A e. ( -u 1 [,] 1 ) -> ( ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` ( `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` A ) ) = ( sin ` ( `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` A ) ) )
7 f1ocnvfv2 
 |-  ( ( ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) : ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -1-1-onto-> ( -u 1 [,] 1 ) /\ A e. ( -u 1 [,] 1 ) ) -> ( ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` ( `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` A ) ) = A )
8 1 7 mpan 
 |-  ( A e. ( -u 1 [,] 1 ) -> ( ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` ( `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` A ) ) = A )
9 6 8 eqtr3d 
 |-  ( A e. ( -u 1 [,] 1 ) -> ( sin ` ( `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` A ) ) = A )
10 9 fveq2d 
 |-  ( A e. ( -u 1 [,] 1 ) -> ( arcsin ` ( sin ` ( `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` A ) ) ) = ( arcsin ` A ) )
11 reasinsin 
 |-  ( ( `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` A ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( arcsin ` ( sin ` ( `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` A ) ) ) = ( `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` A ) )
12 5 11 syl 
 |-  ( A e. ( -u 1 [,] 1 ) -> ( arcsin ` ( sin ` ( `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` A ) ) ) = ( `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` A ) )
13 10 12 eqtr3d 
 |-  ( A e. ( -u 1 [,] 1 ) -> ( arcsin ` A ) = ( `' ( sin |` ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) ) ` A ) )
14 13 5 eqeltrd 
 |-  ( A e. ( -u 1 [,] 1 ) -> ( arcsin ` A ) e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )