previous up next
Go backward to 4.4 The Real Numbers
Go up to 4 Numbers
Go forward to 4.6 Relationships between Number Domains
RISC-Linz logo

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 := <x, y>.
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 = <x, y>;
imaginary(c) := such y: exists x: c in C /\  c = <x, y>.

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) 
0 := 0R+0Ri; 1 := 1R+0Ri; 2 := 2R+0Ri;
The  imaginary constant (imaginäre Konstante):
i := 0R+1Ri.
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)

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
      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

previous up next