Definition df-rsqrt 10940

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

Step	Hyp	Ref	Expression
1		csqrt 10938	. 2 class √
2		vx	. . 3 setvar 𝑥
3		cr 7752	. . 3 class ℝ
4		vy	. . . . . . . 8 setvar 𝑦
5	4	cv 1342	. . . . . . 7 class 𝑦
6		c2 8908	. . . . . . 7 class 2
7		cexp 10454	. . . . . . 7 class ↑
8	5, 6, 7	co 5842	. . . . . 6 class (𝑦↑2)
9	2	cv 1342	. . . . . 6 class 𝑥
10	8, 9	wceq 1343	. . . . 5 wff (𝑦↑2) = 𝑥
11		cc0 7753	. . . . . 6 class 0
12		cle 7934	. . . . . 6 class ≤
13	11, 5, 12	wbr 3982	. . . . 5 wff 0 ≤ 𝑦
14	10, 13	wa 103	. . . 4 wff ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦)
15	14, 4, 3	crio 5797	. . 3 class (℩𝑦 ∈ ℝ ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦))
16	2, 3, 15	cmpt 4043	. 2 class (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℝ ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦)))
17	1, 16	wceq 1343	1 wff √ = (𝑥 ∈ ℝ ↦ (℩𝑦 ∈ ℝ ((𝑦↑2) = 𝑥 ∧ 0 ≤ 𝑦)))

This definition is referenced by:  sqrtrval  10942  absval  10943