book集

section 2乗
txt \(m^n\) は \(m\) の \(n\) 乗（ソースでは m ↑ n・0-pa の ↑𝕄）。
let/thm ↑2 <- `m ∈ 𝕄 ⟹ m ↑ 2 = m ⋅ m` ◀ 𝕄0s , IND𝕄 , +𝕄 , *𝕄 , ↑𝕄 , 1. , 2.
prf ↑2 -| ↑𝕄 , ⋅C , L⋅1 , 1. , 2. , 𝕄0s p;
    ↑2 -| 𝕄0s , IND𝕄 , +𝕄 , *𝕄 , ↑𝕄 , 1. , 2. h;

section 偶数と奇数
txt どの自然数も \(2k\) か \(2k+1\) のどちらか一方の形（0-pa の Lpar・Lne）。奇数の2乗は奇数なので、\(m^2\) が偶数なら \(m\) は偶数（Lev）。
let/thm Lev <- `[ m ; x col ∈ 𝕄 ] and m ⋅ m = 2 ⋅ x ⟹ [ ∃ k ∈ 𝕄 . m = 2 ⋅ k ]` ◀ 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , 2.
prf Lodd <- `[ k ; x col ∈ 𝕄 ] and (2 ⋅ k + 1) ⋅ (2 ⋅ k + 1) = 2 ⋅ x ⟹ ⊥` -| Sx2k1 , Lne , ⋅∈𝕄 , +∈𝕄 , 𝕄0s , 1. , 2. v;
    Lev -| Lpar , Lodd v;
    Lev -| 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , 2. h;

section 主定理
txt \(\sqrt{2}\) が分数 \(m/n\)（\(n \neq 0\)）で書けるなら \(m^2 = 2n^2\)。この本は有理数・実数を扱わないので、この言い換えは本の外で行い、本は「そのような自然数 \(m, n\) は無い」ことを示す（√2∄）。
txt \(m^2 = 2n^2\) なら \(m^2\) は偶数なので \(m = 2k\)、すると \(n^2 = 2k^2\) で \(n = 2j\)、さらに \(k^2 = 2j^2\)。
txt \(n \neq 0\) なら \(j < n\) で同じ形の解 \((k, j)\) ができる（無限降下）。\(n\) についての強い帰納法（SIND𝕄）で \(n = 0\)。
let/thm √2 <- `[ m ; n col ∈ 𝕄 ] and m ↑ 2 = 2 ⋅ n ↑ 2 ⟹ n = 0` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , ↑𝕄
prf Lsq <- `[ k ; x col ∈ 𝕄 ] and (2 ⋅ k) ⋅ (2 ⋅ k) = 2 ⋅ x ⟹ x = 2 ⋅ (k ⋅ k)` -| Sx2k , L2K , ⋅∈𝕄 , 𝕄0s , 1. , 2. v;
    Lj <- `j ∈ 𝕄 and 2 ⋅ j {/}= 0 ⟹ j < 2 ⋅ j` -| L2⋅ , L<+ , *𝕄 , 𝕄0s , 1. , 2. p;
    L1 <- `[ b ; m col ∈ 𝕄 ] and [ ∀ z ∈ 𝕄 . (z < b ⟹ [ ∀ m ∈ 𝕄 . (m ⋅ m = 2 ⋅ (z ⋅ z) ⟹ z = 0) ]) ] and m ⋅ m = 2 ⋅ (b ⋅ b) ⟹ b = 0` -| Lev , Lsq , Lj , ⋅∈𝕄 , *𝕄 , 𝕄0s , 1. , 2. v;
    L√ <- `[ m ; n col ∈ 𝕄 ] and m ⋅ m = 2 ⋅ (n ⋅ n) ⟹ n = 0` -| SIND𝕄[D_:=`\{ cls b | [ ∀ m ∈ 𝕄 . (m ⋅ m = 2 ⋅ (b ⋅ b) ⟹ b = 0) ] \}`] , L1 v;
    √2 -| L√ , ↑2 , ⋅∈𝕄 p;
    √2 -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , ↑𝕄 h;
txt すなわち \(m^2 = 2n^2\)、\(n \neq 0\) となる自然数 \(m, n\) は無い。
let/thm √2∄ <- `¬ [ ∃ m ∈ 𝕄 . [ ∃ n ∈ 𝕄 . n {/}= 0 and m ↑ 2 = 2 ⋅ n ↑ 2 ] ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , ↑𝕄
prf √2∄ -| √2 p;
    √2∄ -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , ↑𝕄 h;

articles3/1.book

`articles3/1.book`