>>320
よろしければ 補題2の略証のmod 4の数学的な意味を教えてくれませんか。
補題3の証明もそうですが少し頭がよすぎる方法だとおもいます。
(補題3は√2がF_p(~=Z/pZ)に入っている可能性があるので、
√2+1≠0は明らかであるとは言い難いきがします。
といっても、√2 = -1 ⇒ 2 = 1 となるので すぐ確認できますが)
たしかに素早く処理できいて素晴らしいとおもいますが、
私を含む多くの人達は次のような解答をとったとおもいます。

[略解] (若干飛躍気味なので各自脳内補完お願いします)
x^2-2y^2=1 ・・・Л を満たす正整数x,y(x＞17,y＞12)が存在したとする。
このとき、yの素因数の個数が2以下であると仮定する。
すると y=2^m*p^n を満たす奇素数p,正整数m,非負整数nが取れる。
これとЛから (x+1)(x-1)=2^(2m+1)*p^(2n)
(gcd(x+1,x-1)=2 に注意して)これから次の2パターンが考えれる。
x+1 = 2^(2m) かつ x-1 = 2p^(2n) ・・・①
x+1 = 2p^(2n) かつ x-1 = 2^(2m) ・・・②
①の場合 1=2^(2m-1)-p^(2n) となり、mod 4でみることで m=1がわかり、
m=1のとき x=3であり、これは矛盾である。
②の場合 2^(2m-1)=(p^n+1)(p^n-1) となるが、
gcd(p^n+1,p^n-1)=2 であり (p^n+1)/2＞(p^n-1)/2＞1 なので、
(∵ x＞17より、n≠0 と「p=3かつn=1」でないことが確認できるから)
この場合も矛盾であるといえる。したがって題意は示せた。