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

Definition df-sqr 11995
 Description: Define a function whose value is the square root of a complex number. 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 sqrcl 12120 for its closure, sqrval 11997 for its value, sqrth 12123 and sqsqri 12134 for its relationship to squares, and sqr11i 12143 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.)
Assertion
Ref Expression
df-sqr
Distinct variable group:   ,

Detailed syntax breakdown of Definition df-sqr
StepHypRef Expression
1 csqr 11993 . 2
2 vx . . 3
3 cc 8944 . . 3
4 vy . . . . . . . 8
54cv 1648 . . . . . . 7
6 c2 10005 . . . . . . 7
7 cexp 11337 . . . . . . 7
85, 6, 7co 6040 . . . . . 6
92cv 1648 . . . . . 6
108, 9wceq 1649 . . . . 5
11 cc0 8946 . . . . . 6
12 cre 11857 . . . . . . 7
135, 12cfv 5413 . . . . . 6
14 cle 9077 . . . . . 6
1511, 13, 14wbr 4172 . . . . 5
16 ci 8948 . . . . . . 7
17 cmul 8951 . . . . . . 7
1816, 5, 17co 6040 . . . . . 6
19 crp 10568 . . . . . 6
2018, 19wnel 2568 . . . . 5
2110, 15, 20w3a 936 . . . 4
2221, 4, 3crio 6501 . . 3
232, 3, 22cmpt 4226 . 2
241, 23wceq 1649 1
 Colors of variables: wff set class This definition is referenced by:  sqrval  11997  sqrf  12122
 Copyright terms: Public domain W3C validator