Skeleton for the Proof development leading to the Fundamental Theorem of Algebra

Herman Geuvers, Randy Pollack, Freek Wiedijk, Jan Zwanenburg

November 10, 2000

1 Setoids

A basic ingredient of constructive real numbers is the apartness relation #. This is a constructive version of the (classical) inequality on reals: two real numbers are apart if it can positively be decided that they are distinct from each other. In constructive analysis, the apartness is more basic then equality. We therefore take the notion of apartness as a basic ingredient of our structures Usually this apartness is taken to be tight, saying that the negation of apartness is the equality. In [3] and [4] also apartness relations occur that are not necessarily tight, but in the formalization of reals one can restrict to a tight apartness. This also implies that, in the formalization, we could have done without an equality alltogether (and replace it with the negation of #). For reasons of exposition and for relating to a more classical set-up we choose to take equality as a primitive.

Definition 1.1 A binary relation # on a set S is an apartness relation if

1. # is consistent, i.e. ¬a # a for all a.

2. # is symmetric, i.e. a # b → b # a for all a, b.

3. # is cotransitive, i.e. a # b → ∀z[a # z ∨ z # b] for all a, b.

An apartness relation is tight if its negation is the equality, i.e. ¬(a # b) ↔ a = b for all a, b.

Fact 1.2 The negation of an apartness relation on S is an equivalence relation on S which is stable, i.e. ¬¬¬(a # b) → ¬(a # b).

Lemma 1.3 A tight apartness relation respects the equality, i.e.

a # b ∧ b = b′ → a # b′ for all a, b, b′.

Proof If a # b, then a # b′ ∨ b # b′. The latter is false, because b = b′.

Definition 1.4 A constructive setoid is a triple ⟨S, =, #⟩, with S a set, = an equivalence relation on S and # a tight apartness relation on S.

In a structure, we want the operations and relations to respect the equality and the apartness. For the equality this means that we want to have the replacement property for all predicates:

R(x_{1}, …, x_{n}) ∧ x_{1} = y_{1} ∧ … ∧ x_{n} = y_{n} → R(y_{1}, …, y_{n}).

Fact 1.5 The replacement property is closed under ∨, ∧, ¬, →, ∃ and ∀.

So, we only have to require that the basic relations satisfy the replacement property and that all basic operations are well-defined with respect to the equality, i.e. for f of arity n we have the following.

x_{1} = y_{1} ∧ … ∧ x_{n} = y_{n} → f(x_{1}, …, x_{n}) = f(y_{1}, …, y_{n}).

If we have a tight apartness relation, this immediately implies

¬(x_{1} # y_{1}) ∧ … ∧ ¬(x_{n} # y_{n}) → ¬(f(x_{1}, …, x_{n}) # f(y_{1}, …, y_{n})),

but one would like to have a more positive formulation saying

f(x_{1}, …, x_{n}) # f(y_{1}, …, y_{n}) → (x_{1} # y_{1}) ∨ … ∨ (x_{n} # y_{n}).

This property is called strong extensionality of f.

Definition 1.6 Let S be a set with an apartness relation # defined on it. For f a n-ary function on S, we say that f is strongly extensional if

∀x_{1}, …, x_{n}, y_{1}, …, y_{n}[f(x⃗) # f(y⃗) → (x_{1} # y_{1} ∨ … ∨ x_{n} # y_{n})].

For R a n-ary relation on S, we say that R is strongly extensional if

∀x_{1}, …, x_{n}, y_{1}, …, y_{n}[R(x⃗) → (R(y⃗) ∨ x_{1} # y_{1} ∨ … ∨ x_{n} # y_{n})].

Fact 1.7 Strong extensionality of functions is closed under composition. Strong extensionality of relations is closed under ∨, ∧, ∃ and the substitution of strongly extensional terms.

Lemma 1.8 Strong extensionality implies well-definedness for functions.

Proof Suppose f(x⃗) # f(y⃗) → (x_{1} # y_{1} ∨ … ∨ x_{n} # y_{n}) for all x_{1}, …, x_{n}, y_{1}, …, y_{n}. Suppose x_{1} = y_{1} ∧ … ∧ x_{n} = y_{n} and f(x⃗) # f(y⃗). Then x_{1} # y_{1} ∨ … ∨ x_{n} # y_{n} by strong extensionality of f. Contradiction, so ¬(f(x⃗) # f(y⃗)), i.e. f(x⃗) = f(y⃗).

Remark 1.9 Strong extensionality (for functions) says that a function can only distinguish elements that can already be distinguished. We will require all basic functions in constructive structures to be strongly extensional. As a consequence, all composed functions will be strongly extensional.

We do not want all relations to be strongly extensional. For example, equality is not strongly extensional: if it were, then x = y → p = q ∨ x # p ∨ y # q for all x, y, p, q, which implies the decidability of equality (take x for y and p).

Lemma 1.10 If a binary function f is strongly extensional in both arguments, i.e.

∀x_{1}, x_{2}, y[f(x_{1}, y) # f(x_{2}, y) → (x_{1} # x_{2})],
∀x, y_{1}, y_{2}[f(x, y_{1}) # f(x, y_{2}) → (y_{1} # y_{2})],

then it is strongly extensional. Similarly for functions of higher arity.

Proof Suppose the binary function f is strongly extensional in both arguments and suppose f(x_{1}, y_{1}) # f(x_{2}, y_{2}). Then f(x_{1}, y_{1}) # f(x_{1}, y_{2}) ∨ f(x_{1}, y_{2}) # f(x_{2}, y_{2}) by cotransitivity. Hence y_{1} # y_{2} ∨ x_{1} # x_{2}.

Lemma 1.11 If f is strongly extensional, then

f(x⃗) ≠ f(y⃗) → ¬(x_{1} = y_{1} ∧ … ∧ x_{n} = y_{n}).

Proof Suppose f(x⃗) ≠ f(y⃗), i.e. ¬¬(f(x⃗) ≠ f(y⃗)). Suppose also that x_{1} = y_{1} ∧ … ∧ x_{n} = y_{n}. Now, if f(x⃗) # f(y⃗), then x_{1} # y_{1} ∨ … ∨ x_{n} # y_{n}, contradicting x_{1} = y_{1} ∧ … ∧ x_{n} = y_{n}. So ¬(f(x⃗) # f(y⃗)), contradicting f(x⃗) ≠ f(y⃗). So we conclude that ¬(x_{1} = y_{1} ∧ … ∧ x_{n} = y_{n}).

If a function f has an inverse, we want it to respect the apartness. Note that, if f has no inverse we do not want that in general (e.g. consider multiplication in ℤ_{4}). That f respects # comes as a consequence of strong extensionality and the existence of an inverse.

Lemma 1.12 Suppose that the unary function f has an inverse g which is strongly extensional. Then f respects the apartness, i.e.

x # y → f(x) # f(y).

Proof We know that g(x) # g(y) → x # y and that g(f(x)) = x. Now suppose x # y, i.e. g(f(x)) # g(f(y)). Then f(x) # f(y) by strong extensionality of g.

Lemma 1.13 If f respects the apartness, then f respects the inequality

Proof Let f respect the apartness(i.e. (x_{1} # y_{1} ∨ … ∨ x_{n} # y_{n}) → f(x⃗) # f(y⃗)). Suppose x_{1} ≠ y_{1} ∨ … ∨ x_{n} ≠ y_{n} and suppose f(x⃗ = f(y⃗). Now, if x_{i} # y_{i} for some i, then f(x⃗ # f(y⃗), contradiction, so x_{i} = y_{i} for all i. This is again a contradiction, so f(x⃗) ≠ f(y⃗).

Lemma 1.14 If a relation R is strongly extensional in each of its arguments, it is strongly extensional.

Proof We give the proof for a binary relation R. Suppose R is strongly extensional in both arguments, i.e.

R(x, y) → R(x, q) ∨ y # q,
R(x, y) → R(p, y) ∨ p # x.

for all x, y, p, q. Now, if R(x, y), then R(x, q) ∨ y # q. If R(x, q), then R(p, q) ∨ p # x, so R(p, q) ∨ p # x ∨ y # q.

Lemma 1.15 Apartness is strongly extensional.

Proof Suppose x # y. Then x # p ∨ y # p by cotransitivity and hence x # p ∨ y # q ∨ p # q by again cotransitivity.

1.1 On the choice of the primitives

In view of the fact that we require an apartness relation in a setoid to be tight, we could have chosen to define a setoid as a pair ⟨S, #⟩ with # an apartness relation and then define equality by

x = y := ¬(x # y).

Then the following can be shown.

1. If an operation f is strongly extensional, then it respects =.

2. If a relation R is strongly extensional, then it satisfies the replacement property.

3. Hence all relations satisfy the replacement property.

So, we could have done without an equality alltogether. However, we have not chosen this option, because equality is a natural primitive. Furthermore one may at some point encounter structures in which apartness is not tight.

1.2 Subsetoids and Quotient Setoids

Definition 1.16 Given a constructive setoid ⟨S, =, #⟩ and a predicate P on S, we define the subsetoid of the x ∈ S that satisfy P as the setoid ⟨{x ∈ S | P (x)}, =′, #′⟩, where =′ and #′ are the equality and apartness inherited from S, i.e. for q, t ∈ {x ∈ S | P (x)},

t =′ q ⟺ t = q,
t #′ q ⟺ t # q,

We denote this subsetoid just by {x ∈ S | P (x)}.

For this definition to be correct, it has to be shown that =′ is indeed an equivalence relation and that #′ is a tight apartness relation (w.r.t. =) on {x ∈ S | P (x)}. This is trivially the case. As the equivalence and apartness are directly inherited from S, we never write them explicitly, but use the ones from S.

Definition 1.17 Given a constructive setoid ⟨S, =, #⟩ and a strongly extensional apartness relation Q on S, we define the co-quotient setoid S/R as the setoid ⟨S, \overline{R}, R⟩, where \overline{R} is the complement of R, i.e. \overline{R}(x, y) iff ¬R(x, y).

For this definition to be correct, it has to be shown that \overline{R} is an equivalence relation and that R is a tight apartness relation (w.r.t. \overline{R}) on \{x ∈ S | P (x)\}. This follows trivially from the definition of \overline{R} and the fact that R is an apartness.

If we do not require R to be strongly extensional, S/R as defined above is still a constructive setoid. However, we only want to consider the situation where the new apartness R is a subset of the old one, i.e. R(x, y) → x # y. This is a consequence of strong extensionality of R: take x for p and for q in R(x, y) → (R(p, q) ∨ x # p ∨ y # q). As a consequence we then find that = is a subset of \overline{R}, so the new equality is a refinement of the old one. So, the definition of co-quotient setoid subsumes the ordinary definition of quotient set.

For a strongly extensional function f on a setoid ⟨S, =, #⟩ we find that, if f is strongly extensional w.r.t. R, with R a strongly extensional apartness relation on S, then f is also strongly extensional on the co-quotient setoid.

The real numbers form a primary example of a co-quotient setoid. They can be seen as the setoid (ℕ→ℚ)/R, where ℕ→ℚ is the set of infinite sequences of rational numbers and R is the apartness relation between such sequences: for r and s two sequences, R(r, s) iff ∃k, N ∈ ℕ∀m > N(|r_{m} − s_{m}| > \frac{1}{k}).

2 Constructive Commutative Algebra

We define the notions of commutative monoid, group, ring, integral domain and field in a constructive way. In doing so, we follow [3] and [6], by requiring the basic operations to be strongly extensional. In the end this choice does not effect our work, because in a real number structure, it can be proved from the axioms that all basic operations and relations are strongly extensional.

Convention 2.1 Without stating it explicitly, we require all operations on setoids to respect the equality. We also require all basic operations and relations on setoids to be strongly extensional (Definition 1.6).

2.1 Groups: One associative operation

Definition 2.2 (Constructive Semi-Group) A constructive semi-group is a tuple ⟨S, +, =, #⟩ with ⟨S, =, #⟩ a constructive setoid, + a binary operation on S such that

1. + is associative: ∀x, y, z[(x + y) + z = x + (y + z)].

Definition 2.3 (Constructive Monoid) A constructive monoid is a tuple ⟨S, 0, +, =, #⟩ with ⟨S, +, =, #⟩ a constructive semi-group and 0 an element of S such that

1. 0 is the identity w.r.t. +: ∀x[x + 0 = x].

Definition 2.4 (Constructive Group) A constructive group is a tuple ⟨S, 0, +, −, =, #⟩ with ⟨S, 0, +, =, #⟩ a constructive monoid, − a unary operation on S such that

1. −x is the inverse of x: ∀x[x + (−x) = 0].

In practice we write “x − y” for “x + (−y)”.

Lemma 2.5 (Inverses are unique) The inverse of + is unique, i.e. for all x, y,

x + y = 0 → y = −x.

As a consequence we find immediately that for all x, y,

−(−x) = x,
−(x + y) = (−y) + (−x).

Lemma 2.6 (Cancellation) For all x, y, z,

x + y = x + z → x = y.

2.1.1 Apartness in Groups

Lemma 2.7 For all x, y,

x + y # 0 → x # 0 ∨ y # 0.

Proof By strong extensionality of +, x + y # 0 + 0 implies x # 0 ∨ y # 0.

Lemma 2.8 The operations of a group respect #, i.e. for all x, y, z,

x # y ↔ x + z # y + z,
x # y ↔ x − y # 0,
x # 0 ↔ −x # 0.

Proof For direction →, (x + z) − z = x # y = (y + z) − z (using that # respects =, 1.3), so by strong extensionality of +, x + z # y + z. The converse uses the forward direction with −z. The second part follows from the first part noting that 0 = y − y.

Remark 2.9 As has already been pointed out, we always require functions to respect the equality and to be strongly extensional. In general, you’d want a function to respect the inequality or the apartness only if it has an inverse. See Lemma 1.12.

2.2 Rings: Two associative operations

Definition 2.10 (Constructive Ring) A non-trivial constructive ring is a tuple ⟨S, 0, 1, +, −, ∗, =, #⟩ with ⟨S, 0, +, −, =, #⟩ a constructive group and ⟨S, 1, ∗, =, #⟩ a constructive monoid such that

1. Non-triviality: 1 # 0.

2. + distributes over ∗: ∀x, y, z[x ∗ (y + z) = (x ∗ y) + (x ∗ z)].

Notation 2.11 When dealing with rings we replace the operation ∗ by juxtaposition, writing xy for x ∗ y.

Lemma 2.12 For all x, y:

x0 = 0,
x(−y) = −(xy).

Proof The first by cancellation: x0 = x(0 + 0) = x0 + x0. The second (using the first) by uniqueness of inverses 2.5.

Lemma 2.13 For all x, y,

xy # 0 → x # 0 ∧ y # 0.

Proof Suppose xy # 0. As ∗ is strongly extensional, we know xy # x0 → y # 0 and xy # 0y → x # 0.

Definition 2.14 (Constructive Field) A constructive field is a tuple ⟨S, 0, 1, +, −, ∗,^{−1} , =, #⟩ such that ⟨S, 0, 1, +, −, ∗, =, #⟩ is a constructive ring and ^{−1} is an operation on the subsetoid {x ∈ S | x # 0}, such that

1. x^{−1} is inverse of x with respect to ∗: ∀x[x # 0 → xx^{−1} = 1].

We have not introduces Integral Domains as a seperate algebraic notion, but constructive fields are indeed constructive integral domains, as they satisfy the following property.

Lemma 2.15 (Integral Domain Property) In a constructive field we have

∀x, y[x # 0 ∧ y # 0 → xy # 0],

that is, a constructive field is a constructive integral domain.

Proof Suppose x # 0, y # 0. Then (xy)y^{−1} = x # 0 = 0y^{−1}, so xy # 0, by strong extensionality of ∗. .

Lemma 2.16 If ⟨S, 0, 1, +, −, ∗,^{−1} , =, #⟩ is a constructive field, then ⟨{x ∈ S | x # 0}, 1, ∗, =, #⟩ forms a constructive monoid.

Lemma 2.17 In a constructive field, ∗ respects #, i.e.

∀x, y, z[x # y ∧ z # 0 → xz # yz].

Proof Suppose x # y and z # 0. By lemma 2.8, we have that x − y # 0. Hence xz − yz = (x − y)z # 0, and zx # zy using lemma 2.8 again.

Lemma 2.18 The following hold in a constructive field.

x ≠ 0 ∧ y ≠ 0 → xy ≠ 0,
x ≠ y ∧ z ≠ 0 → xz ≠ yz,
x ≠ 0 ∧ xy = 0 → y = 0.

Proof For the first, suppose ¬¬(x # 0) and ¬¬(y # 0) and suppose ¬(xy # 0). If x 0̸, then if y # 0 we would have xy # 0, contradiction, so ¬(y # 0. But this is a contradiction, so ¬(x # 0). Contradiction, so ¬¬(xy # 0).

For the second, suppose x ≠ y and z ≠ 0. Then x − y ≠ 0 (using Lemma 1.11). Now, z(x − y) ≠ 0 using the first and hence zx ≠ zy using distributivity and again Lemma 1.11. For the third, suppose x ≠ 0 and xy = 0. If y ≠ 0, then xy ≠ 0 by the first. Contradiction, so ¬(y ≠ 0), which implies y = 0.

Remark 2.19 It is in general not the case that in a constructive integral domain,

xy = 0 → x = 0 ∨ y = 0.

This is just because the ∨ has a strong interpretation. A weak counterexample is given by defining the real numbers x and y respectively by the following Cauchy sequences of rationals (x_{i})_{i∈ℕ}, resp. (y_{i})_{i∈ℕ}. (In this definition we use k_{99} as abbreviation of ‘the number k where we have just completed a sequence of 99 9s in the decimal series of π. Similarly i < k_{99} if up to i we have not yet encountered such a sequence of 99 9s.)

x_{i} := 2^{−i} if i < k_{99},
x_{i} := 2^{i} if i ≥ k_{99} and k_{99} is even,
x_{i} := 0 if i ≥ k_{99} and k_{99} is odd,
y_{i} := 2^{−i} if i < k_{9}9,
y_{i} := 2^{i} if i ≥ k_{99} and k_{99} is odd,
y_{i} := 0 if i ≥ k_{99} and k_{99} is even.

Now, xy = 0, but to say that x = 0 implies that we know that k_{99} exists and that it is odd. Similarly for y = 0.

Lemma 2.20 In a constructive field we have the following

x^{2} = a^{2} → ¬(x # a ∧ x # −a),
2 # 0 ∧ a # 0 ∧ x^{2} = a^{2} → x = a ∨ x = −a.

Proof If x^{2} = a^{2}, then

(x − a)(x + a) = 0. (∗)

Now, if x # a ∧ x # −a, then x − a # 0 ∧ x + a # 0, hence (x − a)(x + a) # 0, contradiction. If also a # 0, then a # −a (a # 0 → 2a # 0 → a # −a). Hence x # a ∨ x # −a by cotransitivity of #. Now, if x # a, then x − a # 0 hence x + a = 0 by (*) and Lemma 2.18, and hence x = −a. Similarly, if x # −a, then x = a.

Remark 2.21 In the previous Lemma we use the premise 2 # 0 to conclude a −̸a from a 0̸. Note that if 2 = 0, the result (a # 0 ∧ x^{2} = a^{2} → x = a ∨ x = −a) is also true. We would like to prove 2 # 0 ∨ 2 = 0, so we can drop the assumption 2 # 0 in the Lemma. We conjecture this to hold (the charachteristic of a field is discreet, also constructively (?)). Note that for the present development this doesn’t really matter, as we will only be dealing with fields of charachteristic 0 (hence 2 # 0): the reals and the complex numbers.

Lemma 2.22 If  ⟨S, 0, 1, +, −, ∗,^{−1} , =, #⟩  is  a  constructive  field,  then

⟨{x ∈ S | x # 0}, 1, ∗,^{−1} , =, #⟩ is a constructive group.

Definition 2.23 (Constructive Ordered Field) A constructive ordered field is a tuple ⟨S, 0, 1, +, −, ∗,^{−1} , =, <, #⟩ such that ⟨S, 0, 1, +, −, ∗,^{−1} , =, #⟩ is a constructive field and < is a binary relation on S such that

1. < is transitive, irreflexive, anti-symmetric,

2. + respects <, i.e. ∀x, y[x < y → ∀z[x + z < y + z]],

3. ∗ respects 0 <, i.e. ∀x, y[0 < x ∧ 0 < y → 0 < xy],

4. ∀x, y[x # y ↔ (x < y ∨ y < x)], 2.2.1 Properties of the ordering in a field Lemma 2.24 (< is cotransitive) The relation < is cotransitive:

∀x, y[x < y → ∀z[x < z ∨ z < y]].

Proof Suppose x < y, then x # y, so for all z: x # z ∨z # y. Hence x < z ∨z < x∨z < y ∨y < z. As z < x → z < y and y < z → x < z, we conclude that x < z ∨ z < y. Lemma 2.25 (∗ respects <)

a < b, c > 0 → ac < bc.

Proof Using Axioms 3, 4 and distributivity. Lemma 2.26

a > b ↔ −a < −b.

Proof Using Axiom 3. Corollary 2.27

0 < 1.

Proof 0 < 1 ∨ 1 < 0. If 1 < 0, then −1 > 0 (by 2.26), so 1 = (−1)(−1) > 0. Lemma 2.28

a > 0 ↔ a^{−1} > 0.

Proof If a > 0, then a # 0, so a^{−1} # 0, i.e. a^{−1} > 0 ∨ a^{−1} < 0. Now, if a^{−1} < 0, then −a^{−1} > 0 (Lemma 2.26), so −1 > 0 (Lemma 2.25), contradiction. Hence a^{−1} > 0. Lemma 2.29

a > b > 0 ↔ b^{−1} > a^{−1} > 0
0 > a > b ↔ 0 > b^{−1} > a^{−1}.

Proof The first using Lemma 2.25 and Lemma 2.28. The second using Lemma 2.26 and the first.

Definition 2.30 We define the relation ≤ by

x ≤ y := ¬(y < x).

Lemma 2.31

x ≤ y → x + z ≤ y + z,
x ≤ y ∧ z > 0 → xz ≤ yz.

Proof If x + z > y + z, then x > y by Axiom 3. If xz > yz and z > 0, then x > y by Lemma 2.25, using Lemma 2.28. Lemma 2.32 x ≥ y ↔ ∀z[y > z → x > z]. Proof From right to left: Suppose x < y, then x < \frac{x+y}{2} < y, contradiction. From left to right: Let z ∈ ℝ be such that y > z. Then y > x ∨ x > z. As y ≤ x, we conclude that x > z. Lemma 2.33

x ≤ y ∧ y ≤ x → x = y,
x > y ∨ y = x → x ≥ y

Proof Both trivial.

Lemma 2.34

x < y ∧ y ≤ z → x < z,
x ≤ y ∧ y < z → x < z,
x ≤ y ∧ y ≤ z → x ≤ z.

Proof For the first, if x < y, then x < z ∨ z < y. As y ≤ z we conclude that x < z. The second is similar. For the third, suppose x > z. The x > z using the second, contradiction.

Lemma 2.35 x^{2} ≥ 0.

Proof Suppose x^{2} < 0. Then x^{2} # 0, so x # 0 (using 2.13), so x > 0 or x < 0. In the first case x^{2} > 0. In the second case −x > 0, so (−x)^{2} = x^{2} > 0. Contradiction in both cases, so ¬(x^{2} < 0).

3 The Reals

We give a constructive axiomatization of the reals ℝ. The intention is that the axioms can be instantiated by any specific construction of ℝ. In our axiomatization, the reals form a constructive ordered field, for which Cauchy-completeness and the axiom of Archimedes hold.

Definition 3.1 A structure for real numbers is a constructive abelian ordered field ⟨ℝ, 0, 1, +, ∗, −,^{−1} , =, <, #⟩ that

1. is Cauchy-complete:

∀x_{1}, x_{2}, … (∀ϵ > 0∃N ∈ ℕ∀m > N(−ϵ < x_{m} − x_{N} < ϵ)) → ∃x[x = lim_{n→∞} x_{n}].

2. satisfies the Axiom of Archimedes:

∀x∃n ∈ ℕ[x < n].

Remark 3.2 (to the Definition) In the definition we actually use ℕ to denote both ℕ itself (in 1) as the image of ℕ in ℝ (in 2) via the function f that maps 0 ∈ ℕ to 0 ∈ ℝ and S(x) ∈ ℕ to f(x) + 1. So, in 1, we quantify over the set of functions from ℕ to ℝ. In 2, the axiom really reads ∀x∃n ∈ ℕ[x < f(n)], with f the injection of ℕ into ℝ.

3.1 Properties of the real numbers

Lemma 3.3 There are no non-standard real numbers, i.e.

∀n ∈ ℕ[−\frac{1}{n} < x < \frac{1}{n}] → x = 0,

for all x.

Proof Suppose x # 0 towards a contradiction. (Then ¬(x # 0) and hence x = 0.) Then x^{−1} exists and by the Axiom of Archimedes we find a n ∈ ℕ such that \frac{1}{x} < n. But then either \frac{1}{n} < x or x < \frac{−1}{n} (distinguishing cases according to x > 0 or x < 0 and using Lemma 2.29.

Definition 3.4 A sequence of reals x_{1}, x_{2}, … is called a Cauchy sequence if

∀ϵ > 0∃N ∈ ℕ∀m > N(−ϵ < x_{m} − x_{N} < ϵ).

Lemma 3.5 A sequence of reals x_{1}, x_{2}, … is a Cauchy-sequence iff

∀k ∈ ℕ∃N ∈ ℕ∀m > N(−\frac{1}{k} < x_{m} − x_{N} < \frac{1}{k}).

Proof The implication from left to right is immediate, as \frac{1}{k} > 0. The reverse implication uses the axiom of Archimedes. Assume ∀k ∈ ℕ∃N ∈ ℕ∀m > N(−\frac{1}{k} < x_{m} − x_{N} < \frac{1}{k}). Let ϵ > 0. Then ϵ^{−1} ∈ ℝ, so there is a k ∈ ℕ such that ϵ^{−1} < k and hence ϵ > \frac{1}{k}. Now we find N by our assumption.

Lemma 3.6 Given x, y ∈ ℝ and ϵ > 0, there exists x′ ∈ ℝ such that

−ϵ < x − x′ < ϵ ∧ x′ # y.

Proof y < x+ \frac{ϵ}{2} ∨y > x− \frac{ϵ}{2}. In the first case take x′ := x+ \frac{ϵ}{2}, in the second case take x′ := x− \frac{ϵ}{2}.

We now define the maximum of two real numbers. This is not straightfoward, because we have no trichotomy. (Classically, the maximum can be defined in an ordered field, but constructively that is in general not the case: one needs the Cauchy property.) In a situation where the reals are constructed out of the rationals, say, x = (x_{i})_{i∈ℕ}, one can use the maximum of two rationals (max(x_{i}, y_{i})) to define a Cauchy sequence of the maximum of x and y, namely (max(x_{i}, y_{i})_{i∈ℕ}. Here we can not do that. Instead when defining the maximum of x and y we first have to define an auxiliary sequence of reals (y_{i})_{i∈ℕ} that has y as a limit and such that x # y_{i} for all i.

Definition 3.7 We construct a sequence (y_{i})_{i∈ℕ} such that

∀i ∈ ℕ[−\frac{1}{i} < y − y_{i} < \frac{1}{i} ∧ y_{i} # x].

This is is possible, due to Lemma 3.6. Note that (y_{i})_{i∈ℕ} is a Cauchy sequence and y = lim_{i→∞} y_{i}. Now define the sequence (s_{i})_{i∈ℕ} by

s_{i} := \{ \begin{matrix}x & if & x > y_{i}, \\ y_{i} & if & x < y_{i}, \end{matrix}

Now (s_{i})_{i∈ℕ} is a Cauchy sequence and we define

max(x, y) := lim_{i→∞} s_{i}.

Lemma 3.8 ∀x, y ∈ ℝ[¬(max(x, y) > x ∧ max(x, y) > y)].

Proof From the Definition of max.

Lemma 3.9 max is commutative, i.e. ∀x, y ∈ ℝ[max(x, y) = max(y, x)].

Lemma 3.10 max gives an upperbound, i.e. ∀x, y ∈ ℝ[max(x, y) ≥ x ∧ max(x, y) ≥ y].

Lemma 3.11 max give a least upperbound, i.e. ∀x, y, z ∈ ℝ[z ≥ x ∧ z ≥ y → z ≥ max(x, y)].

Proof Suppose z < max(x, y). Then z < y ∨ y < max(x, y) and z < x ∨ x < max(x, y). If y < max(x, y), then x < max(x, y) contradicts Lemma 3.8, so z < y ∨ z < x, contradicting z ≥ x ∧ z ≥ y. So z ≥ max(x, y).

Lemma 3.12 ∀x, y ∈ ℝ[x ≤ y ↔ max(x, y) = y].

Proof For →: max(x, y) ≥ y by Lemma 3.10 and max(x, y) ≤ y by Lemma 3.11. For ←: suppose x > y. Then x ≥ y and hence max(x, y) = x by the previous. Hence x = y, contradiction. So x ≤ y.

Definition 3.13 For x ∈ ℝ, we define

|x| := max(x, −x).

Lemma 3.14 ∀x ∈ ℝ[x ≥ 0 → |x| = x]. Proof If x ≥ 0, then −x ≤ 0, hence −x ≤ x. So max(x, −x) = x by Lemma 3.12. Lemma 3.15 ∀x, y, r ∈ ℝ[|x − y| ≤ r ↔ x − r ≤ y ≤ x + r]. Proof Immediate using the intermediate equivalent statement x − y ≤ r ∧ −x + y ≤ r. Lemma 3.16 ∀x, y ∈ ℝ[|x + y| ≤ |x| + |y|]. Proof max(x, −x)+max(y, −y) ≥ x+y and max(x, −x)+max(y, −y) ≥ −x−y. Hence |x|+|y| = max(x, −x) + max(y, −y) ≥ max(x + y, −x − y) = |x + y|. Lemma 3.17 ∀x, y, z, r, q ∈ ℝ[|x − y| ≤ r ∧ |y − z| ≤ q → |x − z| ≤ r + q. Proof |x − z| = |x − y + y − z| ≤ |x − y| + |y − z| ≤ r + q. Lemma 3.18 If x_{0}, x_{1}, … and y_{0}, y_{1}, … are Cauchy sequences with limits (respectively) x and y, then

lim_{n→∞} x_{n} + lim_{n→∞} y_{n} = lim_{n→∞}(x_{n} + y_{n}),
( lim_{n→∞} x_{n})( lim_{n→∞} y_{n}) = lim_{n→∞}(x_{n}y_{n}),
| lim_{n→∞} x_{n}| = lim_{n→∞} |x_{n}|,
− lim_{n→∞} x_{n} = lim_{n→∞}(−x_{n}),
( lim_{n→∞} x_{n})^{−1} = lim_{n→∞}(x_{n})^{−1},

where the latter is only defined if ∀i ∈ ℕ[x_{i} # 0]. Furthermore, if x_{i} ≤ y_{i} for all i, then x ≤ y.

In the following, for n ∈ ℕ, y^{n} denotes the n-times multiplication of y. Definition 3.19 For x ≥ 0 and n ∈ ℕ^{+}, we define ^{n} \sqrt{x}. First we notice that (x + 1)^{n} > x (proof by induction on n). Define the sequences (p_{i})_{i∈ℕ} and (q_{i})_{i∈ℕ} as follows.

p_{0} := 0,
q_{0} := x + 1,
p_{i+1} := \{ \begin{matrix}p_{i} & if & (\frac{2p_{i}+q_{i}}{3} )^{n} < x, \\ \frac{2p_{i}+q_{i}}{3} & if & (\frac{p_{i}+2q_{i}}{3} )^{n} > x \end{matrix}
q_{i+1} := \{ \begin{matrix}q_{i} & if & (\frac{p_{i}+2q_{i}}{3} )^{n} > x, \\ \frac{p_{i}+2q_{i}}{3} & if & (\frac{2p_{i}+q_{i}}{3} )^{n} < x \end{matrix}

Then we have the following.

1. ∀i ∈ ℕ[p_{i} < x < q_{i}],

2. ∀i ∈ ℕ[q_{i+1} − p_{i+1} = \frac{2}{3}(q_{i} − p_{i})]. So, (q_{i})_{i∈ℕ} is a Cauchy sequence and we define

n \sqrt{x} := lim_{i→∞} q_{i}.

Lemma 3.20 ∀x ∈ ℝ∀n ∈ ℕ^{+}[x ≥ 0 → ^{n} \sqrt{x} ≥ 0].

Lemma 3.21 ∀x, y ∈ ℝ∀n ∈ ℕ^{+}[x, y ≥ 0 → ^{n} \sqrt{x} ^{n} \sqrt{y} = ^{n} \sqrt{xy}].

Lemma 3.22

∀x∀n ∈ ℕ^{+}[x ≥ 0 → ( ^{n} \sqrt{x})^{n} = x].

Lemma 3.23 If x ≥ 0, then there is a unique y ≥ 0 such that y^{2} = x.

Proof Suppose we have y and z (y, z ≥ 0) such that y^{2} = x = z^{2} and suppose y # z. Using Lemma ?? we conclude that y = z ∨ y = −z, hence y = −z. Also y # 0 ∨ z # 0, so (y > 0 ∧ z < 0) ∨ (y < 0 ∧ z > 0). Contradiction. So y = z.

4 Polynomials

4.1 Definition and general properties

Definition 4.1 For R a ring, we define the set of polynomials over R, R[X], as the finite lists of elements of R. We define the operations +, ∗ and − on R[X]. Let f = ⟨f_{0}, …, f_{n}⟩ and g = ⟨g_{0}, …, g_{m}⟩ be two polynomials Then f+g and f−g are polynomials of length max{m+1, n+1} and f ∗ g is a polynomial of length m + n + 1 defined as follows.

(f + g)_{i} := f_{i} + g_{i} for i ≤ max{m, n},
(f − g)_{i} := f_{i} − g_{i} for i ≤ max{m, n},
(f ∗ g)_{i} := Σ_{j=0}^{i}f_{j} ∗ g(i − j) for i ≤ m + n,

where it is understood that we take f_{j} (resp. g_{j}) to be 0 if j > n (resp. j > m). The zero and unit are defined by

0 := ⟨ ⟩, (the empty sequence),
1 := ⟨1⟩.

The apartness relation on R[X] is defined by

f # g := ∃i(f_{i} # g_{i}).

Note that we use the terminology length of a polynomial when talking about the length of the list of coefficients. The length of a polynomial may not be the same as its degree (defined precisely in 4.2)may be 0.

It is easy to see that

f = g ↔ ∀i(f_{i} = g_{i}).

Definition 4.2 Let f(X) = f_{n}X^{n} + f_{n−1}X^{n−1} + … + f_{1}X + f_{0} be a polynomial.

1. f(X) has degree k, notation deg(f) = k, if k ≤ n, f_{k} # 0 and i = 0 for all i with k < i ≤ n,

2. f(X) has degree at most k, notation deg(f) ≤ k, if k ≤ n, and i = 0 for all i with k < i ≤ n,

3. f(X) has degree at least k, notation deg(f) ≥ k, if k ≤ n, f_{k} # 0.

So, not all polynomials have a degree: ‘degree’ is not a function on polynomials but a relation between polynomials and natural numbers. However, it is always the case that the degree of f(X) = f_{n}X^{n} + f_{n−1}X^{n−1} + … + f_{1}X + f_{0} is at most n, and if we know that f_{k} # 0, it is at least k.

Definition 4.3 A polynomial f(X) = f_{n}X^{n} + f_{n−1}X^{n−1} + … + f_{1}X + f_{0} is called regular if for its leading coefficient one has f_{n} # 0. (That is: the polynomial has a degree, which is the same as its length, n.)

Lemma 4.4 For R a ring, R[X] is a ring.

In the following, unless stated otherwise, R is a ring. Notation 4.5 A polynomial f = ⟨f_{0}, …, f_{n}⟩ will often be denoted by f(X) = f_{n}X^{n}+f_{n−1}X^{n−1}+ … + f_{0} or by f(X) = Σ_{j=0}^{n}f_{j}X^{j}. The multiplication operation ∗ will usually be omitted. Definition 4.6 For every polynomial f(X) = f_{n}X^{n} + f_{n−1}X^{n−1} + … + f_{0} over R we define a function \overline{f} : R → R in the canonical way:

f(a) := f_{n}a^{n} + f_{n−1}a^{n−1} + … + f_{0}.

In the following, we will often just write f for this function \overline{f}.

The following two Lemmas already hold for integral domains (rings with the additional property x # 0 ∧ y # 0 → xy # 0, see Lemma 2.15), but we have not introduced that notion here. Lemma 4.7 Let F be a field and let f = f_{n}X^{n} +…+f_{0} and g = g_{m}X^{m} +…+g_{0} be polynomials over F. Write h_{m+n}X^{m+n} + … + h_{0} for fg. Then

f_{i}g_{j} # 0 → ∃k[i + j ≤ k ≤ n + m ∧ h_{k} # 0].

Proof See [6], p. 417. Theorem 4.8 If F is a field, then F [X] satisfies the integral domain property, i.e. for all f, g ∈ F [X], if f # 0 and g # 0, then fg # 0. Proof Suppose f = f_{n}X^{n}+…+f_{0} # 0 and g = g_{m}X^{m}+…+g_{0} # 0 and let h_{m+n}X^{m+n}+…+h_{0} be fg. Then f_{i}g_{j} # 0 for some i, j, but then h_{k} # 0 for some k.

4.2 Factorization and zeros

Let R be a constructive ring. Lemma 4.9 Let f = f_{n}X^{n} + … + f_{0} and g = g_{m}X^{m} + … + g_{0} be polynomials over R. Then there exist k ∈ ℕ, q, r ∈ R[X] such that

(g_{m})^{k}f(X) = q(X)g(X) + r(X)

and r(X) has length less then m or 0. Proof See [6], p. 418. Theorem 4.10 Let f(X) ∈ R[X] and a ∈ R. Then

∃!q(X) ∈ R[X](f(X) = (X − a)q(X) + f(a)).

Proof By Lemma 4.9, f(X) = q(X)(X − a) + c, for some polynomial q(X) and c ∈ R. By taking the value of the function f in a, we find that c = f(a). Furthermore, q(X) = q_{n−1}X^{n−1} + … + q_{0} and we can determine the coefficients of q(X) uniquely from the equation f(X) = q(X)(X − a) + f(a). Corollary 4.11 For f(X) ∈ R[X] and a ∈ R,

(X − a)|f(X) ↔ f(a) = 0.

Moreover, if f(X) has length n and f has n + 1 zeros, then f = 0.

We now prove that if the polynomial f has degree at least k (n ≥ k > 0) and we are given n + 1 distinct elements (a_{i})_{1≤i≤n+1}, then f(a_{i}) # 0 for one of the i. This will be used to prove the Intermediate Value Theorem for polynomials.

Lemma 4.12 Let f(X), g(X) ∈ R[X], both of length n. Let (a_{i})_{0≤i≤n−1} be distinct elements of R (I.e. a_{i} # a_{j} if i ≠ j.). If f(a_{i}) = g(a_{i}) for all i (0 ≤ i ≤ n − 1), then f = g.

Proof The polynomial h := f − g has length n and has n zeros, so h = 0 by Corollary 4.11. Hence, f = g.

Let F be a constructive field.

Lemma 4.13 Let f(X) ∈ R[X] of length n and let (a_{i})_{1≤i≤n} be distinct elements of R. Then

f(X) = f(a_{1})\frac{(X − a_{2})(X − a_{3}) ⋯ (X − a_{n})}{(a_{1} − a_{2})(a_{1} − a_{3}) ⋯ (a_{1} − a_{n})} +

f(a_{2})\frac{(X − a_{1})(X − a_{3}) ⋯ (X − a_{n})}{(a_{2} − a_{1})(a_{2} − a_{3}) ⋯ (a_{2} − a_{n})} +

⋯

f(a_{n})\frac{(X − a_{1})(X − a_{2}) ⋯ (X − a_{n−1})}{(a_{n} − a_{1})(a_{n} − a_{2}) ⋯ (a_{n} − a_{n−1})}.

Proof The right hand side of the equation is a polynomial h(X) of length n (note that all the fractions are defined, because all a_{i} are distinct). Furthermore f and h agree on all a_{i}, hence f = h by Lemma 4.12.

Lemma 4.14 Let f(X) ∈ R[X] of degree at least k (n ≥ k > 0) and let (a_{i})_{1≤i≤n+1} be distinct elements of R. Then

f(a_{i}) # 0

for some i.

Proof Write f(X) = f_{n}X^{n} + … + f_{0}. By Lemma 4.13 we find that for the coefficient f_{k} we have

f_{k} = Σ_{1≤i≤n+1}f(a_{i})h_{k}^{i},

where h_{k}^{i} is the k-th coefficient of the i-th polynomial as above:

\frac{(X − a_{1}) ⋯ (X − a_{i−1})(X − a_{i+1}) ⋯ (X − a_{n})}{(a_{i} − a_{1}) ⋯ (a_{i} − a_{i−1})(a_{i} − a_{i+1}) ⋯ (a_{i} − a_{n+1})}

As f_{k} # 0, we find that f(a_{i}) # 0 for at least one i.

4.3 Operations on polynomials

We need some formal operations on polynomials. Let F be an ordered field (to make sure that always n! # 0; as ordered field are infinite this is the case).

Definition 4.15 For f(X) = a_{n}X^{n} + a_{n−1}X^{n−1} + … + a_{1}X + a_{0} a polynomial, we define the derivative of f, f′ as follows.

f′(X) := na_{n}X^{n−1} + (n − 1)a_{n−1}X^{n−2} + … + a_{1}.

Taking k-times the deriavtive of f is denoted as f^{(k)}.

Definition 4.16 Let f(x) = a_{n}x^{n} + a_{n−1}x^{n−1} + … + a_{0} be a polynomial over R and c ∈ R. Define the polynomials f~ and f_{c} as follows.

f~(X) = a_{0}X^{n} + … + a_{n−1}X + a_{n},
f_{c}(X) = \frac{f^{(n)}(c)}{n!}X^{n} + \frac{f^{(n−1)}(c)}{(n − 1)!}X^{n−1} + … + \frac{f′(c)}{1!}X + f(c)

Lemma 4.17 Let f(X) = a_{n}X^{n} + a_{n−1}X^{n−1} + … + a_{0} be a polynomial over R and c ∈ R. For the function \overline{f} associated to this polynomial (4.6) we have

\overline{f~}(x) = x^{n}\overline{f}(x^{−1}), if x # 0,

\overline{f~}(0) = a_{n},
\overline{f_{c}}(x) = \overline{f}(x + c).

Proof We informally write f where we refer to the function \overline{f} etcetera.

x^{n}f(\frac{1}{x}) = x^{n}(a_{n}x^{−n} + … + a_{0})
= a_{n} + a_{n−1} + … + a_{0}x^{n}
= f~(x).

Clearly f_{c}(x) is a polynomial of maximal degree n. Hence,

f_{c}(x) = b_{n}x^{n} + … + b_{0}.

It follows that

f(c) = f_{c}(0) = b_{0}, hence b_{0} = f(c),
f′(c) = f′_{c}(0) = b_{1}, hence b_{1} = f′(c)
f^{(2)}(c) = f_{c}^{(2)}(0) = 2!b_{2}, hence b_{2} = \frac{f^{(2)}(c)}{2!}
…
f^{(n)}(c) = f_{c}^{(n)}(0) = n!b_{n}, hence b_{n} = \frac{f^{(n)}(c)}{n!}.

5 Real valued functions

In the proof of the Fundamental Theorem of Algebra, we use a strong version of the Intermediate Value Theorem (with a strong conclusion and a strong premise). This is Theorem 6.1.5 of [5]. Definition 5.1 Intervals (closed and open) in ℝ. Definition 5.2 Continuity of functions f : ℝ^{n} → ℝ (n ∈ ℕ). Lemma 5.3 The identity and a constant function are continuous. Continuity is preserved under +, ∗, composition and maximum (of finitely many functions). Corollary 5.4 If f(X) is a polynomial over ℝ, then the associated function f is continuous. Theorem 5.5 (Intermediate Value Theorem) Let a, b ∈ ℝ, a < b, and let f be continuous on [a, b] with f(a) < 0 < f(b). Moreover assume that

∀x, y ∈ [a, b](x < y → ∃z ∈ [x, y](f(z) # 0)).

Then ∃z ∈ [a, b](f(z) = 0).

Proof See [5], p. 294.

Corollary 5.6 (Intermediate Value Theorem for regular polynomials) Let f be a regular polynomial over ℝ and let a, b ∈ ℝ such that a < b.

If f(a) < 0 and f(b) > 0 then ∃z ∈ [a, b](f(z) = 0).

Proof The premise in Theorem 5.5 is satisfied: if n is the degree of f, we choose n + 1 distinct points in the interval [x, y]; due to Lemma 4.14 the value of f is apart from 0 for one of these points.

Proposition 5.7 (Roots of polynomials over ℝ of odd degree) Every polynomial of odd degree over ℝ has a root.

Proof Let f be a polynomial of odd degree. We only have to show that for x sufficiently small, f(x) < 0 and for x sufficiently large, f(x) > 0. Then Corollary 5.6 does the job. .

Lemma 5.8 (Intermediate Value Theorem for stricly monotonic functions) If f : ℝ→ℝ is strictly monotonic and continuous on some interval I, and a, b ∈ I with a < b, f(a) < 0, f(b) > 0, then there is a c ∈ (a, b) with f(c) = 0.

Proof We show that the premise of Theorem 5.5 is satisfied. Let x, y ∈ [a, b] with x < y. Take z_{1}, z_{2} ∈ [x, y] such that z_{1} < z_{2}. Then f(z_{1}) < f(z_{2}) due to the strict monotonicity of f. Hence f(z_{1}) < 0 ∨ f(z_{2}) > 0.

Definition 5.9 Let n ∈ ℕ, n ≥ 1, a_{1}, …, a_{n} ∈ {x ∈ ℝ|x ≥ 0} with a_{n} = 1. Define m : [0, ∞) → [0, ∞) as follows.

m(s) := max{a_{i}s^{i} | 1 ≤ i ≤ n}.

Lemma 5.10 The function m is strictly monotonic on (0, ∞).

Proof We prove that for every x, y ∈ (0, ∞), if x < y then \frac{m(y)}{m(x)} ≥ \frac{y}{x}. (Then \frac{m(y)}{m(x)} > 1 and hence

m(y) > m(x).) Let x, y ∈ (0, ∞), x < y, and suppose \frac{m(y)}{m(x)} < \frac{y}{x}. Then \frac{x}{y}m(y) < m(x). We conclude that ∀j ∈ \{1, …, n\}(\frac{x}{y}a_{j}y^{j} < m(x)) and hence

∀j ∈ {1, …, n}(a_{j}x^{j} ≠ m(x)).

(If a_{j}x^{j} = m(x), then \frac{x}{y}a_{j}y^{j} < a_{j}x^{j} and y^{j−1} < x^{j−1}, contradiction.) Also

∀j ∈ {1, …, n}(a_{j}x^{j} ≤ m(x)).

From these two, we conclude that

∀j ∈ {1, …, n}(¬¬(a_{j}x^{j} < m(x))).

From Lemma 3.8 we conclude that

¬∀j ∈ {1, …, n}(a_{j}x^{j} < m(x)).

From these two statements we derive a contradiction. (Here we use that the universal quantifier ranges over a finite set.) Viz. Suppose a_{1}x < m(x), a_{2}x^{2} < m(x), …, a_{n}x^{n} < m(x). Then ⊥ using the second. Hence ¬(a_{1}x < m(x)), which contradicts the first, hence ¬(a_{2}x^{2} < m(x)), which contradicts the first, etcetera until we derive ¬(a_{n}x^{n} < m(x)) and a contradiction.

6 Complex numbers

Definition 6.1 A structure for the complex numbers consists of

ℂ = ℝ × ℝ,

where ℝ is a structure for the real numbers. On a structure of the complex numbers one defines

(r, s) +_{ℂ} (r′, s′) = (r + r′, s + s′);
(r, s) ∗_{ℂ} (r′, s′) = (r ∗ r′ − s ∗ s′, r ∗ s′ + r′ ∗ s);
0_{ℂ} = (0, 0);
1_{ℂ} = (1, 0);
i = (0, 1),
(r, s) =_{ℂ} (r′, s′) = r = r′ ∧ s = s′,
(r, s) #_{ℂ} (r′, s′) = r # r′ ∨ s # s′.

Here +, ∗, 0, 1, =, # denote the usual operations and relations on the structure for the reals. Notation 6.2 As a corollary of the definition, an element z = (r, s) ∈ ℂ will also be denoted by r + is. Proposition 6.3 1. With the definitions

−_{ℂ}(r, s) = (−r, −s);
(r, s)^{−1} = (\frac{r}{r^{2} + s^{2}} , \frac{−s}{r^{2} + s^{2}} ).

a structure for the reals becomes a constructive field.

2. Moreover i^{2} = −1.

Let in the following ℂ be a structure for the complex numbers. Definition 6.4 For z = (r, s) ∈ ℂ define

|z| = \sqrt{(r^{2} + s^{2})};
\overline{z} = (r, −s).

Lemma 6.5 For z ∈ ℂ one has

z # 0 ↔ |z| # 0,

where the second # and 0 are taken from the structure of reals. Proposition 6.6 For z_{1}, z_{2} ∈ ℂ one has

\overline{z_{1} ∗_{ℂ} z_{2}} = \overline{z_{1}} ∗_{ℂ} \overline{z_{2}}.
|z_{1} ∗_{ℂ} z_{2}| = |z_{1}| ∗ |z_{2}|.
|z_{1} +_{ℂ} z_{2}| ≤ |z_{1}| + |z_{2}|.

Lemma 6.7 For z_{1}, z_{2} ∈ ℂ one has

\frac{z_{1}}{z_{2}} < 0 → |z_{1} + z_{2}| = |z_{1}| − |z_{2}|,

where the statement \frac{z_{1}}{z_{2}} < 0 denotes that the complex number \frac{z_{1}}{z_{2}} is of the form (r, 0) with r < 0.. Proof |a + b| = |a(1 + \frac{b}{a})| = |a||1 + \frac{b}{a}| = |a|(1 − \frac{b}{a}) = |a| − |b|. Lemma 6.8 For z ∈ ℂ one has

z ∗ \overline{z} = |z|^{2}.

6.1 Roots of complex numbers

We show that for c ∈ ℂ, c # 0 and n ∈ ℕ^{+}, ^{n} \sqrt{c} exists in ℂ. To prove this we rely just on the following two facts: 1. Every positive number in ℝ has a square root, 2. Every polynomial of odd degree over ℝ has a root in ℝ. The proof avoids the use of polar coordinates, exponentials and arctan. We have learned this proof from [2]; thanks to R. Kortram who made us aware of this proof.

Let in the following ℂ be a structure for the complex numbers.

Lemma 6.9 For each c = a + ib ∈ ℂ with c # 0, there exists a solution to z^{2} = c. In particular, a solution is given by:

z = \sqrt{\frac{\sqrt{a^{2} + b^{2}} + a}{2}} + i\sqrt{\frac{\sqrt{a^{2} + b^{2}} − a}{2}}  for b ≥ 0

z = \sqrt{\frac{\sqrt{a^{2} + b^{2}} + a}{2}} − i\sqrt{\frac{\sqrt{a^{2} + b^{2}} − a}{2}}  for b ≤ 0

Proof The second statement, including the fact that all square roots that occur take positive numbers, is a straightforward computation (using that \sqrt{b^{2}} = b when b ≥ 0, and that \sqrt{b^{2}} = −b when b ≤ 0.) For the first statement, because c # 0, we have either a # 0 or b # 0. The second case we explicitly solved, and the first case reduces to the second by multiplying c by i.

Lemma 6.10 Let z, c ∈ ℂ, c # 0, n ∈ ℕ. Then

z^{n} = c ∨ z^{n} = −c,

if the conjunction of the following two equations holds.

(|z|^{2})^{n} = |c|^{2},  (1)
z^{n}c̄ − z̄^{n}c = 0.  (2)

(If n > 0, the first determines a circle in the complex plane, while the second determines a number of lines through the origin.)

Proof Given these two equations, z^{n}c̄ = z̄^{n}c, and so

(z^{n})^{2}c̄ = z^{n}z^{n}c̄ = z^{n}z̄^{n}c = (|z|^{2})^{n}c = |c|^{2}c = c^{2}c̄.

Because c # 0 we can divide by c̄ and hence (z^{n})^{2} = c^{2}. Again because c # 0 from this it follows that z^{n} = c ∨ z^{n} = −c.

Lemma 6.11 For a, b ∈ ℝ, b # 0, n ∈ ℕ,

\frac{(r + i)^{n}(a − ib) − (r − i)^{n}(a + ib)}{2i}

is a polynomial in r of degree n with real coefficients.

Proof This is equal to Im (r + i)^{n}(a − ib), so it will be real. Now (r + i)^{n}(a − ib) clearly has degree n, and because its head coefficient is a − ib and b # 0, its imaginary part will have head coefficient −b, and so it also will have degree n.

Proposition 6.12 For c = a + ib ∈ ℂ, c # 0, and n ∈ ℕ, n odd, there exists a z ∈ ℂ such that z^{n} = c.

Proof We first treat the case that b # 0. Then by Lemma 6.11, f(r) ≡ ((r + i)^{n}(a − ib) − (r − i)^{n}(a + ib))/2i is a polynomial of odd degree with real coefficients. Hence it has a root in ℝ. We now solve the following two equations in x and y.

r = x/y,
(x^{2} + y^{2})^{n} = a^{2} + b^{2}.

From the fact that r is a root of f, by multiplying with 2iy^{n} we find that (x + iy)^{n}(a − ib) − (x − iy)^{n}(a + ib) = 0, and from Lemma 6.10 then (x + iy)^{n} = a + ib ∨ (x + iy)^{n} = −a − ib. In the first case z = x + iy, and in the second case z = −x − iy will be a solution to z^{n} = c.

The case that a # 0 reduces to the other one by multiplying c by i.

Theorem 6.13 For c ∈ ℂ, c # 0 and n ∈ ℕ^{+} there exists an z ∈ ℂ such that z^{n} = c.

Proof This combines the ability to take square and odd roots. Write n as the product of a power of 2 and an odd factor and iterate taking roots. (Note that this uses strong extensionality of taking powers: we need that the result of taking a root is again # 0.)

7 Proof of the Fundamental Theorem of Algebra

Proposition 7.1 (Kneser Lemma) For every n ∈ ℕ, n ≥ 2 there exists a q ∈ ℝ, 0 < q < 1 such that for every polynomial over ℂ with leading coefficient 1

f(x) = x^{n} + b_{n−1}x^{n−1} + … + b_{1}x + b_{0}

one has

∀c > |b_{0}|∃z ∈ ℂ[|z| < c^{1/n} ∧ |f(z)| < qc].

Before proving the Kneser Lemma, we state the so called ‘Main Lemma’ that gives the main ingredients for proving the Kneser Lemma. The advantage of the Main Lemma is that it is just about real numbers; the complex numbers only come in with the Kneser Lemma. There is a ‘Key Lemma’ that proves the Main Lemma. We state the Key Lemma first.

Lemma 7.2 (Key Lemma) For every n ≥ 2, ϵ > 0 and a_{0}, …, a_{n} ≥ 0 with a_{n} = 1, a_{0} > ϵ, there exists

1. t > 0

2. k_{0} ≥ k_{1}, ≥ k_{2} ≥ …,

such that

a_{k_{0}}t^{k_{0}} = a_{0} + ϵ

and moreover for every j, if we let k = k_{j} and r = 3^{−j}t:

a_{k}r^{k} > a_{i}r^{i} − ϵ for all i ∈ {1, …, n}

From the Key Lemma we obtain the Main Lemma

Lemma 7.3 (Main Lemma) For every n ≥ 2, ϵ > 0 and a_{0}, …, a_{n} ≥ 0 with a_{n} = 1, a_{0} > ϵ, there exists

1. k ∈ {1, …, n},

2. r > 0 such that

r^{n} < a_{0},  (3)
a_{k}r^{k} < a_{0},  (4)
3^{−2n^{2}}a_{0} − 2ϵ < a_{k}r^{k},  (5)
∑_{{i=1 \atop i≠k}}^{n} a_{i}r^{i} < (1 − 3^{−n})a_{k}r^{k} + 3^{n}ϵ.  (6)

The Main Lemma is the crucial property about reals to prove the Kneser Lemma.

Proof of the Key Lemma, 7.2 We prove the Key Lemma in a sequence of smaller Lemmata, some specifically related to FTA, some of a more general nature.

Lemma 7.4 For n > 0, a_{1}, …, a_{n} ∈ ℝ and ϵ > 0 there always is a k ∈ {1, …, n} such that for all i ∈ {1, …, n}:

a_{k} > a_{i} − ϵ

Proof Induction with respect to n.

Lemma 7.5 For each sequence k_{0} ≥ k_{1} ≥ k_{2} ≥ … ∈ {1, …, n} there is a j ∈ ℕ with j < 2n such that k_{j−1} = k_{j} = k_{j+1}.

Proof Induction with respect to n.

Lemma 7.6 Let n > 0 and ϵ > 0. Then for every a_{0}, …, a_{n} ≥ 0 with a_{0} > ϵ and a_{n} = 1, there exist t > 0 and k ∈ {1, …, n} such that:

a_{k}t^{k} = a_{0} − ϵ

and such that for all i ∈ {1, …, n}:

a_{i}t^{i} < a_{0}

Proof Start with k = n and t = ^{n} \sqrt{a_{0} − ϵ}. Then consider in turn for i the values n − 1 down to 1. At each i either a_{i}t^{i} < a_{0} or a_{i}t^{i} > a_{0} − ϵ (for the value of t that is current at that time.) In the first case do nothing, but in the second case set k to i and t to ^{i} \sqrt{(a_{0} − ϵ)/a_{i}} (in which case t will decrease.) This will give at the end a suitable k and t.

Proof [of the Key Lemma, 7.2] Let n ≥ 2, ϵ > 0 and a_{0}, …, a_{n} ≥ 0 with a_{n} = 1, a_{0} > 0 be given. Choose t and k_{0} according to Lemma 7.6.

To get k_{j+1} from k_{j}, let k = k_{j}, r = 3^{j}t and apply lemma 7.4 with ϵ/2 to the sequence

a_{1}(r/3), a_{2}(r/3)^{2}, …, a_{k}(r/3)^{k}

to get k′ = k_{j+1}. Then for i ≤ k the inequality for k_{j+1} directly follows, while for i > k we have:

a_{k}(r/3)^{k} = 3^{−k}a_{k}r^{k} > 3^{−k} (a_{i}r^{i} − ϵ) = 3^{−k}a_{i}r^{i} − 3^{−k}ϵ > a_{i}(r/3)^{i} − ϵ/2

and so:

a_{k′}(r/3)^{k′} > a_{k}(r/3)^{k} − ϵ/2 > a_{i}(r/3)^{i} − ϵ

Proof of the Main Lemma, 7.3 We also prove the Main Lemma in a sequence of smaller Lemmata.

Lemma 7.7 For every n ≥ 2, ϵ > 0 and a_{0}, …, a_{n} ≥ 0 with a_{n} = 1, a_{0} > ϵ, if there exist

1. t > 0

2. k_{0} ≥ k_{1}, ≥ k_{2} ≥ …,

such that

a_{k_{0}}t^{k_{0}} = a_{0} + ϵ

and moreover for every j, if we let k = k_{j} and r = 3^{−j}t:

a_{k}r^{k} > a_{i}r^{i} − ϵ for all i ∈ {1, …, n}

then we have for all j, writing again k = k_{j} and r = 3^{−j}t,

r^{n} < a_{0}
a_{k}r^{k} < a_{0}
3^{−jn}a_{0} − 2ϵ < a_{k}r^{k}

Proof We have r ≤ t and so for all i we have a_{i}r^{i} ≤ a_{i}t^{i} < a_{k_{0}}t^{k_{0}} + ϵ = a_{0}. Of this statement r^{n} < a_{0} and a_{k}r^{k} < a_{0} are special cases. Finally, from a_{k_{0}}r^{k_{0}} = 3^{−jk_{0}}a_{k_{0}}t^{k_{0}} ≥ 3^{−jn}a_{k_{0}}t^{k_{0}} = 3^{−jn}(a_{0} − ϵ) > 3^{−jn}a_{0} − ϵ it follows that a_{k}r^{k} > a_{k_{0}}r^{k_{0}} − ϵ > 3^{−jn}a_{0} − 2ϵ.

Lemma 7.8 For every n ≥ 2, ϵ > 0 and a_{0}, …, a_{n} ≥ 0 with a_{n} = 1, a_{0} > ϵ, if there exist

1. t > 0

2. k_{0} ≥ k_{1}, ≥ k_{2} ≥ …,

such that for every j, if we let k = k_{j} and r = 3^{−j}t:

a_{k}r^{k} > a_{i}r^{i} − ϵ for all i ∈ {1, …, n}

then there is a j_{0} < 2n such that, writing k = k_{j_{0}} and r = 3^{−j_{0}}t,

a_{k}(r/3)^{k} > a_{i}(r/3)^{i} − ϵ  for all i ∈ {1, …, n}
a_{k}(3r)^{k} > a_{i}(3r)^{i} − ϵ  for all i ∈ {1, …, n}

Proof From Lemma 7.5 it follows that there is a j_{0} < 2n such that k_{j_{0}−1} = k_{j_{0}} = k_{j_{0}+1}. Writing k for k_{j_{0}}, it immediately follows from k_{j_{0}−1} = k_{j_{0}} and the properties of the k-sequence that a_{k}(3r)^{k} > a_{i}(3r)^{i} − ϵ. Similarly, it follows from k_{j_{0}} = k_{j_{0}+1} and the properties of the k-sequence that a_{k}(r/3)^{k} > a_{i}(r/3)^{i} − ϵ.

Lemma 7.9 For every ϵ > 0, a_{1}, …, a_{n} ≥ 0, k ∈ {1, …, n} and r > 0 such that for all i ∈ {1, …, n}:

a_{k}(r/3)^{k} > a_{i}(r/3)^{i} − ϵ

holds:

∑_{i=1}^{k−1} a_{i}r^{i} < \frac{1}{2}(1 − 3^{−n})a_{k}r^{k} + \frac{1}{2}3^{n}ϵ

Proof From the assumption it follows that

a_{i}r^{i} = 3^{i}a_{i}(r/3)^{i}
< 3^{i}(a_{k}(r/3)^{k} + ϵ)
< 3^{i−k}a_{k}r^{k} + 3^{i}ϵ

and therefore

∑_{i=1}^{k−1} a_{i}r^{i} < ∑_{i=1}^{k−1} (3^{i−k}a_{k}r^{k} + 3^{i}ϵ)

= ( ∑_{i=1}^{k−1} 3^{i−k})a_{k}r^{k} + ( ∑_{i=1}^{k−1} 3^{i})ϵ

= \frac{1}{2}(1 − 3^{1−k})a_{k}r^{k} + \frac{1}{2}(3^{k} − 3^{1})ϵ
< \frac{1}{2}(1 − 3^{−n})a_{k}r^{k} + \frac{1}{2}3^{n}ϵ

Lemma 7.10 For every ϵ > 0, a_{1}, …, a_{n} ≥ 0, k ∈ {1, …, n} and r > 0 such that for all i ∈ {1, …, n}:

a_{k}(3r)^{k} > a_{i}(3r)^{i} − ϵ

holds:

∑_{i=k+1}^{n} a_{i}r^{i} < \frac{1}{2}(1 − 3^{−n})a_{k}r^{k} + \frac{1}{2}3^{n}ϵ

Proof From the assumption it follows that

a_{i}r^{i} = 3^{−i}a_{i}(3r)^{i}
< 3^{−i}(a_{k}(3r)^{k} + ϵ)
< 3^{k−i}a_{k}r^{k} + 3^{−i}ϵ

and therefore

∑_{i=k+1}^{n} a_{i}r^{i} < ∑_{i=k+1}^{n} (3^{k−i}a_{k}r^{k} + 3^{−i}ϵ)

= ( ∑_{i=k+1}^{n} 3^{k−i})a_{k}r^{k} + ( ∑_{i=k+1}^{n} 3^{−i})ϵ

= \frac{3}{2}(3^{−1} − 3^{k−n−1})a_{k}r^{k} + \frac{3}{2}(3^{−k−1} − 3^{−n−1})ϵ
= \frac{1}{2}(1 − 3^{k−n})a_{k}r^{k} + \frac{1}{2}(3^{−k} − 3^{−n})ϵ
< \frac{1}{2}(1 − 3^{−n})a_{k}r^{k} + \frac{1}{2}3^{n}ϵ

Lemma 7.11 For every ϵ > 0, a_{1}, …, a_{n} ≥ 0, k ∈ {1, …, n} and r > 0 such that for all i ∈ {1, …, n}:

a_{k}(r/3)^{k} > a_{i}(r/3)^{i} − ϵ
a_{k}(3r)^{k} > a_{i}(3r)^{i} − ϵ

holds:

∑_{{i=1 \atop i≠k}}^{n} a_{i}r^{i} < (1 − 3^{−n})a_{k}r^{k} + 3^{n}ϵ

Proof This follows immediately from Lemmata 7.9, 7.10.

Proof [of the Main Lemma, 7.3] Take t and k_{0}, k_{1}, … according to the Key Lemma 7.2. According to Lemma 7.8 there is a j_{0} < 2n such that for k = k_{j_{0}} and r = 3^{−j_{0}}t the premises of Lemma 7.11 hold. Hence inequality (6) of the Main Lemma holds:

∑_{{i=1 \atop i≠k}}^{n} a_{i}r^{i} < (1 − 3^{−n})a_{k}r^{k} + 3^{n}ϵ

Then inequalities (3), (4) and (5) are given by lemma 7.7 (the inequality 3^{−2n^{2}}a_{0} < 3^{−j_{0}n}a_{0} holds because j_{0} < 2n).

Proof of the Kneser Lemma, Proposition 7.1 We prove the Kneser Lemma in a sequence of steps. Let n ≥ 2. We will show that

q := 1 − \frac{1}{3^{2n^{2}+n}}

is a good choice for q. Let

f(x) = x^{n} + b_{n−1}x^{n−1} + … + b_{1}x + b_{0}

be a polynomial over ℂ and let c ∈ ℝ^{+} be such that c > |b_{0}|. We want to apply the Main Lemma taking a_{i} := |b_{i}|. However, we don’t know if |b_{0}| # 0. Hence we will approximate b_{0} by a b′_{0} # 0 such that |b_{0} − b′_{0}| is sufficiently small and |b′_{0}| < c. Then we will define the real numbers a_{0}, …, a_{n} by a_{0} := |b′_{0}|, a_{i} := |b_{i}| for 1 ≤ i < n and a_{n} := 1. Now, for a specific choice of z (with |z|^{n} < a_{0}) the Main Lemma will give an approximation of |f(z)| in terms of a_{0} and hence in terms of c. In particular, it will be shown that |f(z)| < qc, with q as above.

Lemma 7.12 Let a_{0}, …, a_{n} ≥ 0 and b_{0}, …, b_{n} ∈ ℂ with a_{i} = |b_{i}| for i = 1, …, n. Furthermore, let k ∈ {1, …, n} and z ∈ ℂ with r = |z|. Then:

| ∑_{i=0}^{n} b_{i}z^{i}| < |b_{0} + b_{k}z^{k}| + ∑_{{i=1 \atop i≠k}}^{n} a_{i}r^{i}

Proof Repeated application of the triangle inquality for the complex numbers.

The Main Lemma will take care that the second term on the right hand side of the conclusion of Lemma 7.12 is sufficiently small. To assure that the first term is also small enough, a specific value of z can be chosen in such a way that b_{0} and b_{k}z^{k} cancel eachother out.

Lemma 7.13 Given a_{0}, a_{k} > 0, b_{0}, b′_{0}, b_{k} ∈ ℂ, k ∈ {1, …, n}, r > 0 and η > 0 such that:

|b′_{0}| = a_{0}
|b_{k}| = a_{k}
|b_{0} − b′_{0}| < η
a_{k}r^{k} < a_{0}

then there exists a z ∈ ℂ such that |z| = r and:

|b_{0} + b_{k}z^{k}| < a_{0} − a_{k}r^{k} + η

Proof Take

z = r ^{k} \sqrt{−\frac{a_{k}}{a_{0}} \frac{b′_{0}}{b_{k}}}

Then we have:

|−\frac{a_{k}}{a_{0}} \frac{b′_{0}}{b_{k}} | = \frac{a_{k} |b′_{0}|}{a_{0} |b_{k}|} = \frac{a_{k}a_{0}}{a_{0}a_{k}} = 1

so

| ^{k} \sqrt{−\frac{a_{k}}{a_{0}} \frac{b′_{0}}{b_{k}}} | = 1

and so |z| = r.

Because a_{k}r^{k} < a_{0} we get |a_{0} − a_{k}r^{k}| = a_{0} − a_{k}r^{k} and therefore

|b′_{0} + b_{k}z^{k}| = |b′_{0} + b_{k}r^{k}( − \frac{a_{k}}{a_{0}} \frac{b′_{0}}{b_{k}} )|
= |\frac{b′_{0}}{a_{0}} (a_{0} − a_{k}r^{k})|
= \frac{|b′_{0}|}{a_{0}}|a_{0} − a_{k}r^{k}|
= a_{0} − a_{k}r^{k}

From this it follows that |b_{0} + b_{k}z^{k}| ≤ |b_{0} + b_{k}z^{k}| + |b_{0} − b′_{0}| < a_{0} − a_{k}r^{k} + η.

Lemma 7.14 For η > 0 and z ∈ ℂ there is a z′ ∈ ℂ with z′ # 0 and |z′ − z| < η.

Proof Because z + η/2 # z − η/2, either z + η/2 # 0 or z − η/2 # 0. For both choices |z′ − z| = η/2 < η.

Lemma 7.15 Let be given b_{0} ∈ ℂ and c ∈ ℝ with |b_{0}| < c. Then there are b′_{0} ∈ ℂ, a_{0} and η > 0 such that:

|b_{0} − b′_{0}| < η  (7)
|b′_{0}| = a_{0}  (8)
a_{0} > 0  (9)
a_{0} + 3η < c  (10)

and an ϵ > 0 such that:

2(3^{n} + 1)ϵ < η  (11)
2ϵ < 3^{−2n^{2}}a_{0}  (12)
ϵ < a_{0}  (13)

Proof Take

η = \frac{1}{4}(c − |b_{0}|)

so |b_{0}| = c − 4η. Then choose an arbitrary b′_{0} # 0 with |b′_{0} − b_{0}| < η and take a_{0} = |b′_{0}|. To see that (10) is satisfied, calculate:

a_{0} = |b′_{0}| ≤ |b′_{0} − b_{0}| + |b_{0}| < η + c − 4η = c − 3η

The existence of a suitable ϵ then follows easily: take ϵ > 0 smaller then min(\frac{η}{2(3^{n}+1)}, \frac{a_{0}}{2 3^{2n^{2}}} ).

Lemma 7.16 For:

q = 1 − 3^{−2n^{2}−n}

we have that q > \frac{1}{2} and because of that inequalities (10) and (11) imply:

qa_{0} + 3^{n}ϵ + ϵ + η < qc

Proof We get

a_{0} + 2 · 3^{n}ϵ + 2ϵ + 2η = a_{0} + 2(3^{n} + 1)ϵ + 2η < a_{0} + η + 2η < c

Using that 1 < 2q, this gives

qa_{0} + 3^{n}ϵ + ϵ + η < qa_{0} + 2q3^{n}ϵ + 2qϵ + 2qη = q(a_{0} + 2 · 3^{n}ϵ + 2ϵ + 2η) < qc

Proof [of the Kneser Lemma, Proposition 7.1] Take b′_{0}, a_{0}, η and ϵ as in lemma 7.15. Take a_{i} = |b_{i}| for i ∈ {1, …, n}. Take r and k as in lemma 7.3. Finally take z as in lemma 7.13.

Then plugging all conditions and results of lemmas 7.3, 7.12, 7.13, 7.15 and 7.16 together we get

r^{n} < a_{0} < c − 3η < c

so

|z| = r < c^{1/n}

and

| ∑_{i=0}^{n} b_{i}z^{i}| < |b_{0} + b_{k}z^{k}| + ∑_{{i=1 \atop i≠k}}^{n} a_{i}r^{i}

< (a_{0} − a_{k}r^{k} + η) + ((1 − 3^{−n})a_{k}r^{k} + 3^{n}ϵ)
= a_{0} − 3^{−n}a_{k}r^{k} + 3^{n}ϵ + η
< a_{0} − 3^{−n}(3^{−2n^{2}}a_{0} − 2ϵ) + 3^{n}ϵ + η
= (1 − 3^{−2n^{2}−n})a_{0} + 3^{n}ϵ + 3^{−n}2ϵ + η
< (1 − 3^{−2n^{2}−n})a_{0} + 3^{n}ϵ + ϵ + η
= qa_{0} + 3^{n}ϵ + ϵ + η
< qc

Fundamental Theorem for regular polynomials

Proposition 7.17 Let f(x) = x^{n} + a_{n−1}x^{n−1} + … + a_{1}x + a_{0}, with a_{i} ∈ ℂ. Then for some z ∈ ℂ one has f(z) = 0.

Proof Let c ∈ ℝ^{+} with c > |a_{0}|. We will construct a Cauchy sequence z_{i} ∈ ℂ such that for all m

1. |f(z_{m})| < q^{m}c

2. |z_{m+1} − z_{m}| ≤ (q^{m}c)^{1/n}

for some q ∈ (0, 1). Then z = lim_{i→∞} z_{i} exists and by continuity of f one has

|f(z)| = lim_{i→∞} |f(z_{i})| ≤ lim_{i→∞} q^{i}c = 0,

so f(z) = 0.

Now, if 1 and 2 are satisfied, then indeed the z_{i} form a Cauchy seqence:

|z_{m+k} − z_{m}| ≤ |z_{m+k} − z_{m+k−1}| + … + |z_{m+1} − z_{m}|
≤ (q^{\frac{m+k−1}{n}} + q^{\frac{m+k−2}{n}} + … + q^{\frac{m}{n}})c^{1/n}
= \frac{q^{\frac{m}{n}} − q^{\frac{m+k}{n}}}{1 − q^{1/n}} c^{1/n}
= q^{\frac{m}{n}} \frac{1 − q^{\frac{k}{n}}}{1 − q^{1/n}} c^{1/n}
≤ q^{\frac{m}{n}} \frac{c^{1/n}}{1 − q^{1/n}} .

By choosing m sufficiently large (n is fixed), this last expression can be made arbitrarily small.

The construction of z_{i} is as follows. Take z_{0} = 0. Then indeed |f(z_{0})| = |f(0)| < q^{0}c. Now suppose z_{m} is defined satisfying 1. Apply the Kneser Lemma to f_{z_{m}} where

f_{z_{m}}(x) = f(x + z_{m})

and taking q^{m}c for c. (Note that f_{z_{m}} has the same degree as f.) We obtain a z such that

|z| < (q^{m}c)^{1/n} ∧ |f_{z_{m}}(z)| < q^{m+1}c.

Now take z_{m+1} = z + z_{m}. Then we have that 1 is valid: |f(z_{m+1})| = |f(z + z_{m})| = |f_{z_{m}}(z)| < q^{m+1}c.

Moreover, we also have 2: |z_{m+1} − z_{m}| = |z| < (q^{m}c)^{1/n}.

Corollary 7.18 1. Every regular polynomial f(x) = a_{n}x^{n} + a_{n−1}x^{n−1} + … + a_{1}x + a_{0} over ℂ has a root.

2. Moreover, such f can be factorized as follows

\overline{f}(x) = a_{n}(x − α_{1}) … (x − α_{n}).

Proof 1. Divide f by a_{n} to obtain a polynomial g with leading coefficient 1, satisfying a_{n}g(x) = f(x). Then any root of g is a root of f.

2. If α_{1} is a root of f, then

f(x) = (x − α_{1})f_{n−1}(x),

by the Remainder Theorem (4.11) with f_{n−1} being equal to a_{n}x^{n−1} +…, hence also regular. By (i) f_{n−1} has a root α_{2} and hence

f_{n−1}(x) = (x − α_{2})f_{n−2}(x).

Continuing this way one obtains

f(x) = (x − α_{1}) … (x − α_{n})a_{n}.

Proposition 7.19 Let f(x) = a_{n}x^{n} + a_{n−1}x^{n−1} + … + a_{1}x + a_{0}, with a_{i} ∈ ℂ. Suppose that a_{k} # 0, for some 0 < k ≤ n. Then f can be factorized as follows in linear factors.

\overline{f}(x) = (β_{1}x − δ_{1}) … (β_{n}x − δ_{n}).

Proof Let f be given. Take a c ∈ ℂ as in Lemma 4.14 such that f(c) # 0 and let g = (f_{c})~. Note that by Lemma 4.17 we have

\overline{g}(y) = y^{n}\overline{f}(c + \frac{1}{y}), for y # 0.

satisfying

\overline{g}(y) = \overline{f}(c)y^{n} + \frac{\overline{f′}(c)}{1!}y^{n−1} + … + \frac{\overline{f^{(n)}}(c)}{n!}.

It follows that g is regular, with leading coefficient \overline{f}(c), and hence by the corollary g is a product

\overline{g}(y) = \overline{f}(c)(y − α_{1}) … (y − α_{n}).  (1)

Now, for x # c,

\overline{f}(x) = \overline{g}(\frac{1}{x − c})(x − c)^{n}
= \overline{f}(c)(\frac{1}{x − c} − α_{1}) … (\frac{1}{x − c} − α_{n})(x − c)^{n}
= \overline{f}(c)(1 − α_{1}(x − c)) … (1 − α_{n}(x − c))
= \overline{f}(c)(1 + c − α_{1}x) … (1 + c − α_{n}x).

So, we are done by taking β_{i} := −\overline{f}(c)α_{i} and δ_{i} := −\overline{f}(c)(1 + c).

Theorem 7.20 Let f(x) = a_{n}x^{n} + a_{n−1}x^{n−1} + … + a_{1}x + a_{0}, with a_{i} ∈ ℂ. Suppose that a_{k} # 0, for some 0 < k ≤ n. Then f can be factorized as follows in linear factors.

\overline{f}(x) = (x − α_{1}) … (x − α_{k})(β_{k+1}x − δ_{k+1}) … (β_{n}x − δ_{n}).

So, in particular, f has k zeros.

Proof From Proposition 7.19 we conclude that

\overline{f}(x) = (β_{1}x − δ_{1}) … (β_{n}x − δ_{n}),

for some β_{i} and δ_{i} in ℂ. We prove by induction on n that at least k of the β_{i} can be chosen apart from 0; hence, by dividing out these factors, we obtain the α_{i}, β_{i} and δ_{i} of the statement.

n = 1 Then f(x) = a_{1}x + a_{0} and a_{1} # 0, so we are done.

n + 1 Now \overline{f}(x) = (β_{1}x − δ_{1}) … (β_{n+1}x − δ_{n+1}). Writing h(x) = (β_{2}x − δ_{2}) … (β_{n+1}x − δ_{n+1}), we find that h is a polynomial of length n, say h(x) = h_{n}x^{n} + … + h_{0}. We find that

a_{k} = β_{1}h_{k−1} − δ_{1}h_{k}.

As a_{k} # 0, we conclude that β_{1}h_{k−1} # 0 or δ_{1}h_{k} # 0. In the first case, β_{1} # 0 and from the induction hypothesis we derive that k − 1 from the β_{2}, …, β_{n} are # 0, so we are done. In the second case, we conclude from the induction hypothesis that k from the β_{2}, …, β_{n} are # 0, so we are done.

References

[1] Heyting, Intuitionism, an introduction, North-Holland, 1956, 133 pp.

[2] J.E. Littlewood, Every polynomial has a root, Journal of the London Math. Soc. 16 (1941), pp. 95 – 98.

[3] Ruitenburg, Intuitionistic Algebra, Theory and Sheaf Models, Ph.D. Thesis, Utrecht University, June 1982, 143 pp.

[4] Mines, Richman and Ruitenburg, A Course in Constructive Algebra, Universitext, Springer-Verlag, 344 pp.

[5] Troelstra and van Dalen, Constructivism in Mathematics, an Introduction, Vol 1, volume 121 in Studies in Logica and The Foundations of Mathematics, North-Holland, 1988, 342 pp.

[6] Troelstra and van Dalen, Constructivism in Mathematics, an Introduction, Vol 2, volume 123 in Studies in Logica and The Foundations of Mathematics, North-Holland, 1988, 879 pp.