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

Definition df-sqr 11810
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 11935 for its closure, sqrval 11812 for its value, sqrth 11938 and sqsqri 11949 for its relationship to squares, and sqr11i 11958 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 11808 . 2  class  sqr
2 vx . . 3  set  x
3 cc 8822 . . 3  class  CC
4 vy . . . . . . . 8  set  y
54cv 1641 . . . . . . 7  class  y
6 c2 9882 . . . . . . 7  class  2
7 cexp 11194 . . . . . . 7  class  ^
85, 6, 7co 5942 . . . . . 6  class  ( y ^ 2 )
92cv 1641 . . . . . 6  class  x
108, 9wceq 1642 . . . . 5  wff  ( y ^ 2 )  =  x
11 cc0 8824 . . . . . 6  class  0
12 cre 11672 . . . . . . 7  class  Re
135, 12cfv 5334 . . . . . 6  class  ( Re
`  y )
14 cle 8955 . . . . . 6  class  <_
1511, 13, 14wbr 4102 . . . . 5  wff  0  <_  ( Re `  y
)
16 ci 8826 . . . . . . 7  class  _i
17 cmul 8829 . . . . . . 7  class  x.
1816, 5, 17co 5942 . . . . . 6  class  ( _i  x.  y )
19 crp 10443 . . . . . 6  class  RR+
2018, 19wnel 2522 . . . . 5  wff  ( _i  x.  y )  e/  RR+
2110, 15, 20w3a 934 . . . 4  wff  ( ( y ^ 2 )  =  x  /\  0  <_  ( Re `  y
)  /\  ( _i  x.  y )  e/  RR+ )
2221, 4, 3crio 6381 . . 3  class  ( iota_ y  e.  CC ( ( y ^ 2 )  =  x  /\  0  <_  ( Re `  y
)  /\  ( _i  x.  y )  e/  RR+ )
)
232, 3, 22cmpt 4156 . 2  class  ( x  e.  CC  |->  ( iota_ y  e.  CC ( ( y ^ 2 )  =  x  /\  0  <_  ( Re `  y
)  /\  ( _i  x.  y )  e/  RR+ )
) )
241, 23wceq 1642 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  11812  sqrf  11937
  Copyright terms: Public domain W3C validator