Cubes on the mod-nine clock

Every cube lands on 0, 1 or 8 of the nine-residue clock: the first case of the case-of-three story.

Start with a concrete example

2³=8 leaves 8 after division by 9; 4³=64 leaves 1. Working with these small remainders can rule out an equation even when its full numbers are huge.

A small check: try the idea

Think with the concrete example above. You can try again.

What remainder does 4³=64 leave after division by 9?

Read the answer and reasoning

1. 9×7=63, leaving 1. We take the remainder after cubing, not before ignoring the power.

Build the idea in three steps

On a clock with nine positions, every integer has a remainder, and multiplication respects remainders.
Whatever integer n is, its cube reduces on this clock to one of just three values: 0, 1 or 8. A number not divisible by three always avoids the 0 slot and lands on 1 or 8.
The theorem collects the payoff: if 3 divides none of a, b and c, then a ^ 3 + b ^ 3 ≠ c ^ 3 — two residues from {1, 8} cannot sum to another.

A small example

The clock keeps cubes honest: 4³ = 64 leaves remainder 1, and 2³ leaves 8. Summing any two of {1, 8} gives 2, 0 or 7 — never 1 or 8, so no cube of a nonmultiple of three can stand at the far end of an equality.

Lean definition · original excerpt

Mathlib · db584cd · Three.lean

58lemma cube_of_castHom_ne_zero {n : ZMod 9} :59    castHom (show 3 ∣ 9 by simp) (ZMod 3) n ≠ 0 → n ^ 3 = 1 ∨ n ^ 3 = 8 := by60  revert n; decide61 62lemma cube_of_not_dvd {n : ℤ} (h : ¬ 3 ∣ n) :63    (n : ZMod 9) ^ 3 = 1 ∨ (n : ZMod 9) ^ 3 = 8 := by64  apply cube_of_castHom_ne_zero65  rwa [map_intCast, Ne, ZMod.intCast_zmod_eq_zero_iff_dvd]66 67/-- If `a b c : ℤ` are such that `¬ 3 ∣ a * b * c`, then `a ^ 3 + b ^ 3 ≠ c ^ 3`. -/68theorem fermatLastTheoremThree_case_1 {a b c : ℤ} (hdvd : ¬ 3 ∣ a * b * c) :69    a ^ 3 + b ^ 3 ≠ c ^ 3 := by

How to read this Lean

The first lemma is the whole engine: on ZMod 9, a residue whose image in ZMod 3 does not vanish has its cube equal to 1 or to 8 — decide simply checks the nine cases, keeping the source short. The second lemma carries the pattern to integers n with 3 ∤ n. The displayed theorem then continues below the excerpt: 3 dividing the product a * b * c is split into the three individual conditions.

Original source ↗ · L58–69 Open the complete saved source

Where this idea is used

2. The case of three 7. The veterans’ cabinet

Cubes on the mod-nine clock

Start with a concrete example

A small check: try the idea

Build the idea in three steps

A small example

Lean definition · original excerpt

How to read this Lean

Where this idea is used

Mika’s help desk

One thing at a time

In simpler words

A small clue