Rational numbers · The Lumenary

Lens

MotivationH

When the integers run out

With the integers you can always add, subtract and multiply. But you cannot always divide.

Three friends in Lagos share 2 litres of zobo, a hibiscus drink. Each gets $2 \div 3$ litres — and no integer is $2 \div 3$ .
An underwater robot surveying a reef off Mombasa sinks from the surface to $-45$ metres in 6 equal stages. Each stage changes its depth by $-45 \div 6$ metres — a negative number that is not a whole number.

To divide freely we need fractions, positive and negative. They raise some surprising questions:

Is there a smallest positive fraction — a number “just after” $0$ ?
Why does $1 \div 7 = 0.142857\,142857\,142857\ldots$ repeat the same six digits for ever?
Is $0.999\ldots$ (nines for ever) a little less than $1$ , or equal to it?
If we mark every fraction on the number line, is the line full?

By the end of this lesson you will be able to answer all four — with proofs.

IntuitionH

Fractions on both sides of zero

You already know fractions such as $\tfrac34$ from fractions and decimals: cut each unit into $4$ equal parts and take $3$ of them. Negative fractions are their mirror images on the other side of zero, exactly as $-3$ mirrors $3$ .

Some rational numbers on the number line: $-\tfrac32$, $-\tfrac23$, $\tfrac14$, $\tfrac34$ and $\tfrac54$. Each is a whole number of equal parts of a unit, counted to the right of $0$ or to the left.

Look between $\tfrac14$ and $\tfrac34$ : there is $\tfrac12$ . Between $\tfrac14$ and $\tfrac12$ : there is $\tfrac38$ . Cutting into smaller and smaller parts, we keep finding new points.

DefinitionsH

Definitions

Definition— rational number

A rational number is a number that can be written as $\dfrac{a}{b}$ , where $a$ and $b$ are integers and $b \neq 0$ . The set of all rational numbers is written $\Q$ (for quotient).

One rational number has many names: $\tfrac12 = \tfrac24 = \tfrac{-3}{-6}$ . The rule for when two names mean the same number is

\frac{a}{b} = \frac{c}{d} \quad\Longleftrightarrow\quad ad = bc \qquad (b, d \neq 0).

(Multiply both sides of $\tfrac ab = \tfrac cd$ by $bd$ to get $ad = bc$ ; divide $ad = bc$ by $bd$ to go back.) For example, $\tfrac{6}{15} = \tfrac25$ because $6 \cdot 5 = 30 = 15 \cdot 2$ .

Signs. $\dfrac{-a}{b} = \dfrac{a}{-b} = -\dfrac{a}{b}$ . We usually make the denominator positive.
Simplest form. A fraction is in simplest form (lowest terms) when $b > 0$ and $a$ and $b$ have no common factor bigger than $1$ . Every rational number has exactly one simplest form; the proof uses facts about primes from divisibility.
Integers are rational. Every integer $n$ equals $\tfrac n1$ , so $\Z \subseteq \Q$ .

The four operations are defined by the familiar fraction rules, now allowing negative numerators:

\frac ab + \frac cd = \frac{ad + bc}{bd}, \qquad \frac ab - \frac cd = \frac{ad - bc}{bd}, \qquad \frac ab \cdot \frac cd = \frac{ac}{bd}.

Definition— reciprocal

The reciprocal of a number $x$ is a number $y$ with $x \cdot y = 1$ . The reciprocal of $\tfrac ab$ (with $a, b \neq 0$ ) is $\tfrac ba$ . Dividing by a non-zero number means multiplying by its reciprocal:

\frac ab \div \frac cd = \frac ab \cdot \frac dc \qquad (c \neq 0).

Definition— terminating and repeating decimals

A decimal terminates if it stops: $0.375 = \tfrac{375}{1000}$ . A decimal eventually repeats if, from some place on, one block of digits repeats for ever. We mark the block with a bar: $0.41\overline{6} = 0.41666\ldots$ and $0.\overline{142857} = 0.142857142857\ldots$

A terminating decimal can be seen as repeating the block $0$ for ever: $0.375 = 0.375\overline{0}$ .

Worked examplesH

Worked examples

Example— Adding and subtracting with negatives

$-\tfrac34 + \tfrac56 = -\tfrac{9}{12} + \tfrac{10}{12} = \tfrac{1}{12}$ .
$\tfrac25 - \tfrac{7}{10} = \tfrac{4}{10} - \tfrac{7}{10} = -\tfrac{3}{10}$ .

As with integers, subtracting means adding the opposite: $\tfrac25 - \tfrac7{10} = \tfrac25 + \left(-\tfrac7{10}\right)$ .

Example— Multiplying and dividing with negatives

$\left(-\tfrac23\right) \cdot \tfrac94 = -\tfrac{18}{12} = -\tfrac32$ . The sign rules are the ones proved in the integers lesson.
$\left(-\tfrac56\right) \div \left(-\tfrac{10}{9}\right) = \left(-\tfrac56\right) \cdot \left(-\tfrac{9}{10}\right) = \tfrac{45}{60} = \tfrac34$ .
The robot: $-45 \div 6 = -\tfrac{45}{6} = -\tfrac{15}{2} = -7.5$ metres per stage.

Example— Dividing by a half doubles

$3 \div \tfrac12 = 3 \cdot 2 = 6$ . It makes sense: “how many halves fit into $3$ ?” Six. Dividing by a number between $0$ and $1$ makes a positive number bigger.

Example— Fractions to decimals

$\tfrac38$ : since $8 \cdot 125 = 1000$ , $\tfrac38 = \tfrac{375}{1000} = 0.375$ . It terminates.
$\tfrac{5}{12}$ by long division. Keep track of the remainders:
- $50 = 4 \cdot 12 + 2$ : digit $4$ , remainder $2$ ;
- $20 = 1 \cdot 12 + 8$ : digit $1$ , remainder $8$ ;
- $80 = 6 \cdot 12 + 8$ : digit $6$ , remainder $8$ — the same remainder again!
From now on every step is the same, so $\tfrac{5}{12} = 0.41\overline{6}$ .

Example— Non-examples

The decimal $0.101001000100001\ldots$ (one more $0$ each time) never settles into a repeating block, so — by a theorem below — it is not a rational number.
$\sqrt2$ and $\pi$ are not rational numbers. For $\sqrt2$ we prove it in this lesson; for $\pi$ the proof (Lambert, 1761) is harder.

ProofH

The main results, with proofs

Theorem— Theorem 1 (closure)

If $x$ and $y$ are rational, then so are $x + y$ , $x - y$ and $xy$ , and so is $x \div y$ if $y \neq 0$ .

Proof

Write $x = \tfrac ab$ and $y = \tfrac cd$ with integers $a, b, c, d$ and $b, d \neq 0$ . Then

x + y = \frac{ad + bc}{bd}, \qquad x - y = \frac{ad - bc}{bd}, \qquad xy = \frac{ac}{bd}.

The numerators and denominators are integers, and $bd \neq 0$ because a product of non-zero integers is non-zero. If $y \neq 0$ , then $c \neq 0$ (otherwise $y = \tfrac 0d = 0$ ), so $x \div y = \tfrac{ad}{bc}$ with $bc \neq 0$ .

∎

Theorem— Theorem 2 (reciprocals)

Every non-zero rational number has a reciprocal that is also rational. The number $0$ has no reciprocal.

Proof

If $x = \tfrac ab \neq 0$ then $a \neq 0$ , so $\tfrac ba$ is a rational number, and $\tfrac ab \cdot \tfrac ba = \tfrac{ab}{ba} = 1$ . For $0$ : every $y$ has $0 \cdot y = 0 \neq 1$ .

∎

This fills the empty box from the integers lesson, where only $1$ and $-1$ had reciprocals. A number system in which you can add, subtract, multiply, and divide by anything non-zero, with the usual rules, is called a field — $\Q$ is the first field most people meet.

Theorem— Theorem 3 (density)

If $p$ and $q$ are rational numbers with $p < q$ , then their average $m = \tfrac{p + q}{2}$ is rational and $p < m < q$ .

Proof

$m$ is rational by closure. From $p < q$ , adding $p$ to both sides gives $2p < p + q$ , so $p < \tfrac{p+q}2$ . Adding $q$ instead gives $p + q < 2q$ , so $\tfrac{p+q}2 < q$ .

∎

So there is no smallest positive rational number (question 1): if $r > 0$ were the smallest, then $\tfrac r2$ would be a smaller positive rational. Repeating the averaging shows there are infinitely many rationals between any two.

Theorem— Theorem 4 (decimals of fractions repeat)

Let $a \ge 0$ and $b > 0$ be integers. The decimal expansion of $\tfrac ab$ either terminates or eventually repeats. If it does not terminate, the repeating block has at most $b - 1$ digits.

Proof

In long division by $b$ , each step takes the current remainder $r$ , with $0 \le r < b$ , and divides $10r$ by $b$ : $10r = (\text{digit}) \cdot b + (\text{new remainder})$ . The next digit and the next remainder depend only on $r$ .

There are only $b$ possible remainders: $0, 1, \ldots, b - 1$ . So among the first $b + 1$ remainders, two must be equal — this is the pigeonhole principle: $b + 1$ pigeons in $b$ holes means some hole holds two. Once a remainder comes back, the computation from that point on is an exact copy of what happened after its first appearance, so the digits repeat (question 2).

If the remainder $0$ ever appears, all later digits are $0$ and the decimal terminates. Otherwise only the $b - 1$ remainders $1, \ldots, b - 1$ occur, so a repeat happens within $b - 1$ steps and the block has at most $b - 1$ digits.

∎

For $\tfrac17$ the block has the largest length allowed, $7 - 1 = 6$ : all six non-zero remainders appear before one repeats.

Theorem— Theorem 5 (which fractions terminate)

A fraction $\tfrac ab$ in simplest form has a terminating decimal exactly when $b$ has no prime factors other than $2$ and $5$ .

Proof

If $b = 2^m 5^n$ , let $k$ be the larger of $m$ and $n$ . Then $b \cdot 2^{k-m} 5^{k-n} = 2^k 5^k = 10^k$ , so $\tfrac ab = \tfrac{a \cdot 2^{k-m}5^{k-n}}{10^k}$ , which terminates after $k$ places.

Conversely, if $\tfrac ab = \tfrac{N}{10^k}$ for an integer $N$ , then $a \cdot 10^k = N b$ , so $b$ divides $a \cdot 10^k$ . Since $a$ and $b$ have no common factor, $b$ must divide $10^k$ (this step is Euclid's lemma about primes). The only prime factors of $10^k = 2^k 5^k$ are $2$ and $5$ , so the same is true of $b$ .

∎

Theorem— Theorem 6 (repeating decimals are fractions)

Every terminating or eventually repeating decimal is a rational number.

Proof

A terminating decimal with $k$ places is an integer divided by $10^k$ . Now take a purely repeating decimal, say $x = 0.\overline{27}$ . Shifting the decimal point two places gives $100x = 27.\overline{27} = 27 + x$ , so $99x = 27$ and $x = \tfrac{27}{99} = \tfrac3{11}$ . In general, if $x = 0.\overline{d_1 d_2 \ldots d_k}$ and $D$ is the whole number $d_1 d_2 \ldots d_k$ , then $10^k x = D + x$ , so

x = \frac{D}{10^k - 1}.

If some digits come before the block, as in $y = 0.41\overline{6}$ , first shift them past the point: $100y = 41.\overline6 = 41 + \tfrac69$ , so $y = \tfrac{41 + 2/3}{100} = \tfrac{125}{300} = \tfrac5{12}$ . By closure, the result is always rational.

∎

Note

“Shift the point and subtract the infinite tail” treats an infinite decimal as a number. That is justified once we define an infinite decimal to mean the number its finite truncations $0.2,\ 0.27,\ 0.272,\ \ldots$ approach — the subject of sequences and series. Here we use it as known.

Theorem— Theorem 7

$0.999\ldots = 1$ .

Proof

Theorem 6 with $D = 9$ and $k = 1$ gives $x = \tfrac{9}{10 - 1} = 1$ . Here is a second argument that avoids shifting an infinite decimal. The number with $n$ nines, $0.99\ldots9$ , equals $1 - \tfrac{1}{10^n}$ . If $0.999\ldots$ were less than $1$ , the gap $d = 1 - 0.999\ldots$ would be a positive number. But $0.999\ldots$ is at least $0.99\ldots9$ for every $n$ , so $d \le \tfrac{1}{10^n}$ for every $n$ . That is impossible for a positive $d$ : choose $n$ so large that $10^n > \tfrac1d$ . So the gap is $0$ (question 3).

∎

$0.999\ldots$ and $1$ are two names for the same number, just as $\tfrac12$ and $\tfrac24$ are. In fact, every terminating decimal other than $0$ has a second name ending in nines: $0.5 = 0.4999\ldots$

ExplanationH

A gap in the rational line

Now question 4. Draw a square with sides of length $1$ . By the Pythagorean theorem its diagonal $d$ satisfies $d^2 = 1^2 + 1^2 = 2$ . Swing the diagonal down onto the number line with a compass: it marks a real point, $\sqrt 2 \approx 1.414$ . Is that point one of the fractions?

Theorem— Theorem 8 (√2 is irrational)

There is no rational number whose square is $2$ .

Proof

Suppose, for contradiction, that $\left(\tfrac ab\right)^2 = 2$ with $\tfrac ab$ in simplest form. Then $a^2 = 2b^2$ , so $a^2$ is even. If $a$ were odd, $a^2 = a \cdot a$ would be odd (odd times odd is odd); so $a$ is even, say $a = 2c$ . Then $4c^2 = 2b^2$ , so $b^2 = 2c^2$ , which is even, so $b$ is even too. But then $2$ is a common factor of $a$ and $b$ , contradicting simplest form. So no such fraction exists.

∎

So even after every fraction is marked, the number line has a hole at $\sqrt2$ — and, it turns out, infinitely many other holes ( $\sqrt3$ , $\pi$ , …). The rationals are dense (no interval is free of them) but not complete (they have gaps). Filling the gaps gives the real numbers.

Formal mathematicsF

Rational numbers in Lean

Core Lean already contains the rational numbers as the type Rat. Each value is stored in simplest form: an integer numerator, a positive denominator, and a proof that they share no factor. We start with the lesson's definition and check that Lean's Rat matches it.

IsQuotientLean 4Formally verified

/-- A number `x` is a *quotient of integers* if `x = m / n` for some integers `m` and `n`
with `n ≠ 0`. This is the lesson's definition of a rational number. -/
def IsQuotient (x : Rat) : Prop := ∃ m n : Int, n ≠ 0 ∧ x = (m : Rat) / (n : Rat)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

every_rat_is_quotientLean 4Applies a library theoremFormally verified

/-- Every value of Lean's type `Rat` is a quotient of integers: `q = q.num / q.den`.
So Lean's `Rat` really is the set of fractions of the lesson. This applies the core lemmas
`Rat.num_divInt_den` and `Rat.divInt_eq_div`. -/
theorem every_rat_is_quotient (q : Rat) : IsQuotient q := by
  refine ⟨q.num, (q.den : Int), ?_, ?_⟩
  · exact Int.ofNat_ne_zero.mpr q.den_nz
  · rw [← Rat.divInt_eq_div]
    exact (Rat.num_divInt_den q).symm

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

Closure. The addition formula, and closure under addition and division, mirror the proof of Theorem 1. A few routine algebra steps are closed by grind, Lean's built-in automatic prover, which knows the rules of fraction arithmetic.

add_formulaLean 4Proved here from basic factsFormally verified

/-- The rule for adding fractions: `a/b + c/d = (a·d + b·c)/(b·d)` when `b, d ≠ 0`.
Rewrite both fractions over the common denominator `b·d`, then add the numerators. -/
theorem add_formula (a b c d : Int) (hb : b ≠ 0) (hd : d ≠ 0) :
    (a : Rat) / b + (c : Rat) / d = ((a * d + b * c : Int) : Rat) / ((b * d : Int) : Rat) := by
  have hb' := int_cast_ne_zero hb
  have hd' := int_cast_ne_zero hd
  push_cast
  calc (a : Rat) / b + (c : Rat) / d
      = (a * d) / (b * d) + (b * c) / (b * d) := by grind
    _ = (a * d + b * c) / (b * d) := by grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

closed_addLean 4Proved here from basic factsFormally verified

/-- **Closure under addition.** The sum of two quotients of integers is a quotient of
integers: the witness is the numerator `a·d + b·c` over the denominator `b·d` from
`add_formula`, and `b·d ≠ 0` because neither factor is zero. -/
theorem closed_add {x y : Rat} (hx : IsQuotient x) (hy : IsQuotient y) :
    IsQuotient (x + y) := by
  obtain ⟨a, b, hb, rfl⟩ := hx
  obtain ⟨c, d, hd, rfl⟩ := hy
  exact ⟨a * d + b * c, b * d, Int.mul_ne_zero hb hd, add_formula a b c d hb hd⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

closed_divLean 4Proved here from basic factsFormally verified

/-- **Closure under division by a non-zero number.** If `y = c/d ≠ 0` then `c ≠ 0`, and
`(a/b) ÷ (c/d) = (a/b)·(d/c) = (a·d)/(b·c)`: divide by multiplying by the reciprocal. -/
theorem closed_div {x y : Rat} (hx : IsQuotient x) (hy : IsQuotient y) (hy0 : y ≠ 0) :
    IsQuotient (x / y) := by
  obtain ⟨a, b, hb, rfl⟩ := hx
  obtain ⟨c, d, hd, rfl⟩ := hy
  have hb' := int_cast_ne_zero hb
  have hd' := int_cast_ne_zero hd
  have hc : c ≠ 0 := by
    intro hc
    apply hy0
    subst hc
    simp [Rat.div_def]
  have hc' := int_cast_ne_zero hc
  refine ⟨a * d, b * c, Int.mul_ne_zero hb hc, ?_⟩
  push_cast
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

Reciprocals. First our own proof of Theorem 2, then the one-line version that applies core Lean's library theorem Rat.mul_inv_cancel, then the fact that $0$ has no reciprocal, and division by a half.

mul_reciprocalLean 4Proved here from basic factsFormally verified

/-- The reciprocal of `a/b` is `b/a`: if `a, b ≠ 0` then `(a/b)·(b/a) = (a·b)/(b·a) = 1`. -/
theorem mul_reciprocal (a b : Int) (ha : a ≠ 0) (hb : b ≠ 0) :
    ((a : Rat) / b) * ((b : Rat) / a) = 1 := by
  have ha' := int_cast_ne_zero ha
  have hb' := int_cast_ne_zero hb
  calc ((a : Rat) / b) * ((b : Rat) / a)
      = ((a : Rat) * b) / ((b : Rat) * a) := by grind
    _ = 1 := by grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

reciprocal_existsLean 4Applies a library theoremFormally verified

/-- Every non-zero rational number has a multiplicative inverse in `Rat`, unlike in `Int`
(where only `1` and `-1` do). This applies core Lean's `Rat.mul_inv_cancel`. -/
theorem reciprocal_exists (q : Rat) (hq : q ≠ 0) : ∃ r : Rat, q * r = 1 :=
  ⟨q⁻¹, Rat.mul_inv_cancel q hq⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

zero_no_reciprocalLean 4Proved here from basic factsFormally verified

/-- Zero has no reciprocal: `0 · r = 0 ≠ 1` for every `r`. -/
theorem zero_no_reciprocal : ¬ ∃ r : Rat, 0 * r = 1 := by
  intro ⟨r, h⟩
  rw [Rat.zero_mul] at h
  exact absurd h (by decide)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

div_halfLean 4Proved here from basic factsFormally verified

/-- Dividing by `1/2` doubles: `x ÷ (1/2) = 2x`. Division is multiplication by the reciprocal,
and the reciprocal of `1/2` is `2`. -/
theorem div_half (x : Rat) : x / (1 / 2) = 2 * x := by
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

Density (Theorem 3), following the human proof line by line:

average_betweenLean 4Proved here from basic factsFormally verified

/-- If `a < b` then the average `(a + b)/2` lies strictly between them:
`a = (a + a)/2 < (a + b)/2 < (b + b)/2 = b`. -/
theorem average_between {a b : Rat} (h : a < b) : a < (a + b) / 2 ∧ (a + b) / 2 < b := by
  have two_pos : (0 : Rat) < 2 := by decide
  constructor
  · -- `a < (a + b)/2` is the same as `a · 2 < a + b`, i.e. `a + a < a + b`.
    rw [Rat.lt_div_iff two_pos]
    have : a + a < a + b := Rat.add_lt_add_left.mpr h
    grind
  · -- `(a + b)/2 < b` is the same as `a + b < b · 2`, i.e. `a + b < b + b`.
    rw [Rat.div_lt_iff two_pos]
    have : a + b < b + b := Rat.add_lt_add_right.mpr h
    grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

exists_betweenLean 4Proved here from basic factsFormally verified

/-- **Density of the rationals.** Between any two different rationals there is a third, so no
rational number has a "next" one. The witness is the average (`average_between`). -/
theorem exists_between {a b : Rat} (h : a < b) : ∃ c : Rat, a < c ∧ c < b :=
  ⟨(a + b) / 2, average_between h⟩

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

Decimals by long division (Theorem 4). We define the remainders and digits of long division, prove that the $k$ -th remainder is $a \cdot 10^k$ modulo $b$ , prove the pigeonhole principle, and conclude that the digits are eventually periodic with period at most $b$ .

remLean 4Formally verified

/-- The remainders in the long division of `a` by `b`. Start with `a % b`; at each step
"bring down a zero": multiply the remainder by `10` and take the remainder on division by `b`. -/
def rem (a b : Nat) : Nat → Nat
  | 0 => a % b
  | k + 1 => (10 * rem a b k) % b

Axioms used: No axiomsformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

digitLean 4Formally verified

/-- The digit produced at step `k + 1` of the long division of `a` by `b`: how many times `b`
goes into ten times the current remainder. `digit a b 0` is the first digit after the point. -/
def digit (a b k : Nat) : Nat := (10 * rem a b k) / b

Axioms used: No axiomsformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

rem_eqLean 4Proved here from basic factsFormally verified

/-- The `k`-th remainder is the remainder of `a · 10^k` on division by `b`: long division
really is computing `a · 10^k` modulo `b`. Proof by induction, using `(x % b) · 10 ≡ x · 10`. -/
theorem rem_eq (a b k : Nat) : rem a b k = a * 10 ^ k % b := by
  induction k with
  | zero => simp [rem]
  | succ k ih =>
    rw [rem, ih, Nat.mul_mod, Nat.mod_mod, ← Nat.mul_mod, Nat.pow_succ]
    congr 1
    rw [Nat.mul_comm 10, Nat.mul_assoc]

Axioms used: propextformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

rem_periodicLean 4Proved here from basic factsFormally verified

/-- Once a remainder repeats, everything after it repeats: each remainder is computed from the
one before, so if `rem i = rem j` then `rem (i + n) = rem (j + n)` for every `n`. -/
theorem rem_periodic (a b : Nat) {i j : Nat} (h : rem a b i = rem a b j) :
    ∀ n, rem a b (i + n) = rem a b (j + n) := by
  intro n
  induction n with
  | zero => exact h
  | succ n ih =>
    rw [← Nat.add_assoc, ← Nat.add_assoc, rem, rem, ih]

Axioms used: No axiomsformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

pigeonholeLean 4Proved here from basic factsFormally verified

/-- **The pigeonhole principle** for the values `f 0, f 1, …, f b`: if all `b + 1` of them are
less than `b`, two of them are equal. Proof by induction on `b`: either `f (b + 1)` already
appeared, or we relabel the value `b` as `f (b + 1)` and use the induction hypothesis. -/
theorem pigeonhole : ∀ (b : Nat) (f : Nat → Nat), (∀ k, k ≤ b → f k < b) →
    ∃ i j, i < j ∧ j ≤ b ∧ f i = f j := by
  intro b
  induction b with
  | zero =>
    intro f hf
    exact absurd (hf 0 (Nat.le_refl 0)) (Nat.not_lt_zero _)
  | succ b ih =>
    intro f hf
    by_cases hrep : ∃ k, k ≤ b ∧ f k = f (b + 1)
    · obtain ⟨k, hk, hfk⟩ := hrep
      exact ⟨k, b + 1, by omega, Nat.le_refl _, hfk⟩
    · -- `f (b + 1)` is new. Replace the value `b` (if it occurs) by `f (b + 1)`.
      have hnew : ∀ k, k ≤ b → f k ≠ f (b + 1) := fun k hk h => hrep ⟨k, hk, h⟩
      let g : Nat → Nat := fun k => if f k = b then f (b + 1) else f k
      have hg : ∀ k, k ≤ b → g k < b := by
        intro k hk
        have h1 := hf k (by omega)
        have h2 := hf (b + 1) (Nat.le_refl _)
        have h3 := hnew k hk
        simp only [g]
        split <;> omega
      obtain ⟨i, j, hij, hjb, hgij⟩ := ih g hg
      refine ⟨i, j, hij, by omega, ?_⟩
      have hi := hnew i (by omega)
      have hj := hnew j hjb
      simp only [g] at hgij
      split at hgij <;> split at hgij <;> omega

Axioms used: propext, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

remainder_repeatsLean 4Proved here from basic factsFormally verified

/-- In the long division of `a` by `b > 0`, some remainder repeats within the first `b + 1`
steps: the remainders take at most `b` values (`rem_lt`), so `pigeonhole` applies. -/
theorem remainder_repeats (a b : Nat) (hb : 0 < b) :
    ∃ i j, i < j ∧ j ≤ b ∧ rem a b i = rem a b j :=
  pigeonhole b (rem a b) (fun k _ => rem_lt a b k hb)

Axioms used: propext, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

decimal_eventually_periodicLean 4Proved here from basic factsFormally verified

/-- **The decimal expansion of `a/b` is eventually periodic.** There is a starting place `i`
and a period `p` with `1 ≤ p ≤ b` such that the digits repeat with period `p` from place `i`
on. (A terminating decimal is the case where the repeating block is `0`.) -/
theorem decimal_eventually_periodic (a b : Nat) (hb : 0 < b) :
    ∃ i p, 0 < p ∧ p ≤ b ∧ ∀ n, digit a b (i + p + n) = digit a b (i + n) := by
  obtain ⟨i, j, hij, hjb, h⟩ := remainder_repeats a b hb
  refine ⟨i, j - i, by omega, by omega, ?_⟩
  intro n
  have hji : i + (j - i) = j := by omega
  unfold digit
  rw [hji, rem_periodic a b h.symm n]

Axioms used: propext, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

one_seventh_digitsLean 4Proved here from basic factsFormally verified

/-- The first twelve digits of `1/7 = 0.142857142857…`, computed by the long-division
definitions above and checked by evaluation. -/
theorem one_seventh_digits :
    (List.range 12).map (digit 1 7) = [1, 4, 2, 8, 5, 7, 1, 4, 2, 8, 5, 7] := by
  decide

Axioms used: No axiomsformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

Back to fractions, and $0.999\ldots$ (Theorems 6 and 7). Again we prove the finite facts: the shift-and-subtract equation forces $x = \tfrac{D}{10^k - 1}$ , the number with $n$ nines falls short of $1$ by exactly $\tfrac{1}{10^n}$ , and that gap can be made smaller than any positive rational.

repeating_to_fractionLean 4Proved here from basic factsFormally verified

/-- If shifting the decimal point `k ≥ 1` places gives the repeating block `D` plus the
number itself, `10^k · x = D + x`, then `x = D / (10^k - 1)`. For `x = 0.272727…`,
`100x = 27 + x`, so `x = 27/99`. -/
theorem repeating_to_fraction (x D : Rat) (k : Nat) (hk : 1 ≤ k) (h : 10 ^ k * x = D + x) :
    x = D / (10 ^ k - 1) := by
  have hpow : (10 : Rat) ≤ 10 ^ k := by
    have h10 : (10 : Nat) ≤ 10 ^ k := by
      calc 10 = 10 ^ 1 := rfl
        _ ≤ 10 ^ k := Nat.pow_le_pow_right (by decide) hk
    have := Rat.natCast_le_natCast.mpr h10
    simpa using this
  have hne : (10 : Rat) ^ k - 1 ≠ 0 := by
    intro h0
    have : (10 : Rat) ^ k = 1 := by grind
    rw [this] at hpow
    exact absurd hpow (by decide)
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

nines_gapLean 4Proved here from basic factsFormally verified

/-- The number `0.99…9` with `n` nines is `1 - 1/10^n`: its gap below `1` is exactly
`1/10^n`. As `n` grows, this gap becomes smaller than any positive number. -/
theorem nines_gap (n : Nat) : 1 - ((10 : Rat) ^ n - 1) / 10 ^ n = 1 / 10 ^ n := by
  have hpos : (0 : Rat) < 10 ^ n := Rat.pow_pos (by decide)
  have hne : (10 : Rat) ^ n ≠ 0 := Rat.ne_of_gt hpos
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

gap_lt_every_positiveLean 4Proved here from basic factsFormally verified

/-- For every positive rational `ε` there is an `n` with `1/10^n < ε`. Together with `nines_gap`
this is why `0.999… = 1`: the distance from `0.999…` up to `1` is below every positive
number, so it is `0`. Proof: take `n = ⌈1/ε⌉`; then `1/ε ≤ n < 10^n`. -/
theorem gap_lt_every_positive (ε : Rat) (hε : 0 < ε) : ∃ n : Nat, 1 / (10 : Rat) ^ n < ε := by
  refine ⟨(1 / ε).ceil.toNat, ?_⟩
  have hinvpos : 0 < 1 / ε := by
    rw [Rat.lt_div_iff hε]
    simpa using (show (0 : Rat) < 1 by decide)
  have hceil : 1 / ε ≤ ((1 / ε).ceil : Rat) := Rat.le_ceil
  have hceil_nonneg : 0 ≤ (1 / ε).ceil := by
    have : (0 : Rat) ≤ ((1 / ε).ceil : Rat) := Rat.le_trans (Rat.le_of_lt hinvpos) hceil
    exact Rat.intCast_nonneg.mp this
  have hcast : (((1 / ε).ceil.toNat : Nat) : Rat) = ((1 / ε).ceil : Rat) := by
    rw [← Rat.intCast_natCast, Int.toNat_of_nonneg hceil_nonneg]
  have hpow : ((1 / ε).ceil.toNat : Rat) < (10 : Rat) ^ (1 / ε).ceil.toNat := by
    have := Rat.natCast_lt_natCast.mpr
      (Nat.lt_pow_self (n := (1 / ε).ceil.toNat) (a := 10) (by decide))
    simpa using this
  have hlt : 1 / ε < (10 : Rat) ^ (1 / ε).ceil.toNat := by
    rw [hcast] at hpow
    grind
  have h10pos : (0 : Rat) < 10 ^ (1 / ε).ceil.toNat := Rat.pow_pos (by decide)
  rw [Rat.div_lt_iff h10pos]
  rw [Rat.div_lt_iff hε] at hlt
  grind

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

No rational square root of $2$ (Theorem 8). Lean's proof avoids “simplest form” and uses Fermat's infinite descent instead: a solution of $a^2 = 2b^2$ with $b > 0$ would give a smaller one, $b^2 = 2c^2$ , and whole numbers cannot get smaller for ever. It is the same idea — dividing out a $2$ again and again — organised differently.

even_of_sq_evenLean 4Proved here from basic factsFormally verified

/-- If `a · a` is even then `a` is even: an odd number times an odd number is odd. -/
theorem even_of_sq_even (a : Nat) (h : a * a % 2 = 0) : a % 2 = 0 := by
  rcases Nat.mod_two_eq_zero_or_one a with h0 | h1
  · exact h0
  · rw [Nat.mul_mod, h1] at h
    exact absurd h (by decide)

Axioms used: propextformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

sq_two_descentLean 4Proved here from basic factsFormally verified

/-- **No whole-number solution to `a² = 2b²` except `b = 0`** (Fermat's infinite descent).
If `a² = 2b²` with `b > 0`, then `a` is even, `a = 2c`, so `b² = 2c²`: a smaller solution
`(b, c)`, since `b < a`. Smaller and smaller solutions cannot go on for ever. -/
theorem sq_two_descent : ∀ a b : Nat, a * a = 2 * (b * b) → b = 0 := by
  intro a
  induction a using Nat.strongRecOn with
  | _ a ih =>
    intro b hab
    -- `a` is even.
    have heven : a % 2 = 0 := by
      apply even_of_sq_even
      rw [hab, Nat.mul_mod_right]
    obtain ⟨c, rfl⟩ : ∃ c, a = 2 * c := ⟨a / 2, by omega⟩
    -- Cancel a factor 2: `b * b = 2 * (c * c)`.
    have hbc : b * b = 2 * (c * c) := by
      have h4 : 2 * (2 * (c * c)) = 2 * (b * b) := by
        rw [← hab]; grind
      omega
    by_cases hb : b = 0
    · exact hb
    · -- `b < 2c`, because `b ≥ 2c` would give `b² ≥ 4c² > 2c²`.
      have hlt : b < 2 * c := by
        apply Nat.lt_of_not_le
        intro hle
        have hsq : (2 * c) * (2 * c) ≤ b * b := Nat.mul_le_mul hle hle
        have hbpos : 0 < b * b := Nat.mul_pos (by omega) (by omega)
        omega
      have hc : c = 0 := ih b hlt c hbc
      subst hc
      simp at hbc
      exact (Nat.mul_eq_zero.mp hbc).elim id id

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

no_rat_sq_twoLean 4Proved here from basic factsFormally verified

/-- **There is no rational number whose square is 2.** Writing `q = num/den`, `q² = 2` gives
`num² = 2 · den²`; taking absolute values gives whole numbers `a, b` with `a² = 2b²` and
`b = den ≠ 0`, which `sq_two_descent` rules out. So the rational number line has a gap
where `√2` should be. -/
theorem no_rat_sq_two : ¬ ∃ q : Rat, q * q = 2 := by
  intro ⟨q, hq⟩
  have hsq : q ^ 2 = 2 := by rw [← hq]; grind
  -- Compare numerators and denominators: `num(q²) · den(2) = num(2) · den(q²)`.
  have hcross := Rat.eq_iff_mul_eq_mul.mp hsq
  rw [Rat.num_pow, Rat.den_pow] at hcross
  have hint : q.num * q.num = 2 * ((q.den : Int) * (q.den : Int)) := by
    have h2n : (2 : Rat).num = 2 := rfl
    have h2d : (2 : Rat).den = 1 := rfl
    rw [h2n, h2d] at hcross
    simp only [Int.pow_succ, Int.pow_zero, Int.one_mul, Int.natCast_pow] at hcross
    grind
  have hnat : q.num.natAbs * q.num.natAbs = 2 * (q.den * q.den) := by
    have := congrArg Int.natAbs hint
    rw [Int.natAbs_mul, Int.natAbs_mul, Int.natAbs_mul] at this
    simpa using this
  exact q.den_nz (sq_two_descent _ _ hnat)

Axioms used: propext, Classical.choice, Quot.soundformal/Lumenary/RationalNumbers.leanTry it in the Lean web editor

Not formalised here: Theorem 5 (the $2$ -and- $5$ rule), and the meaning of infinite decimals as limits.

ComputationC

Long division by machine

Long division: why the decimals of a fraction repeatPythonExact computationExhaustive finite checkComputationally tested

"""Long division by hand, done by machine: why decimals of fractions repeat.

Dividing a by b, each step leaves a remainder 0, 1, ..., b - 1. As soon as a
remainder comes back, the digits after it repeat for ever. This experiment
runs long division with exact integers, records the remainders, and reports
where the repeating block starts and how long it is. It then checks, for
every fraction a/b with 0 <= a < b <= 200, two facts proved in the lesson:
the period is at most b - 1, and the expansion terminates exactly when b (in
lowest terms) has no prime factors other than 2 and 5. Finally it turns every
expansion back into a fraction. All arithmetic is exact (no floating point).
"""

from fractions import Fraction
from math import gcd

def long_division(a, b):
    """Digits of a/b after the point, for 0 <= a and b > 0.

    Returns (whole, digits, start, period): a/b = whole + 0.d1 d2 d3 ...,
    the digits from index ``start`` on repeat with length ``period``.
    A terminating decimal has repeating block "0" (period 1, digit 0).
    """
    if b <= 0 or a < 0:
        raise ValueError("need a >= 0 and b > 0")
    whole, r = divmod(a, b)
    seen = {}
    digits = []
    while r not in seen:
        seen[r] = len(digits)
        digit, r = divmod(10 * r, b)
        digits.append(digit)
    start = seen[r]
    return whole, digits, start, len(digits) - start

def decimal_string(a, b):
    """The expansion of a/b with the repeating block in brackets: 0.1(6)."""
    whole, digits, start, period = long_division(a, b)
    pre, block = digits[:start], digits[start:]
    if block == [0]:
        text = "".join(map(str, pre))
        return f"{whole}.{text}" if text else f"{whole}"
    pre_text = "".join(map(str, pre))
    return f"{whole}.{pre_text}({''.join(map(str, block))})"

def only_twos_and_fives(n):
    """True if n > 0 has no prime factor other than 2 and 5."""
    for p in (2, 5):
        while n % p == 0:
            n //= p
    return n == 1

def to_fraction(whole, pre, block):
    """Exact value of whole.pre(block) where pre, block are digit strings.

    x = whole + 0.pre(block); shifting by the block length k and
    subtracting removes the infinite tail: (10**k - 1) * 10**m * x is an
    integer, where m = len(pre).
    """
    m, k = len(pre), len(block)
    head = int(pre) if pre else 0
    if k == 0:
        return whole + Fraction(head, 10 ** m)
    tail = Fraction(int(block), 10 ** k - 1)
    return whole + (head + tail) / 10 ** m

def check_all(max_b):
    """Check the period bound, the 2-and-5 rule and round trips."""
    cases = bad_period = bad_rule = bad_trip = 0
    for b in range(1, max_b + 1):
        for a in range(b):
            whole, digits, start, period = long_division(a, b)
            cases += 1
            terminates = digits[start:] == [0]
            if not terminates and period > b - 1:
                bad_period += 1
            if terminates != only_twos_and_fives(b // gcd(a, b)):
                bad_rule += 1
            pre = "".join(map(str, digits[:start]))
            block = "".join(map(str, digits[start:]))
            if to_fraction(whole, pre, block) != Fraction(a, b):
                bad_trip += 1
    return cases, bad_period, bad_rule, bad_trip

def main():
    print("1/b by long division (repeating block in brackets)")
    print(" b   decimal                 period  only 2s and 5s?")
    for b in range(2, 18):
        _, digits, start, period = long_division(1, b)
        terminates = digits[start:] == [0]
        per = "-" if terminates else str(period)
        rule = "yes" if only_twos_and_fives(b) else "no"
        print(f"{b:2d}   {decimal_string(1, b):<22}  {per:>6}  {rule}")
    print()
    cases, bad_period, bad_rule, bad_trip = check_all(200)
    print(f"All a/b with 0 <= a < b <= 200: {cases} fractions checked.")
    print(f"  period longer than b - 1:                 {bad_period} cases")
    print(f"  2-and-5 rule wrong (either direction):     {bad_rule} cases")
    print(f"  expansion does not convert back exactly:  {bad_trip} cases")
    print(f"0.(27) = {to_fraction(0, '', '27')}   0.1(6) = "
          f"{to_fraction(0, '1', '6')}   0.(9) = {to_fraction(0, '', '9')}")
    print()
    print("Epistemic status: exact integer arithmetic, exhaustive for the")
    print("20,100 fractions listed. It shows remainders repeating; it does not")
    print("prove that every fraction behaves this way. The lesson's proof does:")
    print("only b remainders exist, so one must repeat (pigeonhole).")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The table shows that $\tfrac17$ , $\tfrac1{17}$ (block of $16$ digits) and others use the maximum period $b - 1$ , while $\tfrac13$ and $\tfrac16$ repeat after one digit. The exhaustive check is finite evidence: impressive, but it covers only denominators up to $200$ . The pigeonhole proof covers every fraction.

Rationals squeeze the square root of 2 but never hit itPythonExact computationExhaustive finite checkComputationally tested

"""Rationals crowd around the square root of 2, but none of them lands on it.

Three exact computations with fractions:

1. A search of every fraction p/q with 1 <= q <= 2000 for p*p == 2*q*q.
   (It finds none; for each q only p near q * 1.414 needs checking.)
2. Squeezing: halve an interval [lo, hi] with lo*lo < 2 < hi*hi again and
   again. The rational endpoints get as close as we like to each other, yet
   neither square is ever exactly 2.
3. The fractions 1/1, 3/2, 7/5, 17/12, 41/29, ... (each p/q followed by
   (p + 2q)/(p + q)) satisfy p*p - 2*q*q = +1 or -1, so their squares miss 2
   by exactly 1/q**2: astonishingly close, never equal.
"""

from fractions import Fraction
from math import isqrt

def square_root_two_search(max_q):
    """All (p, q) with 1 <= q <= max_q and p*p == 2*q*q (expected: none).

    For each q, the only candidate is p = isqrt(2*q*q), the largest whole
    number whose square is at most 2*q*q.
    """
    hits = []
    for q in range(1, max_q + 1):
        p = isqrt(2 * q * q)
        if p * p == 2 * q * q:
            hits.append((p, q))
    return hits

def squeeze(steps):
    """Halve [1, 2] ``steps`` times, keeping lo*lo < 2 < hi*hi."""
    lo, hi = Fraction(1), Fraction(2)
    history = [(lo, hi)]
    for _ in range(steps):
        mid = (lo + hi) / 2
        if mid * mid == 2:
            raise AssertionError("found a rational square root of 2")
        if mid * mid < 2:
            lo = mid
        else:
            hi = mid
        history.append((lo, hi))
    return history

def pell_fractions(count):
    """The fractions p/q = 1/1, 3/2, 7/5, ... with p*p - 2*q*q = +-1."""
    p, q = 1, 1
    out = []
    for _ in range(count):
        out.append((p, q))
        p, q = p + 2 * q, p + q
    return out

def main():
    hits = square_root_two_search(2000)
    print("1. Fractions p/q with q <= 2000 and (p/q)^2 = 2:", len(hits))
    print()
    print("2. Squeezing between rationals (lo^2 < 2 < hi^2):")
    for k, (lo, hi) in enumerate(squeeze(10)):
        if k % 2 == 0:
            print(f"   step {k:2d}: {str(lo):>9} < sqrt 2 < {str(hi):<9}"
                  f" width {hi - lo}")
    print()
    print("3. p/q with p^2 - 2q^2 = +-1: the square misses 2 by 1/q^2")
    print("      p/q        p^2 - 2q^2   (p/q)^2 - 2")
    for p, q in pell_fractions(8):
        miss = Fraction(p * p, q * q) - 2
        print(f"   {p:>5}/{q:<6}  {p * p - 2 * q * q:>8}      {miss}")
    print()
    print("Epistemic status: exact, exhaustive for denominators up to 2000;")
    print("the squeeze and the list show rationals getting ever closer to")
    print("sqrt 2. No computation can show that no fraction ever works: that")
    print("needs the proof by contradiction in the lesson.")

if __name__ == "__main__":
    main()

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

The fractions get as close to $\sqrt2$ as we like: $\tfrac{577}{408}$ squared misses $2$ by only $\tfrac{1}{166464}$ . But a search, however long, can never show that no fraction works. Only Theorem 8 can.

Explore

Explore: decimals creeping up on a fraction

Fractions on a number line

0.3, 0.33, 0.333 creep up on 1/3 but never reach it. Which points coincide?

Cut each whole into equal parts:3

1/3
0.3
0.33
0.333
1/2
3/4
0.75

From smallest to largest

0.3 < 0.33 < 0.333 < 1/3 < 1/2 < 3/4 = 0.75

With 3 equal parts in each whole, which points land exactly on a tick mark?

0.3 = 3/10 · 0.33 = 33/100 · 0.333 = 333/1000 · 1/3 · 1/2 = 0.5 · 3/4 = 0.75

Notice that $0.75$ and $\tfrac34$ share one point: they are two names for one number. The truncations $0.3, 0.33, 0.333$ get ever closer to $\tfrac13$ without reaching it — only the infinite decimal $0.\overline{3}$ equals $\tfrac13$ . Try typing other decimals, such as $0.125$ or $0.6$ , and find the fractions they equal.

Exercises

1. Rational numbers

Warm-upHuman

Compute $-\tfrac34 + \tfrac56$ .

Choose one

\tfrac1{12}

\tfrac{2}{10}

-\tfrac1{12}

-\tfrac{19}{12}

2. Rational numbers

Warm-upHuman

A water seller in Kano has $7$ litres of water and fills bottles that hold $\tfrac12$ litre each. How many bottles can she fill? (Compute $7 \div \tfrac12$ .)

3. Rational numbers

CoreHuman

Compute $\left(-\tfrac56\right) \div \left(-\tfrac{10}{9}\right)$ .

Choose one

\tfrac34

-\tfrac34

\tfrac{25}{27}

\tfrac43

4. Rational numbers

CoreHuman

Which of these numbers have a reciprocal in $\Q$ ? (Choose all that apply.)

Choose all that apply

-\tfrac25

0

7

0.25

5. Rational numbers

CoreHuman

Which of these fractions have terminating decimal expansions? (Choose all that apply.)

Choose all that apply

6. Rational numbers

CoreHuman

Which fraction equals $0.\overline{36} = 0.363636\ldots$ ?

Choose one

\tfrac4{11}

\tfrac{9}{25}

\tfrac25

\tfrac13

7. Rational numbers

Warm-upHuman

How many rational numbers lie strictly between $\tfrac13$ and $\tfrac12$ ?

Choose one

None — they are next to each otherExactly oneFinitely many, but a lotInfinitely many

8. Rational numbers

StretchHuman

In the proof that $\sqrt2$ is irrational we have $a^2 = 2b^2$ and conclude that $a$ is even. Which reason is correct?

Choose one

a^2

is even, and the square of an odd number is odd, so

a

cannot be oddBecause

2

is evenBecause

b

is evenBecause

\tfrac ab

is in simplest form

9. Rational numbers

CoreFormal

Which Lean statement says correctly that between any two different rational numbers there is another?

Choose one

∀ a b : Rat, a < b → ∃ c, a < c ∧ c < b∃ c : Rat, ∀ a b : Rat, a < c ∧ c < b∀ a b : Rat, ∃ c, a < c ∧ c < b∀ a b : Rat, a < b → a < a + b ∧ a + b < b

10. Rational numbers

StretchComputational

Write period_length(a, b) for whole numbers $a \ge 0$ and $b > 0$ . Do long division: start with the remainder a % b, and at each step replace the remainder r by (10 * r) % b. Remember the step at which each remainder first appears. Return the length of the repeating block of $\tfrac ab$ , or 0 if the decimal terminates (that is, if the remainder 0 appears).

Runs entirely in your browser, in an isolated worker. Nothing is sent to a server.

Common misconceptionsH

Common misconceptions

Misconception

“Dividing always makes a number smaller.” Dividing by a number between $0$ and $1$ makes a positive number bigger: $3 \div \tfrac12 = 6$ . And dividing a negative number by $2$ makes it bigger too: $-6 \div 2 = -3$ , which is greater than $-6$ .

Misconception

“ $0.999\ldots$ is just less than $1$ .” The gap would have to be smaller than $\tfrac1{10^n}$ for every $n$ , and the only such number that is not negative is $0$ . So $0.999\ldots = 1$ (Theorem 7) — two names for one number.

Misconception

“Once every fraction is marked, the number line is full.” The fractions are dense, but $\sqrt2$ (Theorem 8), $\sqrt3$ , $\pi$ and infinitely many other numbers are missing.

Misconception

“To add fractions, add the tops and add the bottoms.” $\tfrac12 + \tfrac13 = \tfrac56$ , not $\tfrac25$ . (Curiously, $\tfrac25$ lies between $\tfrac13$ and $\tfrac12$ — it is their mediant — but it is not their sum.)

Misconception

“A fraction with a big denominator has a long decimal.” $\tfrac{1}{1024} = 0.0009765625$ terminates because $1024 = 2^{10}$ , while $\tfrac13$ repeats for ever. What matters is the prime factors of the denominator (Theorem 5), not its size.

ViewpointsH

Other ways of seeing

Geometry— Rational numbers are slopes through grid points

Draw the square grid of points with integer coordinates. The line from $(0, 0)$ through the grid point $(b, a)$ , with $b \neq 0$ , has slope $\tfrac ab$ — a rational number. Conversely, a line through the origin with rational slope $\tfrac ab$ hits the grid point $(b, a)$ . So the rational numbers are exactly the slopes of lines through the origin that meet another grid point. The line $y = \sqrt2\, x$ passes through no grid point except $(0, 0)$ , however far you follow it: that is Theorem 8 in a picture. See the coordinate plane.

Analysis— Crowded but not complete

The truncations $1,\ 1.4,\ 1.41,\ 1.414,\ \ldots$ of $\sqrt2$ are all rational, and they get closer and closer to one another — yet no rational number is the point they approach. An analyst says $\Q$ is dense but not complete. Building a number line with no gaps, the real numbers, is the starting point of calculus; see real numbers and irrationality and sequences and series. Another surprise: although the rationals are dense, they can be listed one after another — $\Q$ is countable.

Wonder Trails

Reciprocals finish the story of “undoing” multiplication; families of equal fractions are an example of sorting things into classes; and the rationals are a surprising kind of infinity. All of these are optional.

Wonder Trail · Optional · never gradedInverses and structureEvery integer can be added to another integer to get

0

. So why can almost no integer be multiplied by another integer to get

1

?Follow the trail Wonder Trail · Optional · never gradedRemainder familiesSort every integer — positive, negative and zero — into families by its remainder after dividing by 3. If you add a member of one family to a member of another, does the family of the answer depend on which members you chose?Follow the trail Wonder Trail · Optional · never gradedHow many infinities?There are infinitely many counting numbers and infinitely many infinite 0–1 sequences. Are these two infinities the same size?Follow the trail

Set-theoretic connectionH

Set-theoretic connection

The number systems sit inside one another: $\N \subseteq \Z \subseteq \Q$ . At university you may build $\Q$ from $\Z$ : a rational number is a family of pairs of integers $(a, b)$ with $b \neq 0$ , where $(a, b)$ and $(c, d)$ belong to the same family exactly when $ad = bc$ . The family of $(1, 2)$ contains $(2, 4)$ , $(-3, -6)$ , $(50, 100)$ , …

For this to work, “same family” must be an equivalence relation, and the fraction rules must give answers in the same family whichever members we pick: replacing $\tfrac12$ by $\tfrac24$ in a sum must not change the result. Both can be proved; see constructing ℤ, ℚ and ℝ.

Category-theoretic connectionH

A glimpse of structure

$\Q$ is a field: addition and multiplication are commutative and associative, have identities $0$ and $1$ , are linked by the distributive law, every number has an opposite, and every non-zero number has a reciprocal. It is also the smallest field that contains the integers: any field containing $\Z$ (with the same addition and multiplication) contains every $a \cdot b^{-1}$ , and so contains a copy of $\Q$ . Describing an object as “the smallest one with a property” is an example of a universal property, a central idea of algebraic structures and of category theory.

History & global context

History and global context

Egypt. The Rhind Mathematical Papyrus (about 1550 BCE, copied by the scribe Ahmes from an older text) writes fractions as sums of different unit fractions, for example $\tfrac25 = \tfrac13 + \tfrac1{15}$ .
Mesopotamia. Babylonian scribes used base- $60$ fractions. The clay tablet YBC 7289 (about 1800–1600 BCE) gives $\sqrt2 \approx 1;24,51,10 = 1 + \tfrac{24}{60} + \tfrac{51}{60^2} + \tfrac{10}{60^3} \approx 1.4142130$ , within about $6 \times 10^{-7}$ of the true value.
China. The Nine Chapters on the Mathematical Art (compiled by about the 1st century CE) gives rules for adding, subtracting, multiplying and dividing fractions, and reduces them to lowest terms by repeated subtraction — the method we now call Euclid's algorithm.
Greece. Greek mathematicians of the 5th century BCE discovered that the side and the diagonal of a square have no common measure — in modern terms, that $\sqrt2$ is irrational. Aristotle refers to a proof by odd and even numbers. Later stories attribute the discovery to the Pythagoreans; the details are uncertain.
India and the Islamic world. Indian mathematicians wrote a fraction as one number above another; mathematicians writing in Arabic, such as al-Ḥaṣṣār in 12th-century Morocco, are usually credited with adding the horizontal bar. The earliest known decimal fractions appear in the arithmetic book of al-Uqlīdisī (Damascus, 952–953). Jamshīd al-Kāshī used them systematically in The Key to Arithmetic (Samarkand, 1427), and Simon Stevin's booklet De Thiende (1585) spread them in Europe.
Repeating decimals. Carl Friedrich Gauss studied the lengths of the repeating blocks of $\tfrac1p$ in his Disquisitiones Arithmeticae (1801). Whether infinitely many primes $p$ give $\tfrac1p$ a block of the full length $p - 1$ (as $7$ and $17$ do) is still unproved: it is a case of Artin's conjecture on primitive roots.

When the integers run out

Fractions on both sides of zero

Definitions

Worked examples

The main results, with proofs

A gap in the rational line

Rational numbers in Lean

Long division by machine

Explore: decimals creeping up on a fraction

Exercises

Common misconceptions

Other ways of seeing

Wonder Trails

Set-theoretic connection

A glimpse of structure

History and global context

Further reading