偶数・奇数と場合分け

数を偶数と奇数に分けるのは、この証明そのものが使う最初の場合分けです。

まず、身近な例で

あめ7個を2個ずつ組にすると1個余ります。8個なら余りません。この二つの違いが、奇数と偶数です。

上の具体例を見ながら考えよう。何度やり直しても大丈夫。

あめ7個を2個ずつ組にすると、何個余る？

答えと考え方を読む

1個。 3組で6個使い、1個残ります。この余りが、7が奇数であることを表します。

どの整数も偶数か奇数のどちらか一方です。2で割って余り0なら偶数、そうでなければ奇数。両方にあてはまる整数はありません。
問題を偶数と奇数の場合に分けるのは、数の問題の基本的な一手です。FLT自身がそう始めます。指数p = 2の場合は、それ以外のすべての場合と扱いが違います。
2以外の素数は必ず奇数です。小包の欄ppはpが素数であることを、hp5はp ≥ 5であることを記録します。補題hp_oddはこの二つを組み合わせて、pが奇数だと示します。

2・3・4・5のうち、偶数は2と4です。この中で素数でもある偶数は2だけ。素数の指数2が偶数の例外で、小包のhp5はこの議論を5以上の素数に制限します。

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)

証明はodd_of_ne_twoを引用します。素数pは、pが2でないときちょうど奇数です。残る小さな条件p ≠ 2は、hp5が5 ≤ pを供給してから、短い算術のタクティックが閉じます。