Prooftoys real number facts

Contents

Prooftoys / Mathtoys started out with a relatively ad hoc collection of facts about the real numbers, but these are being reorganized to derive everything from an axiomatization of the real numbers as the complete ordered field, the classic characterization of the reals.

Here is a partial list of the number facts that have been proved from the axioms for the real numbers – most of them from the famous “field axioms”. See below for the specific axioms and definitions used.

How to view the proofs

To see the proof of any of these facts to any desired level of detail, click on the text in blue following the statement of the fact. Most of these are just the word “fact”. You can drill down to any level of detail in the same way.

For example let’s look at a proof of item 6 in the main list below. You can see this same proof by clicking on the word “fact” on line 6 of the list of proofs.

Example proof

This is a proof that the negative of zero is zero. It uses the fact that a real number plus its negative is zero, but both of these facts ultimately rely only on standard axioms for the real numbers (the field axioms. It may seem obvious, but we don’t have to just assume it is true. And because it depends only on a handful of carefully-chosen axioms, it can be applied in situations that may be surprising.

Hovering the mouse over a step’s step number gives you some information about how Prooftoys got to that step. For example if you hover the mouse cursor over the [2] in the second step you will see x highlighted everywhere in step 1, and the occurrences of 0 highlighted in step 2 to show that 0 is substituted for x.

If you hover the mouse cursor over the [3] in the third step, you will see the term 0 + -(0) highlighted in step 2. Step 3 applies the fact that 0 + a = 0 to step 2, using -(0) as the value for a, and replacing 0 + -(0) with -(0) to get step 3. (Unless you look into more levels of detail, Prooftoys does not show you that it knows that R 0, which simply means that 0 is a real number.)

To see a level of details behind the operation of step 2, you can click on the words “substitute for x” in the description of step 2. To see the details behind the operation of step 3, click on the word “use”, in blue, in the description of step 3.

Proof list

For a quick start on reading and understanding proofs like these, you may want to get introduced to reading the language and inference in Prooftoys.

Definitions

All of the facts about real numbers rely on these constant definitions.

Except for 0 and 1, the notations for numbers in Prooftoys do not have this sort of definition. Instead, it is appropriate to think of them as shorthands for expressions that build up the appropriate number from 0, 1, addition, and multiplication.

Field axioms

The field axioms here are as stated in the book “Analysis with an Introduction to Proof” by Steven R. Lay. Many important mathematical structures obey the field axioms. In addition to the real numbers, the rational numbers, the complex numbers, and even polynomials follow these laws. Each of these axioms assumes that the variables are elements of the field, in this case the real numbers. There are other possible axiomatizations, all equivalent.

Ordering

Again, each of these axioms assumes that the variables are members of the field, in this case the real numbers. Adding these axioms to the first set makes the domain into an ordered field. Not all fields are ordered.

Effects of addition and multiplication on ordering:

Ordering: more definitions

Dedekind completeness

Upper bounds

Least upper bounds