book集

section 素因数の存在
txt 2以上の \(n\) が素数でなければ、\(1\) でも \(n\) でもない約数 \(d\)（\(2 \le d < n\)）があり、\(d\) の素因数は \(n\) の素因数（\(n\) についての強い帰納法 SIND𝕄）。
let/thm Lpf <- `n ∈ 𝕄 and 2 ≤ n ⟹ [ ∃ p ∈ ℙ . p ∣ n ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄
prf M1 <- `[ n ; d col ∈ 𝕄 ] and 2 ≤ n and d ∣ n ⟹ d {/}= 0` / ∣. -| L0⋅ , L≠0 p;
    M2 <- `[ n ; d col ∈ 𝕄 ] and 2 ≤ n and d ∣ n and d {/}= n ⟹ d < n` -| ∣≤ / ≤. , L≠0 , L0+ , L<+ p;
    Lcomp <- `[ n ; d col ∈ 𝕄 ] and 2 ≤ n and d ∣ n and d {/}= 1 and d {/}= n ⟹ 2 ≤ d and d < n` -| M1 , M2 , L2≤ p;
    L2 <- `b ∈ 𝕄 and 2 ≤ b and b {/}∈ ℙ ⟹ [ ∃ d ∈ 𝕄 . d ∣ b and d {/}= 1 and d {/}= b ]` / ℙ.' -| O p;
    L3 <- `[ ∀ z ∈ 𝕄 . (z < b and 2 ≤ z ⟹ [ ∃ p ∈ ℙ . p ∣ z ]) ] and [ b ; d col ∈ 𝕄 ] and d < b and 2 ≤ d and d ∣ b ⟹ [ ∃ p ∈ ℙ . p ∣ b ]` -| ∣T , ℙ.' p;
    L4 <- `b ∈ 𝕄 and [ ∀ z ∈ 𝕄 . (z < b ⟹ (2 ≤ z ⟹ [ ∃ p ∈ ℙ . p ∣ z ])) ] ⟹ (2 ≤ b ⟹ [ ∃ p ∈ ℙ . p ∣ b ])` -| Lcomp , ∣R , L2 , L3 v;
    Lpf -| SIND𝕄[D_:=`\{ cls b | 2 ≤ b ⟹ [ ∃ p ∈ ℙ . p ∣ b ] \}`] , L4 v;
    Lpf -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 h;

section 主定理
txt \(n\) より大きい素数がある、すなわち素数は無限にある（ユークリッドの証明）。
txt \(n\) 以下の \(0\) でないすべての数で割り切れる \(N \neq 0\) がある（\(n\) についての帰納法・次は \(N \cdot (n+1)\)）。
txt \(N+1 \ge 2\) の素因数を \(p\) とする。\(p \le n\) なら \(p \mid N\) と \(p \mid N+1\) が矛盾するので \(n < p\)。
let/thm LN <- `n ∈ 𝕄 ⟹ [ ∃ N ∈ 𝕄 . N {/}= 0 and [ ∀ d ∈ 𝕄 . (d {/}= 0 and d ≤ n ⟹ d ∣ N) ] ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄
prf Lb <- `[ ∃ N ∈ 𝕄 . N {/}= 0 and [ ∀ d ∈ 𝕄 . (d {/}= 0 and d ≤ 0 ⟹ d ∣ N) ] ]` -| L≤0 , 𝕄0s , 1. , suc𝕄 p;
    S1 <- `[ N ; n col ∈ 𝕄 ] and N {/}= 0 ⟹ N ⋅ n suc {/}= 0` -| *𝕄 , Lpred , +𝕄 , suc𝕄 , ⋅∈𝕄 , +∈𝕄 v;
    Ls <- `n ∈ 𝕄 and [ ∃ N ∈ 𝕄 . N {/}= 0 and [ ∀ d ∈ 𝕄 . (d {/}= 0 and d ≤ n ⟹ d ∣ N) ] ] ⟹ [ ∃ N ∈ 𝕄 . N {/}= 0 and [ ∀ d ∈ 𝕄 . (d {/}= 0 and d ≤ n suc ⟹ d ∣ N) ] ]` -| L≤suc , S1 , ∣M , ∣⋅R , ⋅∈𝕄 , 𝕄0s v;
    LN -| IND𝕄[C_:=`\{ cls n | [ ∃ N ∈ 𝕄 . N {/}= 0 and [ ∀ d ∈ 𝕄 . (d {/}= 0 and d ≤ n ⟹ d ∣ N) ] ] \}`] , Lb , Ls v;
    LN -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 h;
let/thm Lcop <- `p ∈ ℙ and N ∈ 𝕄 and p ∣ N and p ∣ N + 1 ⟹ ⊥` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄
prf Lcop -| ∣sub , ℙ∤1 , Lℙ , `1 ∈ 𝕄` p;
    Lcop -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 h;
let/thm Linf <- `n ∈ 𝕄 ⟹ [ ∃ p ∈ ℙ . n < p ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄
prf L2 <- `N ∈ 𝕄 and N {/}= 0 ⟹ 2 ≤ N + 1` -| L2≤ , +𝕄 , 1. , suc𝕄 , 𝕄0s , +∈𝕄 v;
    L3 <- `[ n ; N ; p col ∈ 𝕄 ] and [ ∀ d ∈ 𝕄 . (d {/}= 0 and d ≤ n ⟹ d ∣ N) ] and p ∈ ℙ and p ∣ N + 1 ⟹ n < p` -| Ltot , Lcop , ℙ.' , L≠0 p;
    Linf -| LN , L2 , Lpf , L3 , ℙ.' , +∈𝕄 , 𝕄0s , 1. v;
    Linf -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 h;

articles3/11.book

`articles3/11.book`