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

Definition df-rsqrt 9207
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 √ = (x ℝ ↦ (y ℝ ((y↑2) = x 0 ≤ y)))
Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-rsqrt
StepHypRef Expression
1 csqrt 9205 . 2 class
2 vx . . 3 setvar x
3 cr 6710 . . 3 class
4 vy . . . . . . . 8 setvar y
54cv 1241 . . . . . . 7 class y
6 c2 7744 . . . . . . 7 class 2
7 cexp 8908 . . . . . . 7 class
85, 6, 7co 5455 . . . . . 6 class (y↑2)
92cv 1241 . . . . . 6 class x
108, 9wceq 1242 . . . . 5 wff (y↑2) = x
11 cc0 6711 . . . . . 6 class 0
12 cle 6858 . . . . . 6 class
1311, 5, 12wbr 3755 . . . . 5 wff 0 ≤ y
1410, 13wa 97 . . . 4 wff ((y↑2) = x 0 ≤ y)
1514, 4, 3crio 5410 . . 3 class (y ℝ ((y↑2) = x 0 ≤ y))
162, 3, 15cmpt 3809 . 2 class (x ℝ ↦ (y ℝ ((y↑2) = x 0 ≤ y)))
171, 16wceq 1242 1 wff √ = (x ℝ ↦ (y ℝ ((y↑2) = x 0 ≤ y)))
Colors of variables: wff set class
This definition is referenced by:  sqrtrval  9209  absval  9210
  Copyright terms: Public domain W3C validator