book集

section 準備
txt 素数 \(p\) が \(k^2\) を割れば \(k\) を割る（∣k）。\(d \mid v\) なら \(d \mid vw\)（∣M）。
let/thm ∣k <- `p ∈ ℙ and k ∈ 𝕄 and p ∣ k ⋅ k ⟹ p ∣ k` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1.
prf ∣k -| Euclid , Lℙ p; ∣k -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. h;

section 主定理
txt 共通の素因数を持たない \(v, w\) について、\(vw = k^2\) なら \(v\) は平方数（Sq）。\(v\) についての強い帰納法で示します。
txt \(v \ge 2\) なら素因数 \(p\) をとると、\(p \mid k\) で \(p \nmid w\) なので \(v = p^2 u\)・\(uw = j^2\)（Dn）。\(u < v\) なので \(u\) は平方数、よって \(v\) も。
let/thm Dn <- `p ∈ ℙ and [ v ; w ; k col ∈ 𝕄 ] and p ∣ v and ¬ p ∣ w and v ⋅ w = k ⋅ k ⟹ [ ∃ u ∈ 𝕄 . [ ∃ j ∈ 𝕄 . v = (p ⋅ p) ⋅ u and u ⋅ w = j ⋅ j ] ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1.
prf A1 <- `[ p ; v ; w col ∈ 𝕄 ] ⟹ (p ⋅ v) ⋅ w = (v ⋅ w) ⋅ p` -| ⋅A , ⋅C , ⋅∈𝕄 v;
    A2 <- `[ p ; j col ∈ 𝕄 ] ⟹ (p ⋅ j) ⋅ (p ⋅ j) = (p ⋅ (j ⋅ j)) ⋅ p` -| ⋅A , ⋅C , ⋅∈𝕄 v;
    D1 <- `[ p ; v ; w ; j col ∈ 𝕄 ] and p {/}= 0 and (p ⋅ v) ⋅ w = (p ⋅ j) ⋅ (p ⋅ j) ⟹ v ⋅ w = p ⋅ (j ⋅ j)` -| A1 , A2 , ⋅K , ⋅∈𝕄 , ℕ.' v;
    D2 <- `[ p ; u ; w ; j col ∈ 𝕄 ] and p {/}= 0 and (p ⋅ u) ⋅ w = p ⋅ (j ⋅ j) ⟹ u ⋅ w = j ⋅ j` -| A1 , ⋅K , ⋅C , ⋅∈𝕄 , ℕ.' v;
    E1 <- `p ∈ ℙ and [ v ; w ; k col ∈ 𝕄 ] and p ∣ v and v ⋅ w = k ⋅ k ⟹ [ ∃ s ∈ 𝕄 . [ ∃ j ∈ 𝕄 . v = p ⋅ s and s ⋅ w = p ⋅ (j ⋅ j) ] ]` -| ∣k , ∣M , ∣. , D1 , Lℙ v;
    E2 <- `p ∈ ℙ and [ s ; w ; j col ∈ 𝕄 ] and ¬ p ∣ w and s ⋅ w = p ⋅ (j ⋅ j) ⟹ [ ∃ u ∈ 𝕄 . s = p ⋅ u and u ⋅ w = j ⋅ j ]` -| Euclid , ∣. , D2 , Lℙ , ⋅∈𝕄 v;
    Dn -| E1 , E2 , ⋅A , Lℙ v;
    Dn -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. h;
let/thm Sq <- `[ v ; w ; k col ∈ 𝕄 ] and v ⋅ w = k ⋅ k and ¬ [ ∃ q ∈ ℙ . q ∣ v and q ∣ w ] ⟹ [ ∃ n ∈ 𝕄 . v = n ⋅ n ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1.
prf Lt <- `[ p ; u ; v col ∈ 𝕄 ] and 2 ≤ p and v {/}= 0 and v = (p ⋅ p) ⋅ u ⟹ u < v` -| Llt , L<T , ⋅A , L0⋅ , *𝕄 , ⋅∈𝕄 , ℕ.' v;
    Cp <- `[ u ; v ; w ; p col ∈ 𝕄 ] and v = (p ⋅ p) ⋅ u and ¬ [ ∃ q ∈ ℙ . q ∣ v and q ∣ w ] ⟹ ¬ [ ∃ q ∈ ℙ . q ∣ u and q ∣ w ]` -| ∣T , ∣⋅ , ⋅C , ⋅∈𝕄 , Lℙ v;
    Sq2 <- `[ p ; n col ∈ 𝕄 ] ⟹ (p ⋅ p) ⋅ (n ⋅ n) = (p ⋅ n) ⋅ (p ⋅ n)` -| ⋅A , ⋅C , ⋅∈𝕄 v;
    hyV <- `|v ∈ 𝕄` ;
    hyI <- `[ ∀ z ∈ 𝕄 . (z < |v ⟹ [ ∀ w ∈ 𝕄 . [ ∀ k ∈ 𝕄 . (z ⋅ w = k ⋅ k and ¬ [ ∃ q ∈ ℙ . q ∣ z and q ∣ w ] ⟹ [ ∃ n ∈ 𝕄 . z = n ⋅ n ]) ] ]) ]` ;
    hyW <- `[ |w ; |k col ∈ 𝕄 ]` ;
    hyE <- `|v ⋅ |w = |k ⋅ |k` ;
    hyC <- `¬ [ ∃ q ∈ ℙ . q ∣ |v and q ∣ |w ]` ;
    S0 <- `|v = 0 ⟹ [ ∃ n ∈ 𝕄 . |v = n ⋅ n ]` -| *𝕄 , 𝕄0s p;
    S1 <- `|v = 1 ⟹ [ ∃ n ∈ 𝕄 . |v = n ⋅ n ]` -| L⋅1 , 1. , 𝕄0s p;
    S2b <- `[ u ; j col ∈ 𝕄 ] and u < |v and u ⋅ |w = j ⋅ j and ¬ [ ∃ q ∈ ℙ . q ∣ u and q ∣ |w ] ⟹ [ ∃ n ∈ 𝕄 . u = n ⋅ n ]` -| hyI , hyW v;
    S2a <- `[ p ; u ; j col ∈ 𝕄 ] and p ∈ ℙ and |v = (p ⋅ p) ⋅ u and u ⋅ |w = j ⋅ j and 2 ≤ |v ⟹ [ ∃ n ∈ 𝕄 . |v = n ⋅ n ]` -| Lt , Cp , S2b , Sq2 , hyV , hyW , hyC , Lℙ , L≠0 , ⋅∈𝕄 , ℕ.' v;
    S2 <- `2 ≤ |v ⟹ [ ∃ n ∈ 𝕄 . |v = n ⋅ n ]` -| Lpf , Dn , S2a , hyC , hyW , hyE , hyV , Lℙ v;
    LQ <- `[ ∃ n ∈ 𝕄 . |v = n ⋅ n ]` -| S0 , S1 , S2 , L2≤ , hyV , ℕ.' p;
    Lf <- `v ∈ 𝕄 and [ ∀ z ∈ 𝕄 . (z < v ⟹ [ ∀ w ∈ 𝕄 . [ ∀ k ∈ 𝕄 . (z ⋅ w = k ⋅ k and ¬ [ ∃ q ∈ ℙ . q ∣ z and q ∣ w ] ⟹ [ ∃ n ∈ 𝕄 . z = n ⋅ n ]) ] ]) ] and [ w ; k col ∈ 𝕄 ] and v ⋅ w = k ⋅ k and ¬ [ ∃ q ∈ ℙ . q ∣ v and q ∣ w ] ⟹ [ ∃ n ∈ 𝕄 . v = n ⋅ n ]` -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. h[fix];
    Sq -| SIND𝕄[D_:=`\{ cls v | [ ∀ w ∈ 𝕄 . [ ∀ k ∈ 𝕄 . (v ⋅ w = k ⋅ k and ¬ [ ∃ q ∈ ℙ . q ∣ v and q ∣ w ] ⟹ [ ∃ n ∈ 𝕄 . v = n ⋅ n ]) ] ] \}`] , Lf v;
    Sq -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. h;

articles3/23-1.book

`articles3/23-1.book`