Metamath Proof Explorer

Theorem reasinsin

Description: The arcsine function composed with sin is equal to the identity. (Contributed by Mario Carneiro, 2-Apr-2015)

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

Proof

Step Hyp Ref Expression
1 neghalfpire 
 |-  -u ( _pi / 2 ) e. RR
2 1 rexri 
 |-  -u ( _pi / 2 ) e. RR*
3 halfpire 
 |-  ( _pi / 2 ) e. RR
4 3 rexri 
 |-  ( _pi / 2 ) e. RR*
5 pirp 
 |-  _pi e. RR+
6 rphalfcl 
 |-  ( _pi e. RR+ -> ( _pi / 2 ) e. RR+ )
7 5 6 ax-mp 
 |-  ( _pi / 2 ) e. RR+
8 rpgt0 
 |-  ( ( _pi / 2 ) e. RR+ -> 0 < ( _pi / 2 ) )
9 7 8 ax-mp 
 |-  0 < ( _pi / 2 )
10 lt0neg2 
 |-  ( ( _pi / 2 ) e. RR -> ( 0 < ( _pi / 2 ) <-> -u ( _pi / 2 ) < 0 ) )
11 3 10 ax-mp 
 |-  ( 0 < ( _pi / 2 ) <-> -u ( _pi / 2 ) < 0 )
12 9 11 mpbi 
 |-  -u ( _pi / 2 ) < 0
13 0re 
 |-  0 e. RR
14 1 13 3 lttri 
 |-  ( ( -u ( _pi / 2 ) < 0 /\ 0 < ( _pi / 2 ) ) -> -u ( _pi / 2 ) < ( _pi / 2 ) )
15 12 9 14 mp2an 
 |-  -u ( _pi / 2 ) < ( _pi / 2 )
16 1 3 15 ltleii 
 |-  -u ( _pi / 2 ) <_ ( _pi / 2 )
17 prunioo 
 |-  ( ( -u ( _pi / 2 ) e. RR* /\ ( _pi / 2 ) e. RR* /\ -u ( _pi / 2 ) <_ ( _pi / 2 ) ) -> ( ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) u. { -u ( _pi / 2 ) , ( _pi / 2 ) } ) = ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
18 2 4 16 17 mp3an 
 |-  ( ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) u. { -u ( _pi / 2 ) , ( _pi / 2 ) } ) = ( -u ( _pi / 2 ) [,] ( _pi / 2 ) )
19 18 eleq2i 
 |-  ( A e. ( ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) u. { -u ( _pi / 2 ) , ( _pi / 2 ) } ) <-> A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) )
20 elun 
 |-  ( A e. ( ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) u. { -u ( _pi / 2 ) , ( _pi / 2 ) } ) <-> ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) \/ A e. { -u ( _pi / 2 ) , ( _pi / 2 ) } ) )
21 19 20 bitr3i 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) <-> ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) \/ A e. { -u ( _pi / 2 ) , ( _pi / 2 ) } ) )
22 elioore 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> A e. RR )
23 22 recnd 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> A e. CC )
24 22 rered 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( Re ` A ) = A )
25 id 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
26 24 25 eqeltrd 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) )
27 asinsin 
 |-  ( ( A e. CC /\ ( Re ` A ) e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) ) -> ( arcsin ` ( sin ` A ) ) = A )
28 23 26 27 syl2anc 
 |-  ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) -> ( arcsin ` ( sin ` A ) ) = A )
29 elpri 
 |-  ( A e. { -u ( _pi / 2 ) , ( _pi / 2 ) } -> ( A = -u ( _pi / 2 ) \/ A = ( _pi / 2 ) ) )
30 ax-1cn 
 |-  1 e. CC
31 asinneg 
 |-  ( 1 e. CC -> ( arcsin ` -u 1 ) = -u ( arcsin ` 1 ) )
32 30 31 ax-mp 
 |-  ( arcsin ` -u 1 ) = -u ( arcsin ` 1 )
33 asin1 
 |-  ( arcsin ` 1 ) = ( _pi / 2 )
34 33 negeqi 
 |-  -u ( arcsin ` 1 ) = -u ( _pi / 2 )
35 32 34 eqtri 
 |-  ( arcsin ` -u 1 ) = -u ( _pi / 2 )
36 fveq2 
 |-  ( A = -u ( _pi / 2 ) -> ( sin ` A ) = ( sin ` -u ( _pi / 2 ) ) )
37 3 recni 
 |-  ( _pi / 2 ) e. CC
38 sinneg 
 |-  ( ( _pi / 2 ) e. CC -> ( sin ` -u ( _pi / 2 ) ) = -u ( sin ` ( _pi / 2 ) ) )
39 37 38 ax-mp 
 |-  ( sin ` -u ( _pi / 2 ) ) = -u ( sin ` ( _pi / 2 ) )
40 sinhalfpi 
 |-  ( sin ` ( _pi / 2 ) ) = 1
41 40 negeqi 
 |-  -u ( sin ` ( _pi / 2 ) ) = -u 1
42 39 41 eqtri 
 |-  ( sin ` -u ( _pi / 2 ) ) = -u 1
43 36 42 eqtrdi 
 |-  ( A = -u ( _pi / 2 ) -> ( sin ` A ) = -u 1 )
44 43 fveq2d 
 |-  ( A = -u ( _pi / 2 ) -> ( arcsin ` ( sin ` A ) ) = ( arcsin ` -u 1 ) )
45 id 
 |-  ( A = -u ( _pi / 2 ) -> A = -u ( _pi / 2 ) )
46 35 44 45 3eqtr4a 
 |-  ( A = -u ( _pi / 2 ) -> ( arcsin ` ( sin ` A ) ) = A )
47 fveq2 
 |-  ( A = ( _pi / 2 ) -> ( sin ` A ) = ( sin ` ( _pi / 2 ) ) )
48 47 40 eqtrdi 
 |-  ( A = ( _pi / 2 ) -> ( sin ` A ) = 1 )
49 48 fveq2d 
 |-  ( A = ( _pi / 2 ) -> ( arcsin ` ( sin ` A ) ) = ( arcsin ` 1 ) )
50 id 
 |-  ( A = ( _pi / 2 ) -> A = ( _pi / 2 ) )
51 33 49 50 3eqtr4a 
 |-  ( A = ( _pi / 2 ) -> ( arcsin ` ( sin ` A ) ) = A )
52 46 51 jaoi 
 |-  ( ( A = -u ( _pi / 2 ) \/ A = ( _pi / 2 ) ) -> ( arcsin ` ( sin ` A ) ) = A )
53 29 52 syl 
 |-  ( A e. { -u ( _pi / 2 ) , ( _pi / 2 ) } -> ( arcsin ` ( sin ` A ) ) = A )
54 28 53 jaoi 
 |-  ( ( A e. ( -u ( _pi / 2 ) (,) ( _pi / 2 ) ) \/ A e. { -u ( _pi / 2 ) , ( _pi / 2 ) } ) -> ( arcsin ` ( sin ` A ) ) = A )
55 21 54 sylbi 
 |-  ( A e. ( -u ( _pi / 2 ) [,] ( _pi / 2 ) ) -> ( arcsin ` ( sin ` A ) ) = A )