Real numbers and irrationality

Lens

MotivationH

A diagonal that is not a fraction

Draw a square whose sides are 1 unit long. By the Pythagorean theorem its diagonal $d$ satisfies $d^2 = 1^2 + 1^2 = 2$ , so $d = \sqrt 2$ . How long is that, exactly?

People have asked this for a very long time. A clay tablet from Old Babylonian Mesopotamia (about 1800–1600 BCE, now in the Yale collection as YBC 7289) shows a square with its diagonals and the number $1;24,51,10$ in base sixty — that is, $1 + \tfrac{24}{60} + \tfrac{51}{60^2} + \tfrac{10}{60^3} \approx 1.41421296$ , correct to about six decimal places. The Indian Śulba-sūtras, manuals for building fire altars, give $1 + \tfrac13 + \tfrac{1}{3 \cdot 4} - \tfrac{1}{3 \cdot 4 \cdot 34} = \tfrac{577}{408} \approx 1.4142157$ .

These are superb approximations. But is there a fraction that is exactly $\sqrt 2$ ? In this lesson we prove that there is not — and then ask what kind of number $\sqrt 2$ must be, if not a fraction.

A unit square standing on the number line. Swinging its diagonal down with a compass marks a point at distance $\sqrt 2$ from 0, between 1 and 2. That point is on the line — but, as we will prove, it is not at any fraction.

IntuitionH

Crowded, and still full of holes

The fractions (rational numbers) are packed tightly on the number line. Between any two of them, $a < b$ , lies their average $\tfrac{a + b}{2}$ ; between $a$ and that average lies another; and so on forever. There is no "next" fraction after $1$ , and every tiny interval, however short, contains infinitely many fractions. You met this density in Rational numbers.

So it is natural to guess that the fractions cover the whole line. They do not. The point at distance $\sqrt 2$ from $0$ is surrounded by fractions — $\tfrac75$ , $\tfrac{17}{12}$ , $\tfrac{41}{29}$ , $\tfrac{577}{408}$ , each closer than the last — but none of them lands on it. The fractions are like an infinitely fine sieve: dense, yet full of holes.

The real numbers $\R$ are what we get when we fill in all the holes. Every point of the line is a real number; the rational ones are special, and the others are called irrational.

DefinitionsH

Definitions

Informally, a real number is a point on the number line, or equivalently an infinite decimal such as $3.14159\ldots$ or $-0.5000\ldots$ . (A rigorous construction of $\R$ from $\Q$ is the subject of Constructing ℤ, ℚ and ℝ; here we use the real numbers and their arithmetic and order as familiar, plus one extra property, completeness, stated below.)

Definition— rational and irrational numbers

A real number $x$ is rational if $x = \tfrac{p}{q}$ for some integers $p, q$ with $q \ne 0$ . The set of rational numbers is $\Q$ . A real number that is not rational is irrational.

Definition— absolute value and distance

The absolute value of a real number $x$ is

|x| = \begin{cases} x & \text{if } x \ge 0, \\ -x & \text{if } x < 0. \end{cases}

It is the distance from $x$ to $0$ , and $|x - y|$ is the distance between $x$ and $y$ . Always $|x| \ge 0$ , $|-x| = |x|$ , $|xy| = |x|\,|y|$ and $-|x| \le x \le |x|$ .

Definition— intervals

For real numbers $a < b$ :

Notation	Meaning	Endpoints included?
$(a, b)$	all $x$ with $a < x < b$	neither (open interval)
$[a, b]$	all $x$ with $a \le x \le b$	both (closed interval)
$[a, b)$	all $x$ with $a \le x < b$	only $a$
$(a, \infty)$	all $x$ with $x > a$	— ( $\infty$ is not a number)

An inequality about distance is a statement about an interval: $|x - c| < r$ means $c - r < x < c + r$ , i.e. $x \in (c - r, c + r)$ .

Definition— upper bound and least upper bound

Let $S$ be a set of real numbers. A number $b$ is an upper bound of $S$ if $s \le b$ for every $s \in S$ ; then $S$ is bounded above. A least upper bound (or supremum, $\sup S$ ) is an upper bound $b$ such that no smaller number is an upper bound: if $c < b$ , some element of $S$ is bigger than $c$ .

The supremum need not belong to the set: $\sup\,[0, 1) = 1$ , although $1 \notin [0, 1)$ . A set has at most one least upper bound (if $b$ and $b'$ were both least, then $b \le b'$ and $b' \le b$ ).

Theorem— completeness of ℝ (informal statement)

Every non-empty set of real numbers that is bounded above has a least upper bound in $\R$ .

In this lesson completeness is taken as a basic property of $\R$ — the property that says "there are no holes". (It can be proved, once $\R$ has been built from $\Q$ , for example by Dedekind cuts or Cauchy sequences; Lean's library does exactly that.) The rational numbers satisfy all the usual rules of arithmetic and order, but not completeness — we will prove this below.

Worked examplesH

Worked examples

Example— Decimals and ordering

To compare two decimals, compare digit by digit from the left: $0.3289\ldots < 0.33$ , and $\sqrt 2 = 1.41421\ldots < 1.4143$ . One subtlety: some numbers have two decimal expansions. $0.4999\ldots$ and $0.5000\ldots$ are the same real number, just as $0.999\ldots = 1$ ; this happens exactly for decimals that end in an infinite string of $9$ s. (Why $0.999\ldots = 1$ is proved in Sequences and series: a decimal means a sum of an infinite series.)

Example— A repeating decimal is a fraction

Let $x = 0.272727\ldots$ . Then $100x = 27.272727\ldots$ , and subtracting,

99x = 27, \qquad x = \frac{27}{99} = \frac{3}{11}.

The same trick (multiply by $10^k$ , where $k$ is the length of the repeating block, and subtract) turns every eventually repeating decimal into a fraction. Conversely, long division of $p$ by $q$ can only produce the remainders $0, 1, \dots, q - 1$ ; as soon as a remainder recurs, the digits repeat. So a decimal is rational exactly when it terminates or eventually repeats, and the repeating block of $\tfrac{p}{q}$ has at most $q - 1$ digits. For instance $\tfrac17 = 0.\overline{142857}$ uses all $6$ possible non-zero remainders.

Example— Absolute value inequalities

$|x - 3| \le 2$ means "the distance from $x$ to $3$ is at most $2$ ", i.e. $1 \le x \le 5$ , the interval $[1, 5]$ . And $|2x + 1| > 5$ means $2x + 1 > 5$ or $2x + 1 < -5$ , so $x > 2$ or $x < -3$ : the union $(-\infty, -3) \cup (2, \infty)$ .

Example— Suprema, attained and not

$S = \{1 - \tfrac1n : n = 1, 2, 3, \dots\} = \{0, \tfrac12, \tfrac23, \tfrac34, \dots\}$ . Every element is less than $1$ , so $1$ is an upper bound. If $c < 1$ , choose $n$ with $\tfrac1n < 1 - c$ ; then $1 - \tfrac1n > c$ , so $c$ is not an upper bound. Hence $\sup S = 1$ , and $1 \notin S$ .
$T = [0, 1]$ has $\sup T = 1 \in T$ : here the supremum is the maximum.
$\N = \{0, 1, 2, \dots\}$ is not bounded above, so it has no supremum in $\R$ at all. Completeness only promises suprema for sets that are bounded above.

Example— Rational or irrational?

$\sqrt{49} = 7$ and $\sqrt{\tfrac{9}{4}} = \tfrac32$ are rational.
$\sqrt 2$ , $\sqrt 3$ , $\sqrt{12} = 2\sqrt 3$ are irrational (proved below).
$3 + \sqrt 2$ is irrational: a rational plus an irrational is irrational.
$\sqrt 2 \cdot \sqrt 8 = \sqrt{16} = 4$ is rational, although both factors are irrational.
$\pi$ is irrational (Lambert, 1761) — so $\tfrac{22}{7} = 3.142857\ldots$ and $3.14$ are approximations, not values.

ProofH

Proofs

We start with a fact about parity.

Theorem— Lemma 1 (squares and parity)

For an integer $p$ : if $p^2$ is even, then $p$ is even.

Proof

We prove the contrapositive: if $p$ is odd, then $p^2$ is odd. Write $p = 2k + 1$ . Then $p^2 = 4k^2 + 4k + 1 = 2(2k^2 + 2k) + 1$ , which is odd.

∎

Theorem— Theorem 1 (√2 is irrational)

There are no natural numbers $p, q$ with $q \ne 0$ and $p^2 = 2q^2$ . Consequently $\sqrt 2$ is irrational.

Proof

Suppose, for a contradiction, that there were such pairs. By the well-ordering principle, choose one, $(p, q)$ , in which $q \ge 1$ is as small as possible.

Since $p^2 = 2q^2$ is even, $p$ is even by Lemma 1; write $p = 2k$ . Then $4k^2 = 2q^2$ , so $q^2 = 2k^2$ . Thus $(q, k)$ is another solution of the same equation. Moreover $k \ge 1$ (otherwise $q^2 = 0$ ), and $k < q$ , because $k^2 < 2k^2 = q^2$ . So $(q, k)$ is a solution with a smaller second number than $q$ — contradicting the choice of $(p, q)$ . Hence no solution exists.

Finally, if $\sqrt 2 = \tfrac{a}{b}$ with integers $a, b$ , $b \ne 0$ , then $a^2 = 2b^2$ , and $(|a|, |b|)$ would be a solution in natural numbers with $|b| \ne 0$ . So $\sqrt 2$ is not rational.

∎

This is an argument by infinite descent: any solution would produce a smaller one, and the natural numbers cannot go down forever. (The version you may have seen — "write $\sqrt 2 = \tfrac pq$ in lowest terms; then both $p$ and $q$ are even, a contradiction" — is the same argument: "lowest terms" is where the well-ordering hides.)

What about other square roots? The same descent works for every non-square, with a neat trick that needs no factorisation into primes.

Theorem— Theorem 2 (√n for non-squares)

Let $n$ be a positive integer that is not a perfect square. Then $\sqrt n$ is irrational.

Proof

Since $n$ is not a square, there is an integer $m$ with $m < \sqrt n < m + 1$ (take $m$ the largest integer with $m^2 < n$ ). Suppose $\sqrt n = \tfrac pq$ with $p, q$ positive integers, and choose such a representation with $q$ as small as possible. Put

q' = p - mq, \qquad p' = nq - mp.

These are integers. Since $p = q\sqrt n$ , we have $q' = q(\sqrt n - m)$ , and $0 < \sqrt n - m < 1$ gives $0 < q' < q$ . And

\frac{p'}{q'} = \frac{nq - mp}{p - mq} = \frac{q\sqrt n\,(\sqrt n - m)}{q(\sqrt n - m)} = \sqrt n,

using $n q = \sqrt n \cdot \sqrt n \, q = \sqrt n \, p$ and $mp = m q \sqrt n$ . Since $p' = q'\sqrt n > 0$ , this writes $\sqrt n$ as a fraction of positive integers with the smaller denominator $q' < q$ — a contradiction.

∎

Where does the proof use that $n$ is not a square? In the strict inequalities $m < \sqrt n < m + 1$ , which give $0 < q' < q$ . If $n = k^2$ is a square, then $\sqrt n = k$ is a whole number, no integer $m$ satisfies them, and indeed $\sqrt n = \tfrac k1$ already has the smallest possible denominator.

Theorem— Theorem 3 (rational + irrational)

If $q$ is rational and $x$ is irrational, then $q + x$ is irrational.

Proof

Suppose $q + x = r$ were rational. Then $x = r - q$ is a difference of two rationals, which is rational. That contradicts the irrationality of $x$ .

∎

No such rule holds for two irrationals: $\sqrt 2 + (-\sqrt 2) = 0$ and $\sqrt 2 \cdot \sqrt 2 = 2$ are rational. (Sometimes the answer is irrational, e.g. $\sqrt 2 + \sqrt 3$ — try squaring it — but it has to be checked case by case.)

Theorem— Theorem 4 (triangle inequality)

For all real numbers $x, y$ : $\;|x + y| \le |x| + |y|$ .

Proof

From $-|x| \le x \le |x|$ and $-|y| \le y \le |y|$ , adding gives

-\big(|x| + |y|\big) \le x + y \le |x| + |y|.

A number $t$ with $-c \le t \le c$ satisfies $|t| \le c$ (whichever of $t$ and $-t$ is $|t|$ , it is at most $c$ ). With $t = x + y$ and $c = |x| + |y|$ this is the claim.

∎

In terms of distance, the inequality reads $|a - c| \le |a - b| + |b - c|$ (put $x = a - b$ , $y = b - c$ ): going from $a$ to $c$ via $b$ is never shorter than going directly. That is where the name comes from.

Now the question Chloe asked. Let

S = \{q \in \Q : q^2 < 2\}.

$S$ is non-empty ( $0 \in S$ ) and bounded above by $2$ (if $q > 2$ then $q^2 > 4$ ). The heart of the matter is one clever fraction.

Theorem— Lemma 2 (pushing towards √2)

For a rational $p > 0$ put $p' = \dfrac{2p + 2}{p + 2}$ . Then

p' - p = \frac{2 - p^2}{p + 2} \qquad\text{and}\qquad p'^2 - 2 = \frac{2(p^2 - 2)}{(p + 2)^2}.

So if $p^2 < 2$ , then $p' > p$ and still $p'^2 < 2$ ; if $p^2 > 2$ , then $p' < p$ and still $p'^2 > 2$ .

Proof

Both identities are algebra: $p' - p = \tfrac{2p + 2 - p^2 - 2p}{p + 2} = \tfrac{2 - p^2}{p + 2}$ , and

p'^2 - 2 = \frac{(2p + 2)^2 - 2(p + 2)^2}{(p + 2)^2} = \frac{4p^2 + 8p + 4 - 2p^2 - 8p - 8}{(p + 2)^2} = \frac{2p^2 - 4}{(p + 2)^2}.

Since $p + 2 > 0$ , the signs of $p' - p$ and $p'^2 - 2$ are those of $2 - p^2$ and $p^2 - 2$ .

∎

Theorem— Theorem 5 (ℚ is not complete)

The set $S = \{q \in \Q : q^2 < 2\}$ has no least upper bound in $\Q$ .

Proof

Suppose $b \in \Q$ were a least upper bound of $S$ . Since $1 \in S$ , $b \ge 1 > 0$ . By Theorem 1, $b^2 \ne 2$ . Let $b' = \tfrac{2b + 2}{b + 2}$ , a rational number.

If $b^2 < 2$ : by Lemma 2, $b' > b$ and $b'^2 < 2$ , so $b' \in S$ is bigger than the upper bound $b$ . Impossible.
If $b^2 > 2$ : by Lemma 2, $b' < b$ and $b'^2 > 2$ . Then $b'$ is an upper bound of $S$ : if some $s \in S$ had $s > b'$ , then (as $b' > 0$ ) $s^2 > b'^2 > 2$ , contradicting $s^2 < 2$ . So $b'$ is an upper bound smaller than the least upper bound $b$ . Impossible.

Both cases fail, so no rational least upper bound exists.

∎

In $\R$ , by completeness, $S$ does have a least upper bound $s$ , and $s^2 = 2$ : the argument of Theorem 5 still rules out $s^2 > 2$ , and it rules out $s^2 < 2$ once we add that between $s$ and $s' = \tfrac{2s + 2}{s + 2}$ there is a rational number, which would then lie in $S$ above $s$ . This is how completeness creates $\sqrt 2$ : the hole in $\Q$ is filled by a real number. Lean confirms below that the supremum is exactly $\sqrt 2$ .

Formal mathematicsF

The proofs, checked by Lean

The Lean module for this lesson uses Mathlib, Lean's library of mathematics. In Mathlib, Irrational x is defined to mean " $x$ is not in the image of the map $\Q \to \R$ ", and √2 is Real.sqrt 2.

First the descent of Theorem 1, as a strong induction on $q$ , and the deduction that $\sqrt 2$ is irrational. The second proof writes a rational number $r$ as r.num / r.den (Mathlib keeps rationals in lowest terms with a positive denominator) and passes to absolute values:

no_nat_sq_eq_two_mul_sqLean 4Proved here from basic factsFormally verified

/-- **Infinite descent.** If `p² = 2q²` for natural numbers `p, q`, then `q = 0`.
Proof by strong induction on `q`: `p²` is even, so `p = 2k`; then `4k² = 2q²`, i.e.
`q² = 2k²`, a *new* solution `(q, k)` with `k < q` (if `q > 0`). The induction hypothesis
gives `k = 0`, so `q² = 0` and `q = 0` after all. -/
theorem no_nat_sq_eq_two_mul_sq : ∀ q p : ℕ, p ^ 2 = 2 * q ^ 2 → q = 0 := by
  intro q
  induction q using Nat.strong_induction_on with
  | _ q ih =>
    intro p h
    -- `p²` is even, hence `p` is even: `p = k + k`.
    have hp : Even p := (Nat.even_pow.mp (h ▸ even_two_mul (q ^ 2))).1
    obtain ⟨k, rfl⟩ := hp
    -- Dividing by 2: `q² = 2k²`.
    have h2 : q ^ 2 = 2 * k ^ 2 := by nlinarith
    by_contra hq
    -- The new solution is smaller: `k < q`, because `k² < 2k² = q²`.
    have hk : k < q := by
      have hq0 : 0 < q := Nat.pos_of_ne_zero hq
      have hk0 : 0 < k := by
        rcases Nat.eq_zero_or_pos k with h0 | h0
        · subst h0; simp at h2; omega
        · exact h0
      have : k ^ 2 < q ^ 2 := by nlinarith
      exact lt_of_pow_lt_pow_left₀ 2 (Nat.zero_le q) this
    have hk0 : k = 0 := ih k hk q h2
    subst hk0
    simp at h2
    exact hq h2