Real and Complex Numbers - Metamath Proof Explorer

Contents of this page Axioms for Complex Numbers Past Work Construction The Extended Real Number System The Real Numbers are Uncountable

...my daughters have been studying (chemistry) for several semesters, think they have learned differential and integral calculus in school, and yet even today don't know why x · y = y · x is true. —Edmund Landau

Axioms for Complex Numbers   In the Metamath Proof Explorer (MPE) we derive the postulates or axioms of complex arithmetic as theorems of ZFC set theory. This page collects in one place these results, providing a complete specification of the properties of complex numbers.

To derive the postulates as theorems, we define each of these objects as specific sets, then derive their properties from the axioms of set theory. The derivation is not easy, but the fact that it works is quite remarkable and lends support to the idea that ZFC set theory is all we need to provide a foundation for essentially all of mathematics.

For convenience, after deriving the complex number postulates we re-introduce them as new axioms on top of set theory. This lets us easily identify which axioms are needed for a particular complex number proof, without the obfuscation of the set theory used to derive them. To do this, we introduce two classes ℂ (set of complex numbers) and ℝ (set of real numbers); three constants 0 (zero), 1 (one), and i (imaginary unit, that is, the square root of minus 1); two binary operations + (plus) and · (times); and one binary relation <_ℝ (less than for real numbers). We then assert that these eight objects have the properties specified by the axioms in the table below, as extensions to ZFC set theory. Note that the real number less-than relation <_ℝ is the same as the traditional relation <, but <_ℝ is limited to only comparing real numbers. As always with proven axioms, each new axiom has a name in the form "ax-NAME", and each corresponding proof has a name in the form "axNAME".

In some cases, an alias for an axiom is created so that its name will follow other naming conventions. In these cases, the alias is used from then on. For example, the closure law for addition of complex numbers (axiom 4 of 22) is proven in axaddcl, restated as axiom ax-addcl, and then aliased as addcl so its name follows closure naming conventions; addcl is used from then on. In these cases the axiom's comment is marked with "(New usage is discouraged.)" and identifies its conventional alias. This improves consistency by encouraging proofs to use our conventional aliases.

Many other concepts are derived from the postulates. For example, subtraction and division are introduced later as definitions. We later define natural numbers, integers, and rational numbers as specific subsets of ℂ, leading to the nice relationships ℕ ⊊ ℤ ⊊ ℚ ⊊ ℝ ⊊ ℂ. We later define the set of extended reals (real numbers, positive infinity, and negative infinity), and once those are defined, we define the traditional relation < (less than) over the extended reals by building on the previously-defined relation <_ℝ.

Interestingly, we could eliminate 0 as an axiomatic object by defining it as as ((i · i) + 1) and replacing it with this expression throughout the axioms. If this is done, axiom ax-i2m1 becomes redundant. However, the remaining axioms would become longer and less intuitive.

The following table presents the 22 axioms for complex numbers in the Metamath Proof Explorer, along with some commentary about them:

The 22 Axioms for Complex Numbers

#	Ref	Expression
1	ax-resscn	⊢ ℝ ⊆ ℂ
2	ax-1cn	⊢ 1 ∈ ℂ     Weakened from earlier 1 ∈ ℝ by Eric Schmidt, 11-Apr-2007; see theorem 1re.
3	ax-icn	⊢ i ∈ ℂ
4	ax-addcl	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) ∈ ℂ)
5	ax-addrcl	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 + 𝐵) ∈ ℝ)
6	ax-mulcl	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) ∈ ℂ)
7	ax-mulrcl	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 · 𝐵) ∈ ℝ)
8	ax-mulcom	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 · 𝐵) = (𝐵 · 𝐴))   It is unknown if this can be derived from the other axioms.
9	ax-addass	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 + 𝐵) + 𝐶) = (𝐴 + (𝐵 + 𝐶)))
10	ax-mulass	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → ((𝐴 · 𝐵) · 𝐶) = (𝐴 · (𝐵 · 𝐶)))
11	ax-distr	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ ∧ 𝐶 ∈ ℂ) → (𝐴 · (𝐵 + 𝐶)) = ((𝐴 · 𝐵) + (𝐴 · 𝐶)))
12	ax-i2m1	⊢ ((i · i) + 1) = 0
13	ax-1ne0	⊢ 1 ≠ 0
14	ax-1rid	⊢ (𝐴 ∈ ℝ → (𝐴 · 1) = 𝐴)     Weakened from earlier ax1id (now mulid1) by Eric Schmidt, 19-Jun-2012, with formalization by Scott Fenton, 4-Jan-2013
15	ax-rnegex	⊢ (𝐴 ∈ ℝ → ∃𝑥 ∈ ℝ(𝐴 + 𝑥) = 0)
16	ax-rrecex	⊢ ((𝐴 ∈ ℝ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℝ (𝐴 · 𝑥) = 1)
17	ax-cnre	⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℝ∃𝑦 ∈ ℝ𝐴 = (𝑥 + (𝑦 · i)))
18	ax-pre-lttri	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → (𝐴 <ℝ 𝐵 ↔ ¬ (𝐴 = 𝐵 ∨ 𝐵 <ℝ 𝐴)))   For extended reals see axlttri
19	ax-pre-lttrn	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → ((𝐴 <ℝ 𝐵 ∧ 𝐵 <ℝ 𝐶) → 𝐴 <ℝ 𝐶))   For extended reals see axlttrn
20	ax-pre-ltadd	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ ∧ 𝐶 ∈ ℝ) → (𝐴 <ℝ 𝐵 → (𝐶 + 𝐴) <ℝ (𝐶 + 𝐵)))   For extended reals see axltadd
21	ax-pre-mulgt0	⊢ ((𝐴 ∈ ℝ ∧ 𝐵 ∈ ℝ) → ((0 <ℝ 𝐴 ∧ 0 <ℝ 𝐵) → 0 <ℝ (𝐴 · 𝐵)))   For extended reals see axmulgt0
22	ax-pre-sup	⊢ ((𝐴 ⊆ ℝ ∧ 𝐴 ≠ ∅ ∧ ∃𝑥 ∈ ℝ∀𝑦 ∈ 𝐴𝑦 <ℝ 𝑥) → ∃𝑥 ∈ ℝ(∀𝑦 ∈ 𝐴¬ 𝑥 <ℝ 𝑦 ∧ ∀𝑦 ∈ ℝ(𝑦 <ℝ 𝑥 → ∃𝑧 ∈ 𝐴 𝑦 <ℝ 𝑧)))     This means that a non-empty, bounded-above set of reals has a supremum.   For extended reals see axsup

Colors of variables: wff set class

In case you are wondering: Why do we use (purple) class variables for most postulates instead of more conventional (red) setvar variables? The answer is simply that it's more convenient. In fact, we can equivalently state these with setvar variables only (which would be more in keeping with textbook notation), and then prove these class-variable versions from them. You may want to do that if you want a nice conventional presentation of these axioms for your classroom, book, etc. However, in our formalism, the advantage of a class variable is that we can directly substitute it with another class expression such as the number "2" or the term "((i · 𝑥) + 𝐵)". A setvar variable would require some logic manipulations to do this, using theorems such as vtoclg (as used, for example, to convert elirrv to elirr). So for convenience we use class variables outright. On the other hand, a class variable cannot be quantified with ∀ (for all) and ∃ (there exists), so for axioms with quantifiers, the setvar variables are unavoidable.

The axioms and proven theorems that apply to all sets or classes are not considered axioms for complex numbers, since they apply in other situations as well. For example, there are many general theorems about equality that apply to complex numbers. We separately prove that 𝐴 = 𝐴 in eqid. If 𝐴 = 𝐵, then 𝐵 = 𝐴 per eqcomi, (𝐴𝐹𝐶) = (𝐵𝐹𝐶) per oveq1i, and (𝐶𝐹𝐴) = (𝐶𝐹𝐵) per oveq2i. If 𝐴 = 𝐵 and 𝐵 = 𝐶, then 𝐴 = 𝐶 per eqtri (that is, equality is transitive). Also note that ((𝐴 = 𝐵 ∧ 𝐶 = 𝐷) → (𝐴𝐹𝐶) = (𝐵𝐹𝐷)) as proven in oveq12.

From these axioms many other statements can be proven. For example, 0 ∈ ℂ is proven in 0cn.

Past Work

Most analysis texts construct complex numbers as ordered pairs of reals, leading to construction-dependent properties that satisfy these axioms but are not usually stated as explicit axioms. Other texts state simply that " ℝ is a complete ordered subfield of ℂ," leading to redundant axioms when this phrase is completely expanded out. To our knowledge, the complete set of axioms in the exact form given here has never been published before. That said, Slawomir Kolodynski found a reference with 27 complex number axioms, similar in spirit to Metamath's axioms: Edward V. Huntington, "The fundamental propositions of algebra," Monographs on Topics of Modern Mathematics Relevant to the Elementary Field, edited by I. W. A. Young, New York, 1911; see also Trans. Amer. Math. Soc., vol. VI, 1905, pp. 209—229.]

The original list of complex number axioms was longer. In 2012 Eric Schmidt released "Reductions in Norman Megill's axiom system for complex numbers", available as schmidt-cnaxioms.pdf (schmidt-cnaxioms.tex). This paper showed that several of the original axioms could be weakened (as discussed above). The paper also showed that several of the axioms of the time were redundant (could be derived from the others), e.g., that axaddcom (now addcom) and ax0id (now addid1) are redundant. Scott Fenton later formalized these results within Metamath itself (as proofs of the redundant theorems). Mario Carneiro on 18-Feb-2014 proved that cnex was redundant (it can be proven that the complex numbers are a set). Eric Schmidt presented a proof that the remaining MPE complex number axioms, with the possible exception of ax-mulcom, are independent of the others. These independence proofs have not yet been formalized in Metamath. It is currently an open question if ax-mulcom is independent of the others.

Former Axioms for Complex Numbers

Ref	Expression
axcnex	⊢ ℂ ∈ V     Proved redundant by Mario Carneiro on 18-Feb-2014; see theorem cnex
axaddcom	⊢ ((𝐴 ∈ ℂ ∧ 𝐵 ∈ ℂ) → (𝐴 + 𝐵) = (𝐵 + 𝐴))     Proved redundant by Eric Schmidt, 19-Jun-2012, and formalized by Scott Fenton on 4-Jan-2013; see theorem addcom.
ax0id	⊢ (𝐴 ∈ ℂ → (𝐴 + 0) = 𝐴)     Proved redundant by Eric Schmidt, 19-Jun-2012, and formalized by Scott Fenton on 4-Jan-2013; see theorem addid1
axnegex	⊢ (𝐴 ∈ ℂ → ∃𝑥 ∈ ℂ(𝐴 + 𝑥) = 0)     Proved redundant by Eric Schmidt, 21-May-2007; see theorem cnegex
axrecex	⊢ ((𝐴 ∈ ℂ ∧ 𝐴 ≠ 0) → ∃𝑥 ∈ ℂ(𝐴 · 𝑥) = 1)     Proved redundant by Eric Schmidt, 21-May-2007; see theorem recex
ax0re	⊢ 0 ∈ ℝ     Proved redundant on 19-Feb-2005; see theorem 0re

Colors of variables: wff set class

Construction

To construct the complex numbers, we start with the finite ordinals (natural numbers) of set theory and successively build temporary positive integers, temporary positive rationals, temporary positive reals (based on Dedekind cuts), temporary signed reals, and finally the actual complex numbers. ("Temporary" means they would not normally be used outside of the construction.) Together with the arithmetic operations and other auxilliary sets needed at each level, there are a total of 36 temporary definitions involved. You can look at the Statement List starting at cnpi (click on its "Related theorems" link) to see the theorems used for the construction, which total 254 (including the 22 that result in the final axioms). These theorems are, in essence, the complete formalization of an entire 136-page book, Landau's Foundations of Analysis (a.k.a. Grundlagen der Analysis), although the approach we use is somewhat more modern.

In 2013 Mario Carneiro did a major revision and cleanup of the construction. In particular, rather than using equivalence classes as is customary for the construction of the temporary rationals, he used only "reduced fractions", so that the use of the axiom of infinity is avoided until it becomes necessary for the construction of the temporary reals.

The construction is "portable" in the sense that the final axioms hide how they are constructed, and another construction that develops the same axioms could be used in place of it. For example, another common construction is to define real numbers as Cauchy sequences of rationals instead of the Dedekind cuts that we use.

The Extended Real Number System   A convenient device used in most analysis texts is an extension ℝ^* of the real number system (see df-xr and related theorems) that includes +∞ and -∞.

Analysis textbooks rarely if ever actually define +∞ and -∞ as concrete objects. Instead, they just say that they are two "new" distinguished elements. But we must choose specific sets in order to use set theory to work with them. So we pick 𝒫 ∪ ℂ (the power set of the union of the set of complex numbers) for +∞ (df-pnf) and 𝒫 +∞ for -∞ (df-mnf), which we can prove are different from each other and to not belong to ℝ (see theorems pnfnemnf, pnfnre, and mnfnre). Many other choices are possible too.

In spite of the seemingly awesome "size" of these two new members, they are really nothing deeper than notational devices to make some proofs shorter. Any theorems making use of them can be stated equivalently without them. They provide a shorthand for saying, for example, "no matter how large a number we pick, this series will eventually grow larger than that number." These "infinities" have nothing to do with the infinite cardinals of set theory—in fact one possible choice for -∞ is {ℂ}, which is a singleton with cardinality 1! (We didn't use this simpler choice because its justification requires the Axiom of Regularity, whose use we prefer to avoid when possible.)

Once the extended reals are defined, we can then define the traditional less-than operation < using the relation <_ℝ (less than for real numbers) while accounting for positive and negative infinity. The full definition of < is given in df-ltxr. The complex number axioms, and this new definition, are then used to prove variants of the axioms that can handle the full set of the extended reals; see axlttri, axlttrn, axltadd, axmulgt0, and axsup.

The Real Numbers are Uncountable     In mathematics, a countable set is a set with the same cardinality (number of elements) as the set (or some subset) of the natural numbers. A countable set may be infinite, but every element of the set can be mapped to a unique natural number. The natural numbers and the integers are countably infinite sets. Even the rational numbers are a countably infinite set; see qnnen. In contrast, the real numbers are not a countable set, but instead, they are an uncountable set. This is a remarkable result. The question is, how can this be proved in Metamath?

Norman Megill's initial plan to prove that the rational numbers are uncountable was to formalize Cantor's diagonal argument [external] using decimal (or possibly quaternary) expansions. However, he ran into some technical complications, such as the fact that some numbers have two equivalent decimal representations (e.g. 0.999... = 1.000...), that would have made a formal proof somewhat messy. So he chose another proof that is simpler to formalize but which he believes is in the same spirit as Cantor's diagonal proof, in the sense that it constructs a real number different from all the numbers in a purported list of all real numbers.

Even so, the "simpler" proof is still daunting when worked out in complete formal detail, involving some 39 lemmas. Therefore we will first give an informal description of the proof, then describe the key formal lemmas that lead to the final result, which is theorem ruc (or equivalently ruclem39).

The informal argument    We will start by claiming that we can list all the reals, i.e. that there exists a function f from ℕ (natural numbers) onto ℝ (the reals). We will then proceed to construct a real number that is not in this purported list f(1), f(2), f(3),... of all reals, thereby falsifying this claim.

Here is how we construct this number. We construct, in parallel, two auxiliary sequences g(1), g(2), g(3),... and h(1), h(2), h(3),... derived from f(1), f(2), f(3),...

We start off by assigning:

g(1) = f(1) + 1
h(1) = f(1) + 2

Given g(i) and h(i), we construct the next value g(i+1) and h(i+1) as follows:

If g(i) < f(i+1) < h(i), then assign

g(i+1) = (2· f(i+1) + h(i)) / 3
h(i+1) = (f(i+1) + 2· h(i)) / 3

Otherwise, assign

g(i+1) = (2· g(i) + h(i)) / 3
h(i+1) = (g(i) + 2· h(i)) / 3

In either case, f(i+1) will not fall between g(i+1) and h(i+1).

Now, using elementary algebra, you can check that g(1) < g(2) < g(3) < ... < h(3) < h(2) < h(1). In addition, for each i, the interval between g(i) and h(i) does not contain any of the numbers f(1), f(2), f(3), ..., f(i). This interval keeps getting smaller and smaller as i grows, avoiding all the f(i)'s up to that point. In effect we are constructing an interval of real numbers that are different from all f(i)'s. This is very much like the diagonal argument, but it is much better suited to a formal proof. Just as happens when we add more decimals in Cantor's proof, the sequence g(1), g(2), g(3),... gets closer and closer (converges to) to a real number that is not in the claimed complete listing.

As i goes to infinity, the interval shrinks down to almost nothing. What is left in this shrinking interval? Well, g(i) and h(i) will converge towards each other, from opposite directions, so the interval will shrink down either to a single point or to an empty interval. It is tempting to think that the interval will shrink down to exactly nothing, but in fact it will not be empty, and the formal proof shows this. Specifically, it will contain exactly one real number, which is the supremum (meaning "least upper bound") of all values g(i). How do we know this? Well, it results from one of the axioms for real numbers. This axiom, shown as ax-sup above, says that the supremum of any bounded-above set of real numbers is a real number. And the set of values g(i) is certainly bounded from above; in fact all of them are less than h(1) in particular.

Contrast this to the rational numbers, where the supremum axiom does not hold. That is why this proof fails for the rational numbers, as it should, since we can make a countable list of all rational numbers. To give you a concrete feel for why the supremum axiom fails for rationals, consider the infinite set of numbers 3, 3.1, 3.14, 3.141, 3.1415... Each of these numbers is a rational number. But the supremum is pi, which is not a rational number.

In Cantor's original diagonal proof, the supremum comes into play as follows. As you go diagonally down the list of decimal expansions of real numbers, mismatching the list digit by digit, at each point you will have a new rational number with one more digit (that is different from all numbers in the list up to that point). The supremum of this list of new rational numbers is a real number (with an infinite number of digits after the decimal point) that is not on the list. The statement "all decimal expansions represent real numbers," which is often stated casually and taken for granted, is actually somewhat deep and needs the supremum axiom for its derivation.

The formal proof    The formal proof consists of 39 lemmas, ruclem1 through ruclem39, and the final theorem ruc. In the formal proof, the functions f, g, and h above are called 𝐹, 𝐺, and 𝐻. A function value such as f(1) is expressed (𝐹‘1). A natural number index i is usually expressed as 𝐴; you can tell by the hypothesis 𝐴 ∈ ℕ such as ruclem18.a in ruclem26.

In the hypotheses for many of the lemmas, for example those for ruclem14, we let 𝐹 be any function such that 𝐹:ℕ⟶ℝ, meaning 𝐹 can be any arbitrary mapping from ℕ into ℝ. We then derive additional properties that 𝐹 must have. In particular, we will conclude that no matter what the function 𝐹 is, it is impossible for it to map onto the set of all reals.

We also have to construct the functions 𝐺 and 𝐻, and doing this formally is rather involved. The purpose of the majority of the lemmas, in fact, is simply to work out that the hypotheses of ruclem14 indeed result in functions 𝐺 and 𝐻 that have the properties described in our informal argument section above.

What makes it complicated is the fact that 𝐺 and 𝐻 depend not only on 𝐹 but on each other as well. So, we have to construct them in parallel, and we do this using a "sequence builder" that you can see defined in df-seq. The sequence builder takes in the functions 𝐶 and 𝐷 defined in hypotheses ruclem.1 and ruclem.2 of ruclem14, and uses them to construct a function on ℕ whose values are ordered pairs. The first member of each ordered pair is the value of 𝐺 and the second is the value of 𝐻. By using ordered pairs, the sequence builder can make use of the previous values of both 𝐺 and 𝐻 simultaneously for its internal recursive construction.

The function 𝐶, which provides the second argument or "input sequence" for the sequence builder seq, is constructed from 𝐹 as follows. Its first value (value at 1) is the ordered pair ⟨((𝐹‘1) + 1), ((𝐹‘1) + 2)⟩. This provides the "seed" for the sequence builder, corresponding to the initial assignment to g(1) and h(1) in the informal argument section above. The subsequent values at 2, 3,... are just the values of 𝐹, and these feed the recursion part of the sequence builder to generate new ordered pairs for the values of the sequence builder at 2, 3,....

The two functions called 1^st and 2^nd in hypothesis ruclem.2 of ruclem14 return the first and second members, respectively, of an ordered pair. The if operation, defined by df-if, can be thought of as a conditional expression operator analogous to those used by computer languages. The expression if(𝜑, 𝐴, 𝐵) can be read "if 𝜑 is true then the expression equals 𝐴 else the expression equals 𝐵".

Hypotheses ruclem.3 and ruclem.4 of ruclem14 extract the first and second members from the ordered pair values of the sequence builder finally giving us our desired auxiliary functions 𝐺, and 𝐻

Armed with this information, you should now compare the arithmetic expressions in the hypothesis ruclem.2 of ruclem14 to the ones in the informal argument section above. Hopefully you will see a resemblance, if only a very rough one, that will provide you with a clue should you want to study the formal proof in more depth. By the way, the assertion (conclusion) of ruclem14 shows the first value of the sequence builder. You can see that the ordered pair entries match g(1) and h(1) from the informal argument section above.

Let us now look at the key lemmas for the uncountability proof. Lemma ruclem26 shows that 𝐺 has an ever-increasing set of values, and ruclem27 shows that 𝐻 has an ever-decreasing set of values. In spite of this, the twain shall never meet, as shown by ruclem32. Lemma ruclem34 defines the supremum 𝑆 of the values of 𝐺 (i.e. the supremum of its range) and shows that the supremum is a real number. Lemma ruclem35 shows that the supremum 𝑆 is always sandwiched between 𝐺 and 𝐻, whereas ruclem29 shows that this is not true for any value of 𝐹. Lemma ruclem36 uses these last two facts to show that the supremum is not equal to any value of 𝐹 and therefore not in the list of real numbers provided by 𝐹. This means, as shown by ruclem37, that 𝐹 cannot map onto the set of all reals.

We are now in a position to get rid of most of the hypotheses (since their variables are no longer referenced in the assertion). In ruclem38 we eliminate all but one hypotheses of ruclem37 by using instances of eqid. In ruclem39 we get rid of the final hypothesis (using the weak deduction theorem dedth, involving a quite different application of the if operator) to result in "there is no function mapping ℕ onto the reals," and finally ruc converts this to the notation for a strict dominance relation.

There are several related interesting proofs. There are at least aleph-one reals (aleph1re) and irrationals (aleph1irr). For another very different proof that the reals are uncountable, see rucALT, which follows from the exact computation of the cardinality of reals, rpnnen.