Definition df-sqrt 14458

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

Since (𝑦↑2) = 𝑥 iff (-𝑦↑2) = 𝑥, 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 14585 for its closure, sqrtval 14460 for its value, sqrtth 14588 and sqsqrti 14599 for its relationship to squares, and sqrt11i 14608 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.)

Assertion

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

Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-sqrt

Step	Hyp	Ref	Expression
1		csqrt 14456	. 2 class √
2		vx	. . 3 setvar 𝑥
3		cc 10335	. . 3 class ℂ
4		vy	. . . . . . . 8 setvar 𝑦
5	4	cv 1506	. . . . . . 7 class 𝑦
6		c2 11498	. . . . . . 7 class 2
7		cexp 13247	. . . . . . 7 class ↑
8	5, 6, 7	co 6978	. . . . . 6 class (𝑦↑2)
9	2	cv 1506	. . . . . 6 class 𝑥
10	8, 9	wceq 1507	. . . . 5 wff (𝑦↑2) = 𝑥
11		cc0 10337	. . . . . 6 class 0
12		cre 14320	. . . . . . 7 class ℜ
13	5, 12	cfv 6190	. . . . . 6 class (ℜ‘𝑦)
14		cle 10477	. . . . . 6 class ≤
15	11, 13, 14	wbr 4930	. . . . 5 wff 0 ≤ (ℜ‘𝑦)
16		ci 10339	. . . . . . 7 class i
17		cmul 10342	. . . . . . 7 class ·
18	16, 5, 17	co 6978	. . . . . 6 class (i · 𝑦)
19		crp 12207	. . . . . 6 class ℝ+
20	18, 19	wnel 3073	. . . . 5 wff (i · 𝑦) ∉ ℝ+
21	10, 15, 20	w3a 1068	. . . 4 wff ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)
22	21, 4, 3	crio 6938	. . 3 class (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))
23	2, 3, 22	cmpt 5009	. 2 class (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)))
24	1, 23	wceq 1507	1 wff √ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)))

This definition is referenced by:  sqrtval  14460  sqrtf  14587  cphsscph  23560