Definition df-sqrt 15243

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

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 30600. The square root symbol was introduced in 1525 by Christoff Rudolff.

See sqrtcl 15370 for its closure, sqrtval 15245 for its value, sqrtth 15373 and sqsqrti 15384 for its relationship to squares, and sqrt11i 15393 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 15241	. 2 class √
2		vx	. . 3 setvar 𝑥
3		cc 11066	. . 3 class ℂ
4		vy	. . . . . . . 8 setvar 𝑦
5	4	cv 1558	. . . . . . 7 class 𝑦
6		c2 12267	. . . . . . 7 class 2
7		cexp 14069	. . . . . . 7 class ↑
8	5, 6, 7	co 7390	. . . . . 6 class (𝑦↑2)
9	2	cv 1558	. . . . . 6 class 𝑥
10	8, 9	wceq 1559	. . . . 5 wff (𝑦↑2) = 𝑥
11		cc0 11068	. . . . . 6 class 0
12		cre 15105	. . . . . . 7 class ℜ
13	5, 12	cfv 6515	. . . . . 6 class (ℜ‘𝑦)
14		cle 11212	. . . . . 6 class ≤
15	11, 13, 14	wbr 5099	. . . . 5 wff 0 ≤ (ℜ‘𝑦)
16		ci 11070	. . . . . . 7 class i
17		cmul 11073	. . . . . . 7 class ·
18	16, 5, 17	co 7390	. . . . . 6 class (i · 𝑦)
19		crp 12988	. . . . . 6 class ℝ+
20	18, 19	wnel 3060	. . . . 5 wff (i · 𝑦) ∉ ℝ+
21	10, 15, 20	w3a 1097	. . . 4 wff ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)
22	21, 4, 3	crio 7346	. . 3 class (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))
23	2, 3, 22	cmpt 5180	. 2 class (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)))
24	1, 23	wceq 1559	1 wff √ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)))

This definition is referenced by:  sqrtval  15245  sqrtf  15372  cphsscph  25291