Definition df-abs 8004

Description: Define the function for the absolute value (modulus) of a complex number. See abscli 8090 for its closure and absval 8012 or absval2i 8092 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 8000	. 2 class abs
2		vx	. . . . . 6 set x
3	2	cv 1297	. . . . 5 class x
4		cc 6384	. . . . 5 class CC
5	3, 4	wcel 1300	. . . 4 wff x e. CC
6		vy	. . . . . 6 set y
7	6	cv 1297	. . . . 5 class y
8		ccj 7999	. . . . . . . 8 class *
9	3, 8	cfv 3998	. . . . . . 7 class (*` x)
10		cmul 6391	. . . . . . 7 class x.
11	3, 9, 10	co 4884	. . . . . 6 class (x x. (*` x))
12		csqr 7919	. . . . . 6 class sqr
13	11, 12	cfv 3998	. . . . 5 class (sqr` (x x. (*` x)))
14	7, 13	wceq 1298	. . . 4 wff y = (sqr` (x x. (*` x)))
15	5, 14	wa 240	. . 3 wff (x e. CC /\ y = (sqr` (x x. (*` x))))
16	15, 2, 6	copab 3395	. 2 class {<.x, y>. | (x e. CC /\ y = (sqr` (x x. (*` x))))}
17	1, 16	wceq 1298	1 wff abs = {<.x, y>. | (x e. CC /\ y = (sqr` (x x. (*` x))))}

This definition is referenced by:  absval 8012  absf 8158  cnph 9819

Copyright terms: Public domain