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 π 2 π 2 arcsin sin A = A

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 A π 2 π 2 π 2 π 2 A π 2 π 2
20 elun A π 2 π 2 π 2 π 2 A π 2 π 2 A π 2 π 2
21 19 20 bitr3i A π 2 π 2 A π 2 π 2 A π 2 π 2
22 elioore A π 2 π 2 A
23 22 recnd A π 2 π 2 A
24 22 rered A π 2 π 2 A = A
25 id A π 2 π 2 A π 2 π 2
26 24 25 eqeltrd A π 2 π 2 A π 2 π 2
27 asinsin A A π 2 π 2 arcsin sin A = A
28 23 26 27 syl2anc A π 2 π 2 arcsin sin A = A
29 elpri A π 2 π 2 A = π 2 A = π 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 A = π 2 sin A = 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 A = π 2 sin A = 1
44 43 fveq2d A = π 2 arcsin sin A = arcsin 1
45 id A = π 2 A = π 2
46 35 44 45 3eqtr4a A = π 2 arcsin sin A = A
47 fveq2 A = π 2 sin A = sin π 2
48 47 40 eqtrdi A = π 2 sin A = 1
49 48 fveq2d A = π 2 arcsin sin A = arcsin 1
50 id A = π 2 A = π 2
51 33 49 50 3eqtr4a A = π 2 arcsin sin A = A
52 46 51 jaoi A = π 2 A = π 2 arcsin sin A = A
53 29 52 syl A π 2 π 2 arcsin sin A = A
54 28 53 jaoi A π 2 π 2 A π 2 π 2 arcsin sin A = A
55 21 54 sylbi A π 2 π 2 arcsin sin A = A