Definition df-abs 6755

Description: Define the function for the absolute value (modulus) of a complex number. See abscl 6839 for its closure and absvalt 6763 or absval2 6841 for its value.

Assertion

Ref	Expression
df-abs	|- abs = {<.x, y>. | (x e. CC /\ y = (sqr` (x x. (*` x))))}

Distinct variable group:   x,y

Detailed syntax breakdown of Definition df-abs

Step	Hyp	Ref	Expression
1		cabs 6751	. 2 class abs
2		vx	. . . . . 6 set x
3	2	cv 957	. . . . 5 class x
4		cc 5244	. . . . 5 class CC
5	3, 4	wcel 960	. . . 4 wff x e. CC
6		vy	. . . . . 6 set y
7	6	cv 957	. . . . 5 class y
8		ccj 6750	. . . . . . . 8 class *
9	3, 8	cfv 3188	. . . . . . 7 class (*` x)
10		cmul 5251	. . . . . . 7 class x.
11	3, 9, 10	co 3969	. . . . . 6 class (x x. (*` x))
12		csqr 6670	. . . . . 6 class sqr
13	11, 12	cfv 3188	. . . . 5 class (sqr` (x x. (*` x)))
14	7, 13	wceq 958	. . . 4 wff y = (sqr` (x x. (*` x)))
15	5, 14	wa 223	. . 3 wff (x e. CC /\ y = (sqr` (x x. (*` x))))
16	15, 2, 6	copab 2671	. 2 class {<.x, y>. | (x e. CC /\ y = (sqr` (x x. (*` x))))}
17	1, 16	wceq 958	1 wff abs = {<.x, y>. | (x e. CC /\ y = (sqr` (x x. (*` x))))}

This definition is referenced by:  absvalt 6763  absf 6906  cnph 8474

Copyright terms: Public domain