Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > df-asin | Structured version Visualization version GIF version |
Description: Define the arcsine function. Because sin is not a one-to-one function, the literal inverse ◡sin is not a function. Rather than attempt to find the right domain on which to restrict sin in order to get a total function, we just define it in terms of log, which we already know is total (except at 0). There are branch points at -1 and 1 (at which the function is defined), and branch cuts along the real line not between -1 and 1, which is to say (-∞, -1) ∪ (1, +∞). (Contributed by Mario Carneiro, 31-Mar-2015.) |
Ref | Expression |
---|---|
df-asin | ⊢ arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | casin 25750 | . 2 class arcsin | |
2 | vx | . . 3 setvar 𝑥 | |
3 | cc 10732 | . . 3 class ℂ | |
4 | ci 10736 | . . . . 5 class i | |
5 | 4 | cneg 11068 | . . . 4 class -i |
6 | 2 | cv 1542 | . . . . . . 7 class 𝑥 |
7 | cmul 10739 | . . . . . . 7 class · | |
8 | 4, 6, 7 | co 7218 | . . . . . 6 class (i · 𝑥) |
9 | c1 10735 | . . . . . . . 8 class 1 | |
10 | c2 11890 | . . . . . . . . 9 class 2 | |
11 | cexp 13640 | . . . . . . . . 9 class ↑ | |
12 | 6, 10, 11 | co 7218 | . . . . . . . 8 class (𝑥↑2) |
13 | cmin 11067 | . . . . . . . 8 class − | |
14 | 9, 12, 13 | co 7218 | . . . . . . 7 class (1 − (𝑥↑2)) |
15 | csqrt 14801 | . . . . . . 7 class √ | |
16 | 14, 15 | cfv 6385 | . . . . . 6 class (√‘(1 − (𝑥↑2))) |
17 | caddc 10737 | . . . . . 6 class + | |
18 | 8, 16, 17 | co 7218 | . . . . 5 class ((i · 𝑥) + (√‘(1 − (𝑥↑2)))) |
19 | clog 25448 | . . . . 5 class log | |
20 | 18, 19 | cfv 6385 | . . . 4 class (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))) |
21 | 5, 20, 7 | co 7218 | . . 3 class (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))) |
22 | 2, 3, 21 | cmpt 5140 | . 2 class (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) |
23 | 1, 22 | wceq 1543 | 1 wff arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))) |
Colors of variables: wff setvar class |
This definition is referenced by: asinf 25760 asinval 25770 dvasin 35603 |
Copyright terms: Public domain | W3C validator |