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

Definition df-sqr 11999
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 12124 for its closure, sqrval 12001 for its value, sqrth 12127 and sqsqri 12138 for its relationship to squares, and sqr11i 12147 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 11997 . 2  class  sqr
2 vx . . 3  set  x
3 cc 8948 . . 3  class  CC
4 vy . . . . . . . 8  set  y
54cv 1648 . . . . . . 7  class  y
6 c2 10009 . . . . . . 7  class  2
7 cexp 11341 . . . . . . 7  class  ^
85, 6, 7co 6044 . . . . . 6  class  ( y ^ 2 )
92cv 1648 . . . . . 6  class  x
108, 9wceq 1649 . . . . 5  wff  ( y ^ 2 )  =  x
11 cc0 8950 . . . . . 6  class  0
12 cre 11861 . . . . . . 7  class  Re
135, 12cfv 5417 . . . . . 6  class  ( Re
`  y )
14 cle 9081 . . . . . 6  class  <_
1511, 13, 14wbr 4176 . . . . 5  wff  0  <_  ( Re `  y
)
16 ci 8952 . . . . . . 7  class  _i
17 cmul 8955 . . . . . . 7  class  x.
1816, 5, 17co 6044 . . . . . 6  class  ( _i  x.  y )
19 crp 10572 . . . . . 6  class  RR+
2018, 19wnel 2572 . . . . 5  wff  ( _i  x.  y )  e/  RR+
2110, 15, 20w3a 936 . . . 4  wff  ( ( y ^ 2 )  =  x  /\  0  <_  ( Re `  y
)  /\  ( _i  x.  y )  e/  RR+ )
2221, 4, 3crio 6505 . . 3  class  ( iota_ y  e.  CC ( ( y ^ 2 )  =  x  /\  0  <_  ( Re `  y
)  /\  ( _i  x.  y )  e/  RR+ )
)
232, 3, 22cmpt 4230 . 2  class  ( x  e.  CC  |->  ( iota_ y  e.  CC ( ( y ^ 2 )  =  x  /\  0  <_  ( Re `  y
)  /\  ( _i  x.  y )  e/  RR+ )
) )
241, 23wceq 1649 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  12001  sqrf  12126
  Copyright terms: Public domain W3C validator