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 ( 𝐴 ∈ ( - ( π / 2 ) [,] ( π / 2 ) ) → ( arcsin ‘ ( sin ‘ 𝐴 ) ) = 𝐴 )

Proof

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