book集

section 互除法の漸化式
txt \(a \gcd b\) を、互除法の漸化式（gcd𝕄・articles3/69 と同じ）を満たす関数として仮定します。それが最大公約数であることは 69 で示しました（69 は自然数を公理で与えた本なので、ここでは import せず仮定だけを書きます）。
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 \\}`

section 主定理
txt 自然数 \(a, b\) に対して、\(as + bt = a \gcd b\) となる整数 \(s, t\) がある（Bézout）。
txt \(a + b\) についての強い帰納法で示します。\(b = 0\) なら \(s = 1, t = 0\)。\(a = c + b\) で \(cs + bt = c \gcd b\) なら \(as + b(t - s) = a \gcd b\)。\(a < b\) なら入れ替えます。
thm `[ a ; b col ∈ 𝕄 ] ⟹ [ ∃ s ∈ ℤ . [ ∃ t ∈ ℤ . a ⋅ s + b ⋅ t = a gcd b ] ]` ◀ W. , ax_s , +𝕄 , *𝕄 , -ℤ , +ℤ , *ℤ , gcd𝕄
prf L0 <- `0 ∈ 𝕄` / 𝕄. -| O p;
    L1 <- `1 ∈ 𝕄 and (a ∈ 𝕄 ⟹ a ⋅ 1 = a)` -| ⋅𝕄:C , *𝕄 , +𝕄 , +𝕄:C , 1.. , L0 , 𝕄1 v;
    Q0 <- `a ∈ 𝕄 ⟹ [ ∃ s ∈ ℤ . [ ∃ t ∈ ℤ . a ⋅ s + 0 ⋅ t = a gcd 0 ] ]` -| gcd𝕄 , L1 , L0 , 𝕄⊂ℤ , *𝕄 , +𝕄 v;
    Qsw <- `[ a ; b col ∈ 𝕄 ] and [ ∃ s ∈ ℤ . [ ∃ t ∈ ℤ . b ⋅ s + a ⋅ t = b gcd a ] ] ⟹ [ ∃ s ∈ ℤ . [ ∃ t ∈ ℤ . a ⋅ s + b ⋅ t = a gcd b ] ]` -| gcd𝕄 , +ℤ:C , ⋅∈ℤ , 𝕄⊂ℤ p;
    R2b <- `[ b ; s ; t col ∈ ℤ ] ⟹ b ⋅ (t + (- s)) = b ⋅ t + (- (b ⋅ s))` -| ⋅- , ⋅ℤ+ , +ℤ- v;
    R2c <- `[ p ; q ; r col ∈ ℤ ] ⟹ (p + q) + (r + (- q)) = p + r` -| +ℤ:A , +ℤ:C , +ℤ- , `0 ∈_ unit (ℤ , [+])` , +∈ℤ v;
    R2 <- `[ c ; b ; s ; t col ∈ ℤ ] ⟹ (c + b) ⋅ s + b ⋅ (t + (- s)) = c ⋅ s + b ⋅ t` -| +⋅ , R2b , R2c , ⋅∈ℤ v;
    Qst <- `[ a ; b ; c col ∈ 𝕄 ] and a = c + b and [ ∃ s ∈ ℤ . [ ∃ t ∈ ℤ . c ⋅ s + b ⋅ t = c gcd b ] ] ⟹ [ ∃ s ∈ ℤ . [ ∃ t ∈ ℤ . a ⋅ s + b ⋅ t = a gcd b ] ]` -| gcd𝕄 , R2 , 𝕄⊂ℤ , +ℤ- , +∈ℤ v;
    hyA <- `[ |a ; |b col ∈ 𝕄 ]` ;
    hyI <- `[ ∀ x ∈ 𝕄 . [ ∀ y ∈ 𝕄 . (x + y ∈ |a + |b ⟹ [ ∃ s ∈ ℤ . [ ∃ t ∈ ℤ . x ⋅ s + y ⋅ t = x gcd y ] ]) ] ]` ;
    B0 <- `|b = 0 ⟹ [ ∃ s ∈ ℤ . [ ∃ t ∈ ℤ . |a ⋅ s + |b ⋅ t = |a gcd |b ] ]` -| Q0 , hyA p;
    A0 <- `|a = 0 ⟹ [ ∃ s ∈ ℤ . [ ∃ t ∈ ℤ . |a ⋅ s + |b ⋅ t = |a gcd |b ] ]` -| Q0 , Qsw , hyA v;
    C1 <- `|b {/}= 0 and |b ⊂ |a ⟹ [ ∃ s ∈ ℤ . [ ∃ t ∈ ℤ . |a ⋅ s + |b ⋅ t = |a gcd |b ] ]` -| Lsub , ∈+ , +𝕄:C , hyI , hyA , Qst v;
    C2 <- `|a {/}= 0 and |a ⊂ |b ⟹ [ ∃ s ∈ ℤ . [ ∃ t ∈ ℤ . |a ⋅ s + |b ⋅ t = |a gcd |b ] ]` -| Lsub , ∈+ , +𝕄:C , hyI , hyA , Qst , Qsw v;
    LQ <- `[ ∃ s ∈ ℤ . [ ∃ t ∈ ℤ . |a ⋅ s + |b ⋅ t = |a gcd |b ] ]` -| B0 , A0 , C1 , C2 , <𝕄:T , hyA v;
    Lf <- `[ a ; b col ∈ 𝕄 ] and [ ∀ x ∈ 𝕄 . [ ∀ y ∈ 𝕄 . (x + y ∈ a + b ⟹ [ ∃ s ∈ ℤ . [ ∃ t ∈ ℤ . x ⋅ s + y ⋅ t = x gcd y ] ]) ] ] ⟹ [ ∃ s ∈ ℤ . [ ∃ t ∈ ℤ . a ⋅ s + b ⋅ t = a gcd b ] ]` -| W. , ax_s , +𝕄 , *𝕄 , -ℤ , +ℤ , *ℤ , gcd𝕄 h[fix];
    goal -| SINDC[D_:=`\{ cls n | [ ∀ x ∈ 𝕄 . [ ∀ y ∈ 𝕄 . (x + y = n ⟹ [ ∃ s ∈ ℤ . [ ∃ t ∈ ℤ . x ⋅ s + y ⋅ t = x gcd y ] ]) ] ] \}`] , Lf , LinM , +∈𝕄 v;
    goal -| W. , ax_s , +𝕄 , *𝕄 , -ℤ , +ℤ , *ℤ , gcd𝕄 h;

articles4/60b.book

`articles4/60b.book`