Description: Define the function for the absolute value (modulus) of a complex number. See abscli for its closure and absval or absval2i for its value. For example, ( abs-u 2 ) = 2 ( ex-abs ). (Contributed by NM, 27-Jul-1999)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-abs | |- abs = ( x e. CC |-> ( sqrt ` ( x x. ( * ` x ) ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cabs | |- abs |
|
| 1 | vx | |- x |
|
| 2 | cc | |- CC |
|
| 3 | csqrt | |- sqrt |
|
| 4 | 1 | cv | |- x |
| 5 | cmul | |- x. |
|
| 6 | ccj | |- * |
|
| 7 | 4 6 | cfv | |- ( * ` x ) |
| 8 | 4 7 5 | co | |- ( x x. ( * ` x ) ) |
| 9 | 8 3 | cfv | |- ( sqrt ` ( x x. ( * ` x ) ) ) |
| 10 | 1 2 9 | cmpt | |- ( x e. CC |-> ( sqrt ` ( x x. ( * ` x ) ) ) ) |
| 11 | 0 10 | wceq | |- abs = ( x e. CC |-> ( sqrt ` ( x x. ( * ` x ) ) ) ) |