Definition df-sqrt

Description: Define a function whose value is the square root of a complex number. For example, ( sqrt2 5 ) = 5 ( ex-sqrt ).

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 for its closure, sqrtval for its value, sqrtth and sqsqrti for its relationship to squares, and sqrt11i for uniqueness. (Contributed by NM, 27-Jul-1999) (Revised by Mario Carneiro, 8-Jul-2013)

	Ref	Expression
Assertion	df-sqrt	⊢ √ = ( 𝑥 ∈ ℂ ↦ ( ℩ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 𝑥 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) )

Detailed syntax breakdown

Step	Hyp	Ref	Expression
0		csqrt	⊢ √
1		vx	⊢ 𝑥
2		cc	⊢ ℂ
3		vy	⊢ 𝑦
4	3	cv	⊢ 𝑦
5		cexp	⊢ ↑
6		c2	⊢ 2
7	4 6 5	co	⊢ ( 𝑦 ↑ 2 )
8	1	cv	⊢ 𝑥
9	7 8	wceq	⊢ ( 𝑦 ↑ 2 ) = 𝑥
10		cc0	⊢ 0
11		cle	⊢ ≤
12		cre	⊢ ℜ
13	4 12	cfv	⊢ ( ℜ ‘ 𝑦 )
14	10 13 11	wbr	⊢ 0 ≤ ( ℜ ‘ 𝑦 )
15		ci	⊢ i
16		cmul	⊢ ·
17	15 4 16	co	⊢ ( i · 𝑦 )
18		crp	⊢ ℝ+
19	17 18	wnel	⊢ ( i · 𝑦 ) ∉ ℝ+
20	9 14 19	w3a	⊢ ( ( 𝑦 ↑ 2 ) = 𝑥 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ )
21	20 3 2	crio	⊢ ( ℩ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 𝑥 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) )
22	1 2 21	cmpt	⊢ ( 𝑥 ∈ ℂ ↦ ( ℩ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 𝑥 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) )
23	0 22	wceq	⊢ √ = ( 𝑥 ∈ ℂ ↦ ( ℩ 𝑦 ∈ ℂ ( ( 𝑦 ↑ 2 ) = 𝑥 ∧ 0 ≤ ( ℜ ‘ 𝑦 ) ∧ ( i · 𝑦 ) ∉ ℝ+ ) ) )