Definition df-asin 26908

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.)

Assertion

Ref	Expression
df-asin	⊢ arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))

Detailed syntax breakdown of Definition df-asin

Step	Hyp	Ref	Expression
1		casin 26905	. 2 class arcsin
2		vx	. . 3 setvar 𝑥
3		cc 11153	. . 3 class ℂ
4		ci 11157	. . . . 5 class i
5	4	cneg 11493	. . . 4 class -i
6	2	cv 1539	. . . . . . 7 class 𝑥
7		cmul 11160	. . . . . . 7 class ·
8	4, 6, 7	co 7431	. . . . . 6 class (i · 𝑥)
9		c1 11156	. . . . . . . 8 class 1
10		c2 12321	. . . . . . . . 9 class 2
11		cexp 14102	. . . . . . . . 9 class ↑
12	6, 10, 11	co 7431	. . . . . . . 8 class (𝑥↑2)
13		cmin 11492	. . . . . . . 8 class −
14	9, 12, 13	co 7431	. . . . . . 7 class (1 − (𝑥↑2))
15		csqrt 15272	. . . . . . 7 class √
16	14, 15	cfv 6561	. . . . . 6 class (√‘(1 − (𝑥↑2)))
17		caddc 11158	. . . . . 6 class +
18	8, 16, 17	co 7431	. . . . 5 class ((i · 𝑥) + (√‘(1 − (𝑥↑2))))
19		clog 26596	. . . . 5 class log
20	18, 19	cfv 6561	. . . 4 class (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))
21	5, 20, 7	co 7431	. . 3 class (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2))))))
22	2, 3, 21	cmpt 5225	. 2 class (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))
23	1, 22	wceq 1540	1 wff arcsin = (𝑥 ∈ ℂ ↦ (-i · (log‘((i · 𝑥) + (√‘(1 − (𝑥↑2)))))))

This definition is referenced by:  asinf  26915  asinval  26925  dvasin  37711