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

Definition df-sqr 12071
Description: Define a function whose value is the square root of a complex number. Since  ( y ^
2 )  =  x iff  ( -u y ^
2 )  =  x, 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 12196 for its closure, sqrval 12073 for its value, sqrth 12199 and sqsqri 12210 for its relationship to squares, and sqr11i 12219 for uniqueness. (Contributed by NM, 27-Jul-1999.) (Revised by Mario Carneiro, 8-Jul-2013.)

Assertion
Ref Expression
df-sqr  |-  sqr  =  ( x  e.  CC  |->  ( iota_ y  e.  CC ( ( y ^
2 )  =  x  /\  0  <_  (
Re `  y )  /\  ( _i  x.  y
)  e/  RR+ ) ) )
Distinct variable group:    x, y

Detailed syntax breakdown of Definition df-sqr
StepHypRef Expression
1 csqr 12069 . 2  class  sqr
2 vx . . 3  set  x
3 cc 9019 . . 3  class  CC
4 vy . . . . . . . 8  set  y
54cv 1652 . . . . . . 7  class  y
6 c2 10080 . . . . . . 7  class  2
7 cexp 11413 . . . . . . 7  class  ^
85, 6, 7co 6110 . . . . . 6  class  ( y ^ 2 )
92cv 1652 . . . . . 6  class  x
108, 9wceq 1653 . . . . 5  wff  ( y ^ 2 )  =  x
11 cc0 9021 . . . . . 6  class  0
12 cre 11933 . . . . . . 7  class  Re
135, 12cfv 5483 . . . . . 6  class  ( Re
`  y )
14 cle 9152 . . . . . 6  class  <_
1511, 13, 14wbr 4237 . . . . 5  wff  0  <_  ( Re `  y
)
16 ci 9023 . . . . . . 7  class  _i
17 cmul 9026 . . . . . . 7  class  x.
1816, 5, 17co 6110 . . . . . 6  class  ( _i  x.  y )
19 crp 10643 . . . . . 6  class  RR+
2018, 19wnel 2606 . . . . 5  wff  ( _i  x.  y )  e/  RR+
2110, 15, 20w3a 937 . . . 4  wff  ( ( y ^ 2 )  =  x  /\  0  <_  ( Re `  y
)  /\  ( _i  x.  y )  e/  RR+ )
2221, 4, 3crio 6571 . . 3  class  ( iota_ y  e.  CC ( ( y ^ 2 )  =  x  /\  0  <_  ( Re `  y
)  /\  ( _i  x.  y )  e/  RR+ )
)
232, 3, 22cmpt 4291 . 2  class  ( x  e.  CC  |->  ( iota_ y  e.  CC ( ( y ^ 2 )  =  x  /\  0  <_  ( Re `  y
)  /\  ( _i  x.  y )  e/  RR+ )
) )
241, 23wceq 1653 1  wff  sqr  =  ( x  e.  CC  |->  ( iota_ y  e.  CC ( ( y ^
2 )  =  x  /\  0  <_  (
Re `  y )  /\  ( _i  x.  y
)  e/  RR+ ) ) )
Colors of variables: wff set class
This definition is referenced by:  sqrval  12073  sqrf  12198
  Copyright terms: Public domain W3C validator