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

Definition df-rsqrt 10801
 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 √ = (𝑥 ∈ ℝ ↦ (𝑦 ∈ ℝ ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦)))
Distinct variable group:   𝑥,𝑦

Detailed syntax breakdown of Definition df-rsqrt
StepHypRef Expression
1 csqrt 10799 . 2 class
2 vx . . 3 setvar 𝑥
3 cr 7642 . . 3 class
4 vy . . . . . . . 8 setvar 𝑦
54cv 1331 . . . . . . 7 class 𝑦
6 c2 8794 . . . . . . 7 class 2
7 cexp 10322 . . . . . . 7 class
85, 6, 7co 5781 . . . . . 6 class (𝑦↑2)
92cv 1331 . . . . . 6 class 𝑥
108, 9wceq 1332 . . . . 5 wff (𝑦↑2) = 𝑥
11 cc0 7643 . . . . . 6 class 0
12 cle 7824 . . . . . 6 class
1311, 5, 12wbr 3936 . . . . 5 wff 0 ≤ 𝑦
1410, 13wa 103 . . . 4 wff ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦)
1514, 4, 3crio 5736 . . 3 class (𝑦 ∈ ℝ ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦))
162, 3, 15cmpt 3996 . 2 class (𝑥 ∈ ℝ ↦ (𝑦 ∈ ℝ ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦)))
171, 16wceq 1332 1 wff √ = (𝑥 ∈ ℝ ↦ (𝑦 ∈ ℝ ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦)))
 Colors of variables: wff set class This definition is referenced by:  sqrtrval  10803  absval  10804
 Copyright terms: Public domain W3C validator