Description: Define a function whose value is the real part of a complex number. See reval for its value, recli for its closure, and replim for its use in decomposing a complex number. (Contributed by NM, 9-May-1999)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | df-re | |- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 0 | cre | |- Re |
|
| 1 | vx | |- x |
|
| 2 | cc | |- CC |
|
| 3 | 1 | cv | |- x |
| 4 | caddc | |- + |
|
| 5 | ccj | |- * |
|
| 6 | 3 5 | cfv | |- ( * ` x ) |
| 7 | 3 6 4 | co | |- ( x + ( * ` x ) ) |
| 8 | cdiv | |- / |
|
| 9 | c2 | |- 2 |
|
| 10 | 7 9 8 | co | |- ( ( x + ( * ` x ) ) / 2 ) |
| 11 | 1 2 10 | cmpt | |- ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) ) |
| 12 | 0 11 | wceq | |- Re = ( x e. CC |-> ( ( x + ( * ` x ) ) / 2 ) ) |