book集

section 互除法
txt 互除法は、大きい方から小さい方を引くことを繰り返して最大公約数を求めます。ここでは \(a \gcd b\) を、次の漸化式（gcd𝕄）を満たす関数として仮定します。そのような関数が存在することは示しません。したがって、互除法が止まって値が決まること（そのような関数の存在）はこの本では示していません。主定理は「gcd𝕄 を満たす関数があれば、それは最大公約数」という形です。
txt \(a \gcd 0 = a\)、\(a \gcd b = b \gcd a\)、\((a + b) \gcd b = a \gcd b\)。
word gcd
prop gcd𝕄 <- `\\{ And a ∈ 𝕄 ⟹ a gcd 0 = a \\ [ a ; b col ∈ 𝕄 ] ⟹ a gcd b = b gcd a \\ [ a ; b col ∈ 𝕄 ] ⟹ (a + b) gcd b = a gcd b \\}`

subsection 公約数は最大公約数の約数
txt \(a \gcd b\) は自然数で、\(d\) が \(a\) と \(b\) を割ることと \(a \gcd b\) を割ることは同じ（K）。
txt \(a + b\) についての強い帰納法で示します。\(b = 0\) なら \(a \gcd 0 = a\)。\(a = c + b\) なら \(a \gcd b = c \gcd b\) で、公約数も同じ（0-pa の ∣+・∣sub）。\(a < b\) なら入れ替えます。
let/thm K <- `[ a ; b ; d col ∈ 𝕄 ] ⟹ a gcd b ∈ 𝕄 and (d ∣ a and d ∣ b ⟺ d ∣ a gcd b)` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , gcd𝕄
prf Q0 <- `[ a ; d col ∈ 𝕄 ] ⟹ a gcd 0 ∈ 𝕄 and (d ∣ a and d ∣ 0 ⟺ d ∣ a gcd 0)` / ∣. -| gcd𝕄 , *𝕄 , 𝕄0s p;
    Qsw <- `[ a ; b ; d col ∈ 𝕄 ] and b gcd a ∈ 𝕄 and (d ∣ b and d ∣ a ⟺ d ∣ b gcd a) ⟹ a gcd b ∈ 𝕄 and (d ∣ a and d ∣ b ⟺ d ∣ a gcd b)` -| gcd𝕄 p;
    Qst <- `[ a ; b ; c ; d col ∈ 𝕄 ] and a = c + b and c gcd b ∈ 𝕄 and (d ∣ c and d ∣ b ⟺ d ∣ c gcd b) ⟹ a gcd b ∈ 𝕄 and (d ∣ a and d ∣ b ⟺ d ∣ a gcd b)` -| gcd𝕄 , ∣+ , ∣sub , +C p;
    Lle <- `[ m ; n col ∈ 𝕄 ] and m ≤ n ⟹ [ ∃ c ∈ 𝕄 . n = c + m ]` / ≤. -| O p;
    hyA <- `[ |a ; |b ; |d col ∈ 𝕄 ]` ;
    hyI <- `[ ∀ x ∈ 𝕄 . [ ∀ y ∈ 𝕄 . (x + y < |a + |b ⟹ x gcd y ∈ 𝕄 and (|d ∣ x and |d ∣ y ⟺ |d ∣ x gcd y)) ] ]` ;
    B0 <- `|b = 0 ⟹ |a gcd |b ∈ 𝕄 and (|d ∣ |a and |d ∣ |b ⟺ |d ∣ |a gcd |b)` -| Q0 , hyA p;
    A0 <- `|a = 0 ⟹ |a gcd |b ∈ 𝕄 and (|d ∣ |a and |d ∣ |b ⟺ |d ∣ |a gcd |b)` -| Q0 , Qsw , hyA v;
    C1 <- `|b {/}= 0 and |b ≤ |a ⟹ |a gcd |b ∈ 𝕄 and (|d ∣ |a and |d ∣ |b ⟺ |d ∣ |a gcd |b)` -| Lle , L<+ , +C , hyI , hyA , Qst v;
    C2 <- `|a {/}= 0 and |a < |b ⟹ |a gcd |b ∈ 𝕄 and (|d ∣ |a and |d ∣ |b ⟺ |d ∣ |a gcd |b)` -| L<≤ , Lle , L<+ , hyI , hyA , Qst , Qsw v;
    LQ <- `|a gcd |b ∈ 𝕄 and (|d ∣ |a and |d ∣ |b ⟺ |d ∣ |a gcd |b)` -| B0 , A0 , C1 , C2 , Ltot , hyA p;
    Lf <- `[ a ; b ; d col ∈ 𝕄 ] and [ ∀ x ∈ 𝕄 . [ ∀ y ∈ 𝕄 . (x + y < a + b ⟹ x gcd y ∈ 𝕄 and (d ∣ x and d ∣ y ⟺ d ∣ x gcd y)) ] ] ⟹ a gcd b ∈ 𝕄 and (d ∣ a and d ∣ b ⟺ d ∣ a gcd b)` -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , gcd𝕄 h[fix];
    K -| SIND𝕄[D_:=`\{ cls n | [ ∀ x ∈ 𝕄 . [ ∀ y ∈ 𝕄 . (x + y = n ⟹ x gcd y ∈ 𝕄 and (d ∣ x and d ∣ y ⟺ d ∣ x gcd y)) ] ] \}`] , Lf , +∈𝕄 v;
    K -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , gcd𝕄 h;

section 主定理
txt 互除法で求めた \(a \gcd b\) は \(a\) と \(b\) の公約数で、どの公約数でも割り切れる＝最大公約数（K で \(d = a \gcd b\) とおく）。
thm `[ a ; b col ∈ 𝕄 ] ⟹ a gcd b ∣ a and a gcd b ∣ b and [ ∀ d ∈ 𝕄 . (d ∣ a and d ∣ b ⟹ d ∣ a gcd b) ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , gcd𝕄
prf goal -| K , ∣R , 𝕄0s v;
    goal -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , gcd𝕄 h;

articles3/69.book

`articles3/69.book`