Definition df-sqrt 15170

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

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

See sqrtcl 15297 for its closure, sqrtval 15172 for its value, sqrtth 15300 and sqsqrti 15311 for its relationship to squares, and sqrt11i 15320 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 15168	. 2 class √
2		vx	. . 3 setvar 𝑥
3		cc 11036	. . 3 class ℂ
4		vy	. . . . . . . 8 setvar 𝑦
5	4	cv 1541	. . . . . . 7 class 𝑦
6		c2 12212	. . . . . . 7 class 2
7		cexp 13996	. . . . . . 7 class ↑
8	5, 6, 7	co 7368	. . . . . 6 class (𝑦↑2)
9	2	cv 1541	. . . . . 6 class 𝑥
10	8, 9	wceq 1542	. . . . 5 wff (𝑦↑2) = 𝑥
11		cc0 11038	. . . . . 6 class 0
12		cre 15032	. . . . . . 7 class ℜ
13	5, 12	cfv 6500	. . . . . 6 class (ℜ‘𝑦)
14		cle 11179	. . . . . 6 class ≤
15	11, 13, 14	wbr 5100	. . . . 5 wff 0 ≤ (ℜ‘𝑦)
16		ci 11040	. . . . . . 7 class i
17		cmul 11043	. . . . . . 7 class ·
18	16, 5, 17	co 7368	. . . . . 6 class (i · 𝑦)
19		crp 12917	. . . . . 6 class ℝ+
20	18, 19	wnel 3037	. . . . 5 wff (i · 𝑦) ∉ ℝ+
21	10, 15, 20	w3a 1087	. . . 4 wff ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)
22	21, 4, 3	crio 7324	. . 3 class (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))
23	2, 3, 22	cmpt 5181	. 2 class (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)))
24	1, 23	wceq 1542	1 wff √ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)))

This definition is referenced by:  sqrtval  15172  sqrtf  15299  cphsscph  25219