\(\sqrt{2}\) が無理数であること。\(m^2 = 2n^2\)（\(n \neq 0\)）なら、最大公約数 \(g\) で割って互いに素な \(a, b\) にしても \(a^2 = 2b^2\) で、\(a, b\) がともに偶数になり矛盾する（1a と別の証明）。

1 準備

2 は素数で、\(2 \mid a^2\) なら \(2 \mid a\)（ユークリッドの補題）。
\(2 \mid a^2\) なら \(2 \mid a\)。\(a^2 = 2b^2\) なら \(a = 2c\) で \(b^2 = 2c^2\)。
E2 … \(a \in \mathbb{M} , 2 \mid a \cdot a \Longrightarrow 2 \mid a\) \(\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}\) ，Ldiv ，LG ，Euclid ，\(2 \in \mathbb{P}\) ，\(2 \in \mathbb{N}\)
Lev2 … \(a , b \in \mathbb{M} , a \cdot a = 2 \cdot ( b \cdot b ) \Longrightarrow \exists c \in \mathbb{M} . a = 2 \cdot c , b \cdot b = 2 \cdot ( 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}\) ，Ldiv ，LG ，Euclid ，\(2 \in \mathbb{P}\) ，\(2 \in \mathbb{N}\) ，E2
Lbd … \(b , c \in \mathbb{M} , b \cdot b = 2 \cdot ( c \cdot c ) \Longrightarrow \exists d \in \mathbb{M} . b = 2 \cdot d\) \(\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}\) ，Ldiv ，LG ，Euclid ，\(2 \in \mathbb{P}\) ，\(2 \in \mathbb{N}\) ，E2 ，Lev2
Lcop … \(a , b \in \mathbb{M} , a \cdot a = 2 \cdot ( b \cdot b ) \Longrightarrow \exists c \in \mathbb{M} . \exists d \in \mathbb{M} . a = 2 \cdot c , b = 2 \cdot d\) \(\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}\) ，Ldiv ，LG ，Euclid ，\(2 \in \mathbb{P}\) ，\(2 \in \mathbb{N}\) ，E2 ，Lev2 ，Lbd

2 主定理

最大公約数 \(g\) で割ると \(a^2 = 2b^2\) は変わらない（\(g \neq 0\)）。
Lcan … \(g , a , b \in \mathbb{M} , g \in \mathbb{N} , ( g \cdot a ) \cdot ( g \cdot a ) = 2 \cdot ( ( g \cdot b ) \cdot ( g \cdot b ) ) \Longrightarrow a \cdot a = 2 \cdot ( b \cdot b )\) \(\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}\) ，Ldiv ，LG ，Euclid ，\(2 \in \mathbb{P}\) ，\(2 \in \mathbb{N}\) ，E2 ，Lev2 ，Lbd ，Lcop ，Lcl
\(g\) が \(m, n\) の最大公約数なら、\(g \mid m\)・\(g \mid n\) で、\(m = ga\)・\(n = gb\) と書ける。\(a^2 = 2b^2\) から \(a = 2c\)・\(b = 2d\) となり、\(2g\) も公約数になるので \(2g \mid g\)。これは \(g \neq 0\) と矛盾する。
Lg … \(m , n , g \in \mathbb{M} , n \in \mathbb{N} , m \cdot m = 2 \cdot ( n \cdot n ) , g \mid m , g \mid n , \forall d \in \mathbb{M} . ( d \mid m , d \mid n \Longrightarrow d \mid g ) \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}\) ，Ldiv ，LG ，Euclid ，\(2 \in \mathbb{P}\) ，\(2 \in \mathbb{N}\) ，E2 ，Lev2 ，Lbd ，Lcop ，Lcl ，Lcan
\(n \neq 0\) とすると、最大公約数 \(g\)（69b）で矛盾が出る。したがって \(m^2 = 2n^2\) なら \(n = 0\)（\(m, n\) は自然数）。
√2 … \(m , n \in \mathbb{M} , m ^ 2 = 2 \cdot n ^ 2 \Longrightarrow n = 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}\) ，Ldiv ，LG ，Euclid ，\(2 \in \mathbb{P}\) ，\(2 \in \mathbb{N}\) ，E2 ，Lev2 ，Lbd ，Lcop ，Lcl ，Lcan ，Lg
すなわち \(m^2 = 2n^2\)、\(n \neq 0\) となる自然数 \(m, n\) は無い。
√2∄ … \(\neg \exists m \in \mathbb{M} . \exists n \in \mathbb{M} . n \neq 0 , m ^ 2 = 2 \cdot n ^ 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}\) ，Ldiv ，LG ，Euclid ，\(2 \in \mathbb{P}\) ，\(2 \in \mathbb{N}\) ，E2 ，Lev2 ，Lbd ，Lcop ，Lcl ，Lcan ，Lg ，√2