book集

section 主定理
txt 最大公約数 \(a \gcd b\) は \(a\) と \(b\) の整数係数の和で書ける（Bézout）。自然数には引き算が無いので、\(a \gcd b = |as - bt|\) を「\(as = bt + a \gcd b\) か \(bt = as + a \gcd b\)」と述べます。
txt \(a + b\) についての強い帰納法で示します（69 の K と同じ組み立て）。\(b = 0\) なら \(s = 1, t = 0\)。\(a = c + b\) で \((c, b)\) に \(s, t\) があれば、\((a, b)\) には \(s, t + s\)。\(a < b\) なら入れ替えます。
thm `[ a ; b col ∈ 𝕄 ] ⟹ [ ∃ s ∈ 𝕄 . [ ∃ t ∈ 𝕄 . (a ⋅ s = b ⋅ t + a gcd b or b ⋅ t = a ⋅ s + a gcd b) ] ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , gcd𝕄
prf Q0 <- `a ∈ 𝕄 ⟹ [ ∃ s ∈ 𝕄 . [ ∃ t ∈ 𝕄 . (a ⋅ s = 0 ⋅ t + a gcd 0 or 0 ⋅ t = a ⋅ s + a gcd 0) ] ]` -| gcd𝕄 , L⋅1 , L0⋅ , L0+ , *𝕄 , 1. , 𝕄0s v;
    Qsw <- `[ a ; b col ∈ 𝕄 ] and [ ∃ s ∈ 𝕄 . [ ∃ t ∈ 𝕄 . (b ⋅ s = a ⋅ t + b gcd a or a ⋅ t = b ⋅ s + b gcd a) ] ] ⟹ [ ∃ s ∈ 𝕄 . [ ∃ t ∈ 𝕄 . (a ⋅ s = b ⋅ t + a gcd b or b ⋅ t = a ⋅ s + a gcd b) ] ]` -| gcd𝕄 v;
    S1 <- `[ b ; c ; s ; t ; g col ∈ 𝕄 ] and c ⋅ s = b ⋅ t + g ⟹ (c + b) ⋅ s = b ⋅ (t + s) + g` -| Rdist , Ldist , +A , +C , ⋅∈𝕄 v;
    S2 <- `[ b ; c ; s ; t ; g col ∈ 𝕄 ] and b ⋅ t = c ⋅ s + g ⟹ b ⋅ (t + s) = (c + b) ⋅ s + g` -| Rdist , Ldist , +A , +C , ⋅∈𝕄 v;
    Qst <- `[ a ; b ; c col ∈ 𝕄 ] and a = c + b and [ ∃ s ∈ 𝕄 . [ ∃ t ∈ 𝕄 . (c ⋅ s = b ⋅ t + c gcd b or b ⋅ t = c ⋅ s + c gcd b) ] ] ⟹ [ ∃ s ∈ 𝕄 . [ ∃ t ∈ 𝕄 . (a ⋅ s = b ⋅ t + a gcd b or b ⋅ t = a ⋅ s + a gcd b) ] ]` -| gcd𝕄 , S1 , S2 , K , +∈𝕄 v;
    Lle <- `[ m ; n col ∈ 𝕄 ] and m ≤ n ⟹ [ ∃ c ∈ 𝕄 . n = c + m ]` / ≤. -| O p;
    hyA <- `[ |a ; |b col ∈ 𝕄 ]` ;
    hyI <- `[ ∀ x ∈ 𝕄 . [ ∀ y ∈ 𝕄 . (x + y < |a + |b ⟹ [ ∃ s ∈ 𝕄 . [ ∃ t ∈ 𝕄 . (x ⋅ s = y ⋅ t + x gcd y or y ⋅ t = x ⋅ s + x gcd y) ] ]) ] ]` ;
    B0 <- `|b = 0 ⟹ [ ∃ s ∈ 𝕄 . [ ∃ t ∈ 𝕄 . (|a ⋅ s = |b ⋅ t + |a gcd |b or |b ⋅ t = |a ⋅ s + |a gcd |b) ] ]` -| Q0 , hyA p;
    A0 <- `|a = 0 ⟹ [ ∃ s ∈ 𝕄 . [ ∃ t ∈ 𝕄 . (|a ⋅ s = |b ⋅ t + |a gcd |b or |b ⋅ t = |a ⋅ s + |a gcd |b) ] ]` -| Q0 , Qsw , hyA v;
    C1 <- `|b {/}= 0 and |b ≤ |a ⟹ [ ∃ s ∈ 𝕄 . [ ∃ t ∈ 𝕄 . (|a ⋅ s = |b ⋅ t + |a gcd |b or |b ⋅ t = |a ⋅ s + |a gcd |b) ] ]` -| Lle , L<+ , +C , hyI , hyA , Qst v;
    C2 <- `|a {/}= 0 and |a < |b ⟹ [ ∃ s ∈ 𝕄 . [ ∃ t ∈ 𝕄 . (|a ⋅ s = |b ⋅ t + |a gcd |b or |b ⋅ t = |a ⋅ s + |a gcd |b) ] ]` -| L<≤ , Lle , L<+ , hyI , hyA , Qst , Qsw v;
    LQ <- `[ ∃ s ∈ 𝕄 . [ ∃ t ∈ 𝕄 . (|a ⋅ s = |b ⋅ t + |a gcd |b or |b ⋅ t = |a ⋅ s + |a gcd |b) ] ]` -| B0 , A0 , C1 , C2 , Ltot , hyA p;
    Lf <- `[ a ; b col ∈ 𝕄 ] and [ ∀ x ∈ 𝕄 . [ ∀ y ∈ 𝕄 . (x + y < a + b ⟹ [ ∃ s ∈ 𝕄 . [ ∃ t ∈ 𝕄 . (x ⋅ s = y ⋅ t + x gcd y or y ⋅ t = x ⋅ s + x gcd y) ] ]) ] ] ⟹ [ ∃ s ∈ 𝕄 . [ ∃ t ∈ 𝕄 . (a ⋅ s = b ⋅ t + a gcd b or b ⋅ t = a ⋅ s + a gcd b) ] ]` -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , gcd𝕄 h[fix];
    goal -| SIND𝕄[D_:=`\{ cls n | [ ∀ x ∈ 𝕄 . [ ∀ y ∈ 𝕄 . (x + y = n ⟹ [ ∃ s ∈ 𝕄 . [ ∃ t ∈ 𝕄 . (x ⋅ s = y ⋅ t + x gcd y or y ⋅ t = x ⋅ s + x gcd y) ] ]) ] ] \}`] , Lf , +∈𝕄 v;
    goal -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , gcd𝕄 h;

articles3/60.book

`articles3/60.book`