ILE Home Intuitionistic Logic Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  ILE Home  >  Th. List  >  df-rsqrt Unicode version

Definition df-rsqrt 10725
Description: Define a function whose value is the square root of a nonnegative real number.

Defining the square root for complex numbers has one difficult part: choosing between the two roots. The usual way to define a principal square root for all complex numbers relies on excluded middle or something similar. But in the case of a nonnegative real number, we don't have the complications presented for general complex numbers, and we can choose the nonnegative root.

(Contributed by Jim Kingdon, 23-Aug-2020.)

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

Detailed syntax breakdown of Definition df-rsqrt
StepHypRef Expression
1 csqrt 10723 . 2  class  sqr
2 vx . . 3  setvar  x
3 cr 7587 . . 3  class  RR
4 vy . . . . . . . 8  setvar  y
54cv 1315 . . . . . . 7  class  y
6 c2 8735 . . . . . . 7  class  2
7 cexp 10247 . . . . . . 7  class  ^
85, 6, 7co 5742 . . . . . 6  class  ( y ^ 2 )
92cv 1315 . . . . . 6  class  x
108, 9wceq 1316 . . . . 5  wff  ( y ^ 2 )  =  x
11 cc0 7588 . . . . . 6  class  0
12 cle 7769 . . . . . 6  class  <_
1311, 5, 12wbr 3899 . . . . 5  wff  0  <_  y
1410, 13wa 103 . . . 4  wff  ( ( y ^ 2 )  =  x  /\  0  <_  y )
1514, 4, 3crio 5697 . . 3  class  ( iota_ y  e.  RR  ( ( y ^ 2 )  =  x  /\  0  <_  y ) )
162, 3, 15cmpt 3959 . 2  class  ( x  e.  RR  |->  ( iota_ y  e.  RR  ( ( y ^ 2 )  =  x  /\  0  <_  y ) ) )
171, 16wceq 1316 1  wff  sqr  =  ( x  e.  RR  |->  ( iota_ y  e.  RR  ( ( y ^
2 )  =  x  /\  0  <_  y
) ) )
Colors of variables: wff set class
This definition is referenced by:  sqrtrval  10727  absval  10728
  Copyright terms: Public domain W3C validator