Definition df-sqrt 13215

Description: Define a function whose value is the square root of a complex number. Since ( y ^ 2 ) = x iff ( -u y ^ 2 ) = x, we ensure uniqueness by restricting the range to numbers with positive real part, or numbers with 0 real part and nonnegative imaginary part. A description can be found under "Principal square root of a complex number" at http://en.wikipedia.org/wiki/Square_root. The square root symbol was introduced in 1525 by Christoff Rudolff.

See sqrtcl 13341 for its closure, sqrtval 13217 for its value, sqrtth 13344 and sqsqrti 13355 for its relationship to squares, and sqrt11i 13364 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.)

Assertion

Ref	Expression
df-sqrt	|- sqr = ( x e. CC |-> ( iota_ y e. CC ( ( y ^ 2 ) = x /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) )

Distinct variable group:   x, y

Detailed syntax breakdown of Definition df-sqrt

Step	Hyp	Ref	Expression
1		csqrt 13213	. 2 class sqr
2		vx	. . 3 setvar x
3		cc 9519	. . 3 class CC
4		vy	. . . . . . . 8 setvar y
5	4	cv 1404	. . . . . . 7 class y
6		c2 10625	. . . . . . 7 class 2
7		cexp 12208	. . . . . . 7 class ^
8	5, 6, 7	co 6277	. . . . . 6 class ( y ^ 2 )
9	2	cv 1404	. . . . . 6 class x
10	8, 9	wceq 1405	. . . . 5 wff ( y ^ 2 ) = x
11		cc0 9521	. . . . . 6 class 0
12		cre 13077	. . . . . . 7 class Re
13	5, 12	cfv 5568	. . . . . 6 class ( Re ` y )
14		cle 9658	. . . . . 6 class <_
15	11, 13, 14	wbr 4394	. . . . 5 wff 0 <_ ( Re ` y )
16		ci 9523	. . . . . . 7 class _i
17		cmul 9526	. . . . . . 7 class x.
18	16, 5, 17	co 6277	. . . . . 6 class ( _i x. y )
19		crp 11264	. . . . . 6 class RR+
20	18, 19	wnel 2599	. . . . 5 wff ( _i x. y ) e/ RR+
21	10, 15, 20	w3a 974	. . . 4 wff ( ( y ^ 2 ) = x /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ )
22	21, 4, 3	crio 6238	. . 3 class ( iota_ y e. CC ( ( y ^ 2 ) = x /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) )
23	2, 3, 22	cmpt 4452	. 2 class ( x e. CC |-> ( iota_ y e. CC ( ( y ^ 2 ) = x /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) )
24	1, 23	wceq 1405	1 wff sqr = ( x e. CC |-> ( iota_ y e. CC ( ( y ^ 2 ) = x /\ 0 <_ ( Re ` y ) /\ ( _i x. y ) e/ RR+ ) ) )

This definition is referenced by:  sqrtval  13217  sqrtf  13343