Definition df-sqrt 15187

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

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

See sqrtcl 15313 for its closure, sqrtval 15189 for its value, sqrtth 15316 and sqsqrti 15327 for its relationship to squares, and sqrt11i 15336 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 15185	. 2 class √
2		vx	. . 3 setvar 𝑥
3		cc 11111	. . 3 class ℂ
4		vy	. . . . . . . 8 setvar 𝑦
5	4	cv 1539	. . . . . . 7 class 𝑦
6		c2 12272	. . . . . . 7 class 2
7		cexp 14032	. . . . . . 7 class ↑
8	5, 6, 7	co 7412	. . . . . 6 class (𝑦↑2)
9	2	cv 1539	. . . . . 6 class 𝑥
10	8, 9	wceq 1540	. . . . 5 wff (𝑦↑2) = 𝑥
11		cc0 11113	. . . . . 6 class 0
12		cre 15049	. . . . . . 7 class ℜ
13	5, 12	cfv 6543	. . . . . 6 class (ℜ‘𝑦)
14		cle 11254	. . . . . 6 class ≤
15	11, 13, 14	wbr 5148	. . . . 5 wff 0 ≤ (ℜ‘𝑦)
16		ci 11115	. . . . . . 7 class i
17		cmul 11118	. . . . . . 7 class ·
18	16, 5, 17	co 7412	. . . . . 6 class (i · 𝑦)
19		crp 12979	. . . . . 6 class ℝ+
20	18, 19	wnel 3045	. . . . 5 wff (i · 𝑦) ∉ ℝ+
21	10, 15, 20	w3a 1086	. . . 4 wff ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)
22	21, 4, 3	crio 7367	. . 3 class (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+))
23	2, 3, 22	cmpt 5231	. 2 class (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)))
24	1, 23	wceq 1540	1 wff √ = (𝑥 ∈ ℂ ↦ (℩𝑦 ∈ ℂ ((𝑦↑2) = 𝑥 ∧ 0 ≤ (ℜ‘𝑦) ∧ (i · 𝑦) ∉ ℝ+)))

This definition is referenced by:  sqrtval  15189  sqrtf  15315  cphsscph  25000