df-sqrt - Metamath Proof Explorer

	Metamath Proof Explorer		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > df-sqrt		Structured version Visualization version Unicode version

Definition df-sqrt 13975

Description: Define a function whose value is the square root of a complex number. For example,

(ex-sqrt 27311).

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

**Assertion**
Ref	Expression
df-sqrt	$/\$ $/\$

Distinct variable group:

**Detailed syntax breakdown of Definition df-sqrt**
Step	Hyp	Ref	Expression
1		csqrt 13973	. 2
2		vx	. . 3
3		cc 9934	. . 3
4		vy	. . . . . . . 8
5	4	cv 1482	. . . . . . 7
6		c2 11070	. . . . . . 7
7		cexp 12860	. . . . . . 7
8	5, 6, 7	co 6650	. . . . . 6
9	2	cv 1482	. . . . . 6
10	8, 9	wceq 1483	. . . . 5
11		cc0 9936	. . . . . 6
12		cre 13837	. . . . . . 7
13	5, 12	cfv 5888	. . . . . 6
14		cle 10075	. . . . . 6
15	11, 13, 14	wbr 4653	. . . . 5
16		ci 9938	. . . . . . 7
17		cmul 9941	. . . . . . 7
18	16, 5, 17	co 6650	. . . . . 6
19		crp 11832	. . . . . 6
20	18, 19	wnel 2897	. . . . 5
21	10, 15, 20	w3a 1037	. . . 4 $/\$ $/\$
22	21, 4, 3	crio 6610	. . 3 $/\$ $/\$
23	2, 3, 22	cmpt 4729	. 2 $/\$ $/\$
24	1, 23	wceq 1483	1 $/\$ $/\$

Colors of variables: wff setvar class

This definition is referenced by: sqrtval 13977 sqrtf 14103

W3C validator