Even, odd, and case splits

Splitting numbers into even and odd is the proof’s own first case distinction.

Start with a concrete example

Put 7 sweets into pairs: one is left. With 8 sweets none is left. Odd and even distinguish these two possibilities.

A small check: try the idea

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

After pairing 7 sweets, how many are left?

Read the answer and reasoning

1. Three pairs use 6 sweets; one remains. This is why 7 is odd.

Build the idea in three steps

Every integer is even or odd: even when division by two leaves remainder 0, odd otherwise. No integer satisfies both at once.
Sorting a question into even and odd cases is one of the standard moves of number problems. FLT itself starts this way: the exponent case p = 2 behaves differently from all the rest.
A prime different from two is always odd. The package field pp records that p is prime, hp5 records that p ≥ 5, and the lemma hp_odd combines them: p is odd.

A small example

Among 2, 3, 4 and 5, the even numbers are 2 and 4; only 2 is both prime and even. The prime exponent 2 is the even prime exception. The package’s hp5 condition restricts this part of the proof to primes at least 5.

Use in Lean · original excerpt

FLT · aa2d8b3 · Def_FLTPrelim_FreyPackage.lean

46lemma hp_odd (P : FreyPackage) : Odd P.p :=47  P.pp.odd_of_ne_two (by have := P.hp5; omega)

How to read this Lean

The proof cites odd_of_ne_two: a prime p is odd exactly when p is not two. The remaining small condition, p ≠ 2, is closed by a short arithmetic tactic after hp5 supplies 5 ≤ p.

Original source ↗ · L46–47 Open the complete saved source

Where this idea is used

1. The impossible order 7. The veterans’ cabinet

Even, odd, and case splits

Start with a concrete example

A small check: try the idea

Build the idea in three steps

A small example

Use in Lean · 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