\(x^4 + y^4 = z^2\) には正の整数解がない。無限降下：解があれば \(z\) のより小さい解がある。

1 準備

共通の素因数があれば、素数 \(p\) で割った解（\(p^2 \mid z\)）がある。
Lred … \(p \in \mathbb{P} , x , y , z \in \mathbb{M} , p \mid x , p \mid y , ( x \cdot x ) \cdot ( x \cdot x ) + ( y \cdot y ) \cdot ( y \cdot y ) = z \cdot z \Longrightarrow \exists a \in \mathbb{M} . \exists b \in \mathbb{M} . \exists c \in \mathbb{M} . x = p \cdot a , y = p \cdot b , z = ( p \cdot p ) \cdot c , ( a \cdot a ) \cdot ( a \cdot a ) + ( b \cdot b ) \cdot ( b \cdot b ) = c \cdot c\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，Euclid ，∣k⋅
\(x, y\) に共通の素因数がなければ、\(x^2, y^2\) の公約数は 1 だけ（素因数は \(x\) も割る）。
Lc1 … \(x , y \in \mathbb{M} , x \neq 0 , \neg \exists q \in \mathbb{P} . q \mid x , q \mid y \Longrightarrow \forall d \in \mathbb{M} . ( d \mid x \cdot x , d \mid y \cdot y \Longrightarrow d = 1 )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，Euclid ，∣k⋅ ，Lpf
共通の素因数がなければ公約数は 1 だけ（Lc1 の平方でない版）。\(x \le x^2\)（\(x \neq 0\)）。奇数の平方どうしの和は平方数でない。
Lc0 … \(a , b \in \mathbb{M} , a \neq 0 , \neg \exists q \in \mathbb{P} . q \mid a , q \mid b \Longrightarrow \forall d \in \mathbb{M} . ( d \mid a , d \mid b \Longrightarrow d = 1 )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，Euclid ，∣k⋅ ，Lpf
Lsqle … \(x \in \mathbb{M} , x \neq 0 \Longrightarrow x \le x \cdot x\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\)

2 偶奇

奇数の平方は \(4t + 1\)、平方数は \(4v\) か \(4v + 1\)。したがって \(x, y\) がともに奇数なら \(x^2 + y^2 = 4t + 2\) は平方数でない。
Lsq2 … \(x , y , z \in \mathbb{M} , x \cdot x + y \cdot y = z \cdot z , \neg 2 \mid x , \neg 2 \mid y \Longrightarrow {\perp}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\)
平方の和についての偶奇：奇数どうしの平方の和は平方数でない（Lsq2）。4乗の和には平方を当てはめる。
Lodd2 … \(x , y , z \in \mathbb{M} , ( x \cdot x ) \cdot ( x \cdot x ) + ( y \cdot y ) \cdot ( y \cdot y ) = z \cdot z , \neg 2 \mid x , \neg 2 \mid y \Longrightarrow {\perp}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，Euclid ，∣k⋅ ，Lsq2

3 降下の1段

\(x^4 + y^4 = z^2\)（\(x, y\) は互いに素・\(y\) は偶数）に 23 のピタゴラス数の形を当てはめる：\(x^2 + n^2 = m^2\)・\(y^2 = 2mn\)・\(z = m^2 + n^2\)。
La … \(x , y , z \in \mathbb{M} , x \neq 0 , ( x \cdot x ) \cdot ( x \cdot x ) + ( y \cdot y ) \cdot ( y \cdot y ) = z \cdot z , \neg \exists q \in \mathbb{P} . q \mid x , q \mid y , 2 \mid y \Longrightarrow \exists m \in \mathbb{M} . \exists n \in \mathbb{M} . x \cdot x + n \cdot n = m \cdot m , y \cdot y = 2 \cdot ( m \cdot n ) , z = m \cdot m + n \cdot n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅ ，Lc1
\(y\) が偶数で \(x, y\) に共通の素因数がなければ \(x\) は奇数。\(x^2 + n^2 = m^2\)（\(x\) 奇数）で \(m, n\) に共通の素因数がなければ \(n\) は偶数。
Lb1 … \(x , y \in \mathbb{M} , \neg \exists q \in \mathbb{P} . q \mid x , q \mid y , 2 \mid y \Longrightarrow \neg 2 \mid x\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\)
Lb2 … \(x , n , m \in \mathbb{M} , x \cdot x + n \cdot n = m \cdot m , \neg 2 \mid x \Longrightarrow 2 \mid n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Lsq2
Lb3 … \(x , y , m , n \in \mathbb{M} , \neg \exists q \in \mathbb{P} . q \mid x , q \mid y , x \cdot x + n \cdot n = m \cdot m , y \cdot y = 2 \cdot ( m \cdot n ) \Longrightarrow \neg \exists q \in \mathbb{P} . q \mid m , q \mid n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅
Lb4 … \(x , n , m \in \mathbb{M} , \neg \exists q \in \mathbb{P} . q \mid m , q \mid n , x \cdot x + n \cdot n = m \cdot m \Longrightarrow \neg \exists q \in \mathbb{P} . q \mid x , q \mid n\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅
\(x^2 + n^2 = m^2\)（\(x\) と \(n\) は互いに素・\(n\) は偶数）にもう一度ピタゴラス数の形を当てる：\(x + s^2 = r^2\)・\(n = 2rs\)・\(m = r^2 + s^2\)。
Lc … \(x , n , m \in \mathbb{M} , x \neq 0 , \neg \exists q \in \mathbb{P} . q \mid x , q \mid n , x \cdot x + n \cdot n = m \cdot m , 2 \mid n \Longrightarrow \exists r \in \mathbb{M} . \exists s \in \mathbb{M} . x + s \cdot s = r \cdot r , n = 2 \cdot ( r \cdot s ) , m = r \cdot r + s \cdot s\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅ ，Lc0
\(y = 2w\) とおくと \(w^2 = m r s\)。\(r, s, m\) は互いに素なので、それぞれ平方数（Sq⋅）。
Lw … \(w , m , r , s \in \mathbb{M} , ( 2 \cdot w ) \cdot ( 2 \cdot w ) = 2 \cdot ( m \cdot ( 2 \cdot ( r \cdot s ) ) ) \Longrightarrow w \cdot w = m \cdot ( r \cdot s )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅
Lf … \(x , n , m , r , s \in \mathbb{M} , \neg \exists q \in \mathbb{P} . q \mid x , q \mid n , x + s \cdot s = r \cdot r , n = 2 \cdot ( r \cdot s ) , m = r \cdot r + s \cdot s \Longrightarrow \neg \exists q \in \mathbb{P} . q \mid r , q \mid s , \neg \exists q \in \mathbb{P} . q \mid m , q \mid r , \neg \exists q \in \mathbb{P} . q \mid m , q \mid s\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅
Lg … \(w , m , r , s \in \mathbb{M} , w \cdot w = m \cdot ( r \cdot s ) , \neg \exists q \in \mathbb{P} . q \mid r , q \mid s , \neg \exists q \in \mathbb{P} . q \mid m , q \mid r , \neg \exists q \in \mathbb{P} . q \mid m , q \mid s \Longrightarrow \exists a \in \mathbb{M} . \exists b \in \mathbb{M} . \exists c \in \mathbb{M} . r = a \cdot a , s = b \cdot b , m = c \cdot c\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅ ，Sq⋅
0 でない数の判定：\(y^2 = 2mn \neq 0\) なら \(m, n \neq 0\)。\(n = 2rs \neq 0\) なら \(r, s \neq 0\)。\(r = a^2 \neq 0\) なら \(a \neq 0\)。\(m = c^2\)・\(z = m^2 + n^2\) なら \(c < z\)。
Ln0 … \(y , m , n \in \mathbb{M} , y \neq 0 , y \cdot y = 2 \cdot ( m \cdot n ) \Longrightarrow m \neq 0 , n \neq 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅
Lnr … \(n , r , s \in \mathbb{M} , n \neq 0 , n = 2 \cdot ( r \cdot s ) \Longrightarrow r \neq 0 , s \neq 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅
Lna … \(a , r \in \mathbb{M} , r = a \cdot a , r \neq 0 \Longrightarrow a \neq 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅
Lcz … \(c , m , n , z \in \mathbb{M} , m = c \cdot c , m \neq 0 , n \neq 0 , z = m \cdot m + n \cdot n \Longrightarrow c < z\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅
降下の1段：互いに素な解 \(x^4 + y^4 = z^2\)（\(y\) は偶数）から、\(c < z\) の解 \(a^4 + b^4 = c^2\) が得られる。
Ldesc … \(x , y , z \in \mathbb{M} , x \neq 0 , y \neq 0 , ( x \cdot x ) \cdot ( x \cdot x ) + ( y \cdot y ) \cdot ( y \cdot y ) = z \cdot z , \neg \exists q \in \mathbb{P} . q \mid x , q \mid y , 2 \mid y \Longrightarrow \exists a \in \mathbb{M} . \exists b \in \mathbb{M} . \exists c \in \mathbb{M} . a \neq 0 , b \neq 0 , ( a \cdot a ) \cdot ( a \cdot a ) + ( b \cdot b ) \cdot ( b \cdot b ) = c \cdot c , c < z\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅ ，Lc0 ，Lc1 ，Lsq2 ，La ，Lb1 ，Lb2 ，Lb3 ，Lb4 ，Lc ，Lw ，Lf ，Lg ，Ln0 ，Lnr ，Lna ，Lcz

4 無限降下

\(z\) より小さい解がないとき、\(z\) の解もない。共通の素因数があれば Lred、なければ偶奇で場合分けして Ldesc。
Lz2 … \(c , z \in \mathbb{M} , p \in \mathbb{P} , z = ( p \cdot p ) \cdot c , z \neq 0 \Longrightarrow c < z\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅
Lzn … \(x , y , z \in \mathbb{M} , x \neq 0 , ( x \cdot x ) \cdot ( x \cdot x ) + ( y \cdot y ) \cdot ( y \cdot y ) = z \cdot z \Longrightarrow z \neq 0\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅
Lst1 … \(x , y , z \in \mathbb{M} , x \neq 0 , y \neq 0 , ( x \cdot x ) \cdot ( x \cdot x ) + ( y \cdot y ) \cdot ( y \cdot y ) = z \cdot z , \forall c \in \mathbb{M} . ( c < z \Longrightarrow \forall a \in \mathbb{M} . \forall b \in \mathbb{M} . ( a \neq 0 , b \neq 0 \Longrightarrow \neg ( ( a \cdot a ) \cdot ( a \cdot a ) + ( b \cdot b ) \cdot ( b \cdot b ) = c \cdot c ) ) ) , p \in \mathbb{P} , p \mid x , p \mid y \Longrightarrow {\perp}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅ ，Lred ，Lna ，Lz2 ，Lzn
Lev … \(x , y , z \in \mathbb{M} , x \neq 0 , y \neq 0 , ( x \cdot x ) \cdot ( x \cdot x ) + ( y \cdot y ) \cdot ( y \cdot y ) = z \cdot z , \forall c \in \mathbb{M} . ( c < z \Longrightarrow \forall a \in \mathbb{M} . \forall b \in \mathbb{M} . ( a \neq 0 , b \neq 0 \Longrightarrow \neg ( ( a \cdot a ) \cdot ( a \cdot a ) + ( b \cdot b ) \cdot ( b \cdot b ) = c \cdot c ) ) ) , \neg \exists q \in \mathbb{P} . q \mid x , q \mid y , 2 \mid y \Longrightarrow {\perp}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅ ，Lc0 ，Lc1 ，Lsq2 ，La ，Lb1 ，Lb2 ，Lb3 ，Lb4 ，Lc ，Lw ，Lf ，Lg ，Ln0 ，Lnr ，Lna ，Lcz ，Ldesc
Lst2 … \(x , y , z \in \mathbb{M} , x \neq 0 , y \neq 0 , ( x \cdot x ) \cdot ( x \cdot x ) + ( y \cdot y ) \cdot ( y \cdot y ) = z \cdot z , \forall c \in \mathbb{M} . ( c < z \Longrightarrow \forall a \in \mathbb{M} . \forall b \in \mathbb{M} . ( a \neq 0 , b \neq 0 \Longrightarrow \neg ( ( a \cdot a ) \cdot ( a \cdot a ) + ( b \cdot b ) \cdot ( b \cdot b ) = c \cdot c ) ) ) , \neg \exists q \in \mathbb{P} . q \mid x , q \mid y \Longrightarrow {\perp}\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅ ，Lc0 ，Lc1 ，Lodd2 ，Lsq2 ，La ，Lb1 ，Lb2 ，Lb3 ，Lb4 ，Lc ，Lw ，Lf ，Lg ，Ln0 ，Lnr ，Lna ，Lcz ，Ldesc ，Lev
\(z\) についての強い帰納法（SIND）：共通の素因数があれば Lst1、なければ Lst2。
Lmain … \(x , y , z \in \mathbb{M} , x \neq 0 , y \neq 0 \Longrightarrow \neg ( ( x \cdot x ) \cdot ( x \cdot x ) + ( y \cdot y ) \cdot ( y \cdot y ) = z \cdot z )\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅ ，Lc0 ，Lred ，Lc1 ，Lodd2 ，Lsq2 ，La ，Lb1 ，Lb2 ，Lb3 ，Lb4 ，Lc ，Lw ，Lf ，Lg ，Ln0 ，Lnr ，Lna ，Lcz ，Ldesc ，Lz2 ，Lzn ，Lst1 ，Lev ，Lst2

5 主定理

\(x^4 + y^4 = z^2\) を満たす正の整数の組はない。
\(x , y , z \in \mathbb{M} , x \neq 0 , y \neq 0 \Longrightarrow x ^ 4 + y ^ 4 \neq z ^ 2\) \(\blacktriangleleft\) \(\mathbb{W}.\) ，ℤ. ，-ℤ ，+ℤ ，Peano1 ，Peano2 ，ℕ. ，INDC ，+𝕄 ，⋅𝕄 ，↑𝕄 ，ℙ.' ，\(0 \in \mathbb{M}\) ，\(1 \in \mathbb{M}\) ，\(2 \in \mathbb{M}\) ，\(3 \in \mathbb{M}\) ，\(4 \in \mathbb{M}\) ，\(5 \in \mathbb{M}\) ，\(2 \in \mathbb{P}\) ，Euclid ，∣k⋅ ，Lpf ，Pyth⋅ ，Lc0 ，Lred ，Lc1 ，Lodd2 ，Lsq2 ，La ，Lb1 ，Lb2 ，Lb3 ，Lb4 ，Lc ，Lw ，Lf ，Lg ，Ln0 ，Lnr ，Lna ，Lcz ，Ldesc ，Lz2 ，Lzn ，Lst1 ，Lev ，Lst2 ，Lmain