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 ‘ 𝐴 ) ) = 𝐴 )