Go backward to 4.4 The Real NumbersGo up to 4 NumbersGo forward to 4.6 Relationships between Number Domains

## 4.5 The Complex Numbers

Even R does not allow to solve all equations that can be formulated with + and *, e.g. there is no x in R such that
x*x = -1.

Proof  We prove forall x in R: x*x != -1. Take arbitrary x in R. If x >= 0, then x*x >= 0. If x < 0, then also x*x >= 0. Since -1 not  >= 0, x*x != 0.

We introduce a domain in which all equations of this kind can be solved.

Definition 50 (Complex Numbers) The set C of  complex numbers (komplexe Zahlen) is defined as follows:
C:= R x R.
We define a corresponding constructor
 _+_i: R x R -> C x+yi := .
Let c in C and take x and y such that c=<x,y>. We call x the  real part (Realteil) of c and y its  imaginary part (Imaginärteil):
 real(c) := such x: exists y: c in C /\  c = ; imaginary(c) := such y: exists x: c in C /\  c = .

So the question what a complex number x+yi is, can be easily answered: it is the tuple <x, y>.

Logic Evaluator  The corresponding executable definitions (on the basis of rationals instead of reals) are given in Appendix `complex.txt`.

The usual operations on complex numbers are then defined as follows:

Definition 51 (Complex Number Operations)
Constants
 0 := 0R+0Ri; 1 := 1R+0Ri; 2 := 2R+0Ri;
The  imaginary constant (imaginäre Konstante):
 i := 0R+1Ri.
Arithmetic
 x + y := (x0 +R y0) + (x1 +R y1)i; x - y := (x0 -R y0) + (x1 -R y1)i; -x := (-Rx0)+(-Rx1)i; x * y := ((x0 *R y0) -R (x1 *R y1)) + ((x0 * R y1) + (x1 *R y0))i; x / y := (((x0 *R y0) +R (x1 *R y1)) /R d) + (((x1 *R y0) -R (x0 * R y1)) /R d)i where d = (y0 *R y0) +R (y1 *R y1); x-1 := 1 / x.
Special Operations

The  complex conjugate (konjugiert komplexe Zahl):

 x := x0 + (-R x1)i.

The absolute value (Absolutbetrag):

 |x| := sqrt((x0 *R x0) +R (x1 *R x1)).

Please note that an application x+yi of the constructor function denotes the tuple <x, y> while the imaginary constant i denotes (0R+1Ri), i.e., <0R, 1R>. This imaginary constant is the "missing value" that solves the equation stated at the begin of this section.

Proof  We prove i * i = -1.
i * i = (definition of i)
(0R + 1Ri) *R (0R + 1Ri) = (definition of *)
 ((0R *R 0R) -R (1R *R 1R)) + ((0R *R 1R)+R (1R *R 0R))i
= (arithmetic in R)
(-R 1R) + (-R 0R)i = (definition of -)
-(1R + 0Ri) = (definition of 1)
-1.

Logic Evaluator  Function `conj` computes the complex conjugate and `||^2` returns the square of the absolute value:

The following proposition tells us that our quest for a closed number domain has reached its goal.

Proposition 55 (Fundamental Theorem of Algebra) For every a0 in C, ..., an-1 in C, there exists an x in C such that
a0*x0 + ...+ an-1*xn-1 = 0.

We now introduce the complex root function analogously to the corresponding operation on the reals.

Definition 52 (Complex Root Function)
 sqrtn(x) := such y: xn = y

As a consequence of Proposition Fundamental Theorem, we then have

 forall a in C, n in N>0: (sqrtn(a))n = a.

For the special case of the square root function, we give a definition that immediately allows us to "compute" the square of a complex number.

Definition 53 (Complex Square Root)
 sqrt(.): C -> C sqrt(x) := if x1 >= R 0R then u+vi else u+(-Rv)i where u = sqrt((x0 +R sqrt(x02 +R x12)) /R 2R) v = sqrt((-Rx0 +R sqrt(x02 +R x12)) /R 2R).

The equation x*x=a has in general two solutions, the one denoted by the definition above and the one we get by multiplying the value with (-1). In other words, the following holds:

 forall x in C : let r = sqrt(x): x=r*r /\  x=(-r)*(-r).

Absolute Value  Out definition of the absolute value implies, for every x in R, |x+0i| = sqrt(x*Rx), i.e.,

|x+0i| = if x <= R 0R then -Rx else x
which corresponds to the usual definition of | | on R. The absolute value satisfies the following equations and inequalities.

Proposition 56 (Absolute Value) For every x in C, y in C, z in C, the following holds:
 |x| >= R 0R, |-x| = |x|, |x| = 0R <=> x = 0, |x+y| <= R |x| +R |y|, |x-y| <= R |x| +R |y|, ||x| -R |y|| <= R |x + y|, ||x| -R |y|| <= R |x - y|, |x*y| = |x| *R |y|, y != 0 => |x/y| = |x| /R |y|.

Likewise we have the following laws for the complex conjugate.

Proposition 57 (Complex Conjugate) For every x in C, y in C, z in C, the following holds:
 x = x, x+y = x + y, x*y = x * y, y != 0 => x/y = x / y, x1 = 0R <=> x = x, x = ((x+x)/2) + ((x-x)/2)i, |x| = sqrt(z*z)

The set C "embeds" R in the sense that will be discussed in Section Embedding Sets.

Author: Wolfgang Schreiner
Last Modification: October 4, 1999