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

Definition df-sqr 11715
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 11840 for its closure, sqrval 11717 for its value, sqrth 11843 and sqsqri 11854 for its relationship to squares, and sqr11i 11863 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 11713 . 2  class  sqr
2 vx . . 3  set  x
3 cc 8731 . . 3  class  CC
4 vy . . . . . . . 8  set  y
54cv 1623 . . . . . . 7  class  y
6 c2 9791 . . . . . . 7  class  2
7 cexp 11099 . . . . . . 7  class  ^
85, 6, 7co 5820 . . . . . 6  class  ( y ^ 2 )
92cv 1623 . . . . . 6  class  x
108, 9wceq 1624 . . . . 5  wff  ( y ^ 2 )  =  x
11 cc0 8733 . . . . . 6  class  0
12 cre 11577 . . . . . . 7  class  Re
135, 12cfv 5222 . . . . . 6  class  ( Re
`  y )
14 cle 8864 . . . . . 6  class  <_
1511, 13, 14wbr 4025 . . . . 5  wff  0  <_  ( Re `  y
)
16 ci 8735 . . . . . . 7  class  _i
17 cmul 8738 . . . . . . 7  class  x.
1816, 5, 17co 5820 . . . . . 6  class  ( _i  x.  y )
19 crp 10350 . . . . . 6  class  RR+
2018, 19wnel 2449 . . . . 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 6291 . . 3  class  ( iota_ y  e.  CC ( ( y ^ 2 )  =  x  /\  0  <_  ( Re `  y
)  /\  ( _i  x.  y )  e/  RR+ )
)
232, 3, 22cmpt 4079 . 2  class  ( x  e.  CC  |->  ( iota_ y  e.  CC ( ( y ^ 2 )  =  x  /\  0  <_  ( Re `  y
)  /\  ( _i  x.  y )  e/  RR+ )
) )
241, 23wceq 1624 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  11717  sqrf  11842
  Copyright terms: Public domain W3C validator