Definition df-sqr 6671

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 6701 for its closure, sqrval 6672 for its value, sqrsq 6721 and sqsqr 6722 for its relationship to squares, and sqr11 6704 for uniqueness.

Assertion

Ref	Expression
df-sqr	|- sqr = {<.x, y>. | ((x e. RR /\ 0 <_ x) /\ y = sup({z e. RR | (0 <_ z /\ (z x. z) <_ x)}, RR, < ))}

Distinct variable group:   x,y,z

Detailed syntax breakdown of Definition df-sqr

Step	Hyp	Ref	Expression
1		csqr 6670	. 2 class sqr
2		vx	. . . . . . 7 set x
3	2	cv 957	. . . . . 6 class x
4		cr 5245	. . . . . 6 class RR
5	3, 4	wcel 960	. . . . 5 wff x e. RR
6		cc0 5246	. . . . . 6 class 0
7		cle 5307	. . . . . 6 class <_
8	6, 3, 7	wbr 2624	. . . . 5 wff 0 <_ x
9	5, 8	wa 223	. . . 4 wff (x e. RR /\ 0 <_ x)
10		vy	. . . . . 6 set y
11	10	cv 957	. . . . 5 class y
12		vz	. . . . . . . . . 10 set z
13	12	cv 957	. . . . . . . . 9 class z
14	6, 13, 7	wbr 2624	. . . . . . . 8 wff 0 <_ z
15		cmul 5251	. . . . . . . . . 10 class x.
16	13, 13, 15	co 3969	. . . . . . . . 9 class (z x. z)
17	16, 3, 7	wbr 2624	. . . . . . . 8 wff (z x. z) <_ x
18	14, 17	wa 223	. . . . . . 7 wff (0 <_ z /\ (z x. z) <_ x)
19	18, 12, 4	crab 1651	. . . . . 6 class {z e. RR | (0 <_ z /\ (z x. z) <_ x)}
20		clt 5498	. . . . . 6 class <
21	19, 4, 20	csup 4582	. . . . 5 class sup({z e. RR | (0 <_ z /\ (z x. z) <_ x)}, RR, < )
22	11, 21	wceq 958	. . . 4 wff y = sup({z e. RR | (0 <_ z /\ (z x. z) <_ x)}, RR, < )
23	9, 22	wa 223	. . 3 wff ((x e. RR /\ 0 <_ x) /\ y = sup({z e. RR | (0 <_ z /\ (z x. z) <_ x)}, RR, < ))
24	23, 2, 10	copab 2671	. 2 class {<.x, y>. | ((x e. RR /\ 0 <_ x) /\ y = sup({z e. RR | (0 <_ z /\ (z x. z) <_ x)}, RR, < ))}
25	1, 24	wceq 958	1 wff sqr = {<.x, y>. | ((x e. RR /\ 0 <_ x) /\ y = sup({z e. RR | (0 <_ z /\ (z x. z) <_ x)}, RR, < ))}

This definition is referenced by:  sqrval 6672

Copyright terms: Public domain