Definition df-sqr 7920

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 sqrcli 7950 for its closure, sqrval 7921 for its value, sqrsqi 7970 and sqsqri 7971 for its relationship to squares, and sqr11i 7953 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 7919	. 2 class sqr
2		vx	. . . . . . 7 set x
3	2	cv 1297	. . . . . 6 class x
4		cr 6385	. . . . . 6 class RR
5	3, 4	wcel 1300	. . . . 5 wff x e. RR
6		cc0 6386	. . . . . 6 class 0
7		cle 6448	. . . . . 6 class <_
8	6, 3, 7	wbr 3338	. . . . 5 wff 0 <_ x
9	5, 8	wa 240	. . . 4 wff (x e. RR /\ 0 <_ x)
10		vy	. . . . . 6 set y
11	10	cv 1297	. . . . 5 class y
12		vz	. . . . . . . . . 10 set z
13	12	cv 1297	. . . . . . . . 9 class z
14	6, 13, 7	wbr 3338	. . . . . . . 8 wff 0 <_ z
15		cmul 6391	. . . . . . . . . 10 class x.
16	13, 13, 15	co 4884	. . . . . . . . 9 class (z x. z)
17	16, 3, 7	wbr 3338	. . . . . . . 8 wff (z x. z) <_ x
18	14, 17	wa 240	. . . . . . 7 wff (0 <_ z /\ (z x. z) <_ x)
19	18, 12, 4	crab 2108	. . . . . 6 class {z e. RR | (0 <_ z /\ (z x. z) <_ x)}
20		clt 6653	. . . . . 6 class <
21	19, 4, 20	csup 5663	. . . . 5 class sup({z e. RR | (0 <_ z /\ (z x. z) <_ x)}, RR, < )
22	11, 21	wceq 1298	. . . 4 wff y = sup({z e. RR | (0 <_ z /\ (z x. z) <_ x)}, RR, < )
23	9, 22	wa 240	. . 3 wff ((x e. RR /\ 0 <_ x) /\ y = sup({z e. RR | (0 <_ z /\ (z x. z) <_ x)}, RR, < ))
24	23, 2, 10	copab 3395	. 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 1298	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 7921

Copyright terms: Public domain