Definition df-sqr 6670

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 6700 for its closure, sqrval 6671 for its value, sqrsq 6720 and sqsqr 6721 for its relationship to squares, and sqr11 6703 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 6669	. 2 class sqr
2		vx	. . . . . . 7 set x
3	2	cv 955	. . . . . 6 class x
4		cr 5233	. . . . . 6 class RR
5	3, 4	wcel 958	. . . . 5 wff x e. RR
6		cc0 5234	. . . . . 6 class 0
7		cle 5295	. . . . . 6 class <_
8	6, 3, 7	wbr 2619	. . . . 5 wff 0 <_ x
9	5, 8	wa 223	. . . 4 wff (x e. RR /\ 0 <_ x)
10		vy	. . . . . 6 set y
11	10	cv 955	. . . . 5 class y
12		vz	. . . . . . . . . 10 set z
13	12	cv 955	. . . . . . . . 9 class z
14	6, 13, 7	wbr 2619	. . . . . . . 8 wff 0 <_ z
15		cmul 5239	. . . . . . . . . 10 class x.
16	13, 13, 15	co 3963	. . . . . . . . 9 class (z x. z)
17	16, 3, 7	wbr 2619	. . . . . . . 8 wff (z x. z) <_ x
18	14, 17	wa 223	. . . . . . 7 wff (0 <_ z /\ (z x. z) <_ x)
19	18, 12, 4	crab 1648	. . . . . 6 class {z e. RR | (0 <_ z /\ (z x. z) <_ x)}
20		clt 5486	. . . . . 6 class <
21	19, 4, 20	csup 4573	. . . . 5 class sup({z e. RR | (0 <_ z /\ (z x. z) <_ x)}, RR, < )
22	11, 21	wceq 956	. . . 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 2666	. 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 956	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 6671

Copyright terms: Public domain