Definition df-sqr 4728

Description: Define a function whose value is the square root of a nonnegative real number. The square root of x is the supremum of all reals whose square is less than x. See sqrcl 4758 for its closure, sqrval 4729 for its value, sqrsqe 4774 and sqsqr 4775 for its relationship to squares, and sqr11 4761 for uniqueness.

Assertion

Ref	Expression
df-sqr	⊢ √ = {⟨x, y⟩∣((x ∈ ℝ ∧ 0 ≤ x) ∧ y = sup({z ∈ ℝ∣(0 ≤ z ∧ (z · z) ≤ x)}, ℝ, < ))}

Distinct variable group(s):   x,y,z

Detailed syntax breakdown of Definition df-sqr

Step	Hyp	Ref	Expression
1		csqr 4727	. 2 class √
2		vx	. . . . . . 7 set x
3	2	cv 1089	. . . . . 6 class x
4		cr 4027	. . . . . 6 class ℝ
5	3, 4	wcel 1092	. . . . 5 wff x ∈ ℝ
6		cc0 4028	. . . . . 6 class 0
7		cle 4092	. . . . . 6 class ≤
8	6, 3, 7	wbr 2054	. . . . 5 wff 0 ≤ x
9	5, 8	wa 196	. . . 4 wff (x ∈ ℝ ∧ 0 ≤ x)
10		vy	. . . . . 6 set y
11	10	cv 1089	. . . . 5 class y
12		vz	. . . . . . . . . 10 set z
13	12	cv 1089	. . . . . . . . 9 class z
14	6, 13, 7	wbr 2054	. . . . . . . 8 wff 0 ≤ z
15		cmulc 4032	. . . . . . . . . 10 class ·
16	13, 13, 15	co 3001	P. . . . . . . . 9 class (z · z)
17	16, 3, 7	wbr 2054	. . . . . . . 8 wff (z · z) ≤ x
18	14, 17	wa 196	. . . . . . 7 wff (0 ≤ z ∧ (z · z) ≤ x)
19	18, 12, 4	crab 1204	. . . . . 6 class {z ∈ ℝ∣(0 ≤ z ∧ (z · z) ≤ x)}
20		clt 4033	. . . . . 6 class <
21	19, 4, 20	csup 2060	. . . . 5 class sup({z ∈ ℝ∣(0 ≤ z ∧ (z · z) ≤ x)}, ℝ, < )
22	11, 21	wceq 1091	. . . 4 wff y = sup({z ∈ ℝ∣(0 ≤ z ∧ (z · z) ≤ x)}, ℝ, < )
23	9, 22	wa 196	. . 3 wff ((x ∈ ℝ ∧ 0 ≤ x) ∧ y = sup({z ∈ ℝ∣(0 ≤ z ∧ (z · z) ≤ x)}, ℝ, < ))
24	23, 2, 10	copab 2055	. 2 class {⟨x, y⟩∣((x ∈ ℝ ∧ 0 ≤ x) ∧ y = sup({z ∈ ℝ∣(0 ≤ z ∧ (z · z) ≤ x)}, ℝ, < ))}
25	1, 24	wceq 1091	1 wff √ = {⟨x, y⟩∣((x ∈ ℝ ∧ 0 ≤ x) ∧ y = sup({z ∈ ℝ∣(0 ≤ z ∧ (z · z) ≤ x)}, ℝ, < ))}

This definition is referenced by:  sqrval 4729

metamath.org