df-asin - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-asin		Structured version Visualization version Unicode version

Definition df-asin 24592

Description: Define the arcsine function. Because

is not a one-to-one function, the literal inverse

is not a function. Rather than attempt to find the right domain on which to restrict

in order to get a total function, we just define it in terms of

, which we already know is total (except at

). There are branch points at

and

(at which the function is defined), and branch cuts along the real line not between

and

, which is to say

. (Contributed by Mario Carneiro, 31-Mar-2015.)

**Assertion**
Ref	Expression
df-asin	arcsin

**Detailed syntax breakdown of Definition df-asin**
Step	Hyp	Ref	Expression
1		casin 24589	. 2 arcsin
2		vx	. . 3
3		cc 9934	. . 3
4		ci 9938	. . . . 5
5	4	cneg 10267	. . . 4
6	2	cv 1482	. . . . . . 7
7		cmul 9941	. . . . . . 7
8	4, 6, 7	co 6650	. . . . . 6
9		c1 9937	. . . . . . . 8
10		c2 11070	. . . . . . . . 9
11		cexp 12860	. . . . . . . . 9
12	6, 10, 11	co 6650	. . . . . . . 8
13		cmin 10266	. . . . . . . 8
14	9, 12, 13	co 6650	. . . . . . 7
15		csqrt 13973	. . . . . . 7
16	14, 15	cfv 5888	. . . . . 6
17		caddc 9939	. . . . . 6
18	8, 16, 17	co 6650	. . . . 5
19		clog 24301	. . . . 5
20	18, 19	cfv 5888	. . . 4
21	5, 20, 7	co 6650	. . 3
22	2, 3, 21	cmpt 4729	. 2
23	1, 22	wceq 1483	1 arcsin

Colors of variables: wff setvar class

This definition is referenced by: asinf 24599 asinval 24609 dvasin 33496