Metamath Proof Explorer


Theorem sinasin

Description: The arcsine function is an inverse to sin . This is the main property that justifies the notation arcsin or sin ^ -u 1 . Because sin is not an injection, the other converse identity asinsin is only true under limited circumstances. (Contributed by Mario Carneiro, 1-Apr-2015)

Ref Expression
Assertion sinasin A sin arcsin A = A

Proof

Step Hyp Ref Expression
1 asincl A arcsin A
2 sinval arcsin A sin arcsin A = e i arcsin A e i arcsin A 2 i
3 1 2 syl A sin arcsin A = e i arcsin A e i arcsin A 2 i
4 ax-icn i
5 mulcl i A i A
6 4 5 mpan A i A
7 6 negcld A i A
8 ax-1cn 1
9 sqcl A A 2
10 subcl 1 A 2 1 A 2
11 8 9 10 sylancr A 1 A 2
12 11 sqrtcld A 1 A 2
13 6 7 12 pnpcan2d A i A + 1 A 2 - - i A + 1 A 2 = i A i A
14 efiasin A e i arcsin A = i A + 1 A 2
15 mulneg12 i arcsin A i arcsin A = i arcsin A
16 4 1 15 sylancr A i arcsin A = i arcsin A
17 asinneg A arcsin A = arcsin A
18 17 oveq2d A i arcsin A = i arcsin A
19 16 18 eqtr4d A i arcsin A = i arcsin A
20 19 fveq2d A e i arcsin A = e i arcsin A
21 negcl A A
22 efiasin A e i arcsin A = i A + 1 A 2
23 21 22 syl A e i arcsin A = i A + 1 A 2
24 mulneg2 i A i A = i A
25 4 24 mpan A i A = i A
26 sqneg A A 2 = A 2
27 26 oveq2d A 1 A 2 = 1 A 2
28 27 fveq2d A 1 A 2 = 1 A 2
29 25 28 oveq12d A i A + 1 A 2 = - i A + 1 A 2
30 20 23 29 3eqtrd A e i arcsin A = - i A + 1 A 2
31 14 30 oveq12d A e i arcsin A e i arcsin A = i A + 1 A 2 - - i A + 1 A 2
32 6 2timesd A 2 i A = i A + i A
33 2cn 2
34 mulass 2 i A 2 i A = 2 i A
35 33 4 34 mp3an12 A 2 i A = 2 i A
36 6 6 subnegd A i A i A = i A + i A
37 32 35 36 3eqtr4d A 2 i A = i A i A
38 13 31 37 3eqtr4d A e i arcsin A e i arcsin A = 2 i A
39 mulcl i arcsin A i arcsin A
40 4 1 39 sylancr A i arcsin A
41 efcl i arcsin A e i arcsin A
42 40 41 syl A e i arcsin A
43 negicn i
44 mulcl i arcsin A i arcsin A
45 43 1 44 sylancr A i arcsin A
46 efcl i arcsin A e i arcsin A
47 45 46 syl A e i arcsin A
48 42 47 subcld A e i arcsin A e i arcsin A
49 id A A
50 2mulicn 2 i
51 50 a1i A 2 i
52 2muline0 2 i 0
53 52 a1i A 2 i 0
54 48 49 51 53 divmul2d A e i arcsin A e i arcsin A 2 i = A e i arcsin A e i arcsin A = 2 i A
55 38 54 mpbird A e i arcsin A e i arcsin A 2 i = A
56 3 55 eqtrd A sin arcsin A = A