book集

section 主定理
txt \(a^2 + b^2 = c^2\) で \(a, b\) が互いに素、\(b\) が偶数なら、\(a = m^2 - n^2\)・\(b = 2mn\)・\(c = m^2 + n^2\) となる自然数 \(m, n\) がある。自然数には引き算が無いので \(a = m^2 - n^2\) を \(a + n^2 = m^2\) と書きます。
txt 証明：\(a \le c\) なので \(c = a + e\)。\(e^2 + 2ae = b^2\) から \(e\) は偶数で \(e = 2v\)、\(b = 2k\) とおくと \(v(v + a) = k^2\)。\(v\) と \(v + a\) は共通の素因数を持たないので、どちらも平方数 \(n^2\)・\(m^2\)（23-1 の Sq）。
thm `[ a ; b ; c col ∈ 𝕄 ] and a ⋅ a + b ⋅ b = c ⋅ c and [ ∀ d ∈ 𝕄 . (d ∣ a and d ∣ b ⟹ d = 1) ] and 2 ∣ b ⟹ [ ∃ m ∈ 𝕄 . [ ∃ n ∈ 𝕄 . a + n ⋅ n = m ⋅ m and b = 2 ⋅ (m ⋅ n) and c = m ⋅ m + n ⋅ n ] ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , 2.
prf L≠ <- `f ∈ 𝕄 and f {/}= 0 ⟹ f ⋅ f {/}= 0` -| Lpred , *𝕄 , L+=0 , ⋅∈𝕄 , 𝕄0s v;
    Q2a <- `[ x ; d col ∈ 𝕄 ] and d {/}= 0 ⟹ d ⋅ d + 2 ⋅ (d ⋅ x) {/}= 0` -| L≠ , L+=0 , ⋅∈𝕄 , `2 ∈ 𝕄` v;
    Q2 <- `[ x ; d col ∈ 𝕄 ] and d {/}= 0 ⟹ x ⋅ x < (d + x) ⋅ (d + x)` -| Sx , Q2a , L<+ , ⋅∈𝕄 , +∈𝕄 , `2 ∈ 𝕄` v;
    Q< <- `[ x ; y col ∈ 𝕄 ] and x < y ⟹ x ⋅ x < y ⋅ y` -| L<d , Q2 v;
    QK <- `[ x ; y col ∈ 𝕄 ] and x ⋅ x = y ⋅ y ⟹ x = y` -| Q< , L<irr , Ltot , L<≤ , L≤A , ⋅∈𝕄 v;
    hy1 <- `[ |a ; |b ; |c col ∈ 𝕄 ]` ;
    hyE <- `|a ⋅ |a + |b ⋅ |b = |c ⋅ |c` ;
    hyC <- `[ ∀ d ∈ 𝕄 . (d ∣ |a and d ∣ |b ⟹ d = 1) ]` ;
    hy2 <- `2 ∣ |b` ;
    T1a <- `[ x ; y ; z col ∈ 𝕄 ] and x < y and y ≤ z ⟹ x < z` / <. -| L≤T , 𝕄0s v;
    T1b <- `[ a ; b col ∈ 𝕄 ] ⟹ a ⋅ a ≤ a ⋅ a + b ⋅ b` / ≤. -| +C , ⋅∈𝕄 p;
    T1 <- `|a ≤ |c` -| Ltot , Q< , T1a , T1b , L<irr , hyE , hy1 , ⋅∈𝕄 , +∈𝕄 v;
    T1e <- `[ ∃ e ∈ 𝕄 . |c = e + |a ]` -| T1 / ≤. p;
    T2a <- `e ∈ 𝕄 and |c = e + |a ⟹ e ⋅ e + 2 ⋅ (e ⋅ |a) = |b ⋅ |b` -| Sx , hyE , hy1 , +K , +C , ⋅∈𝕄 , +∈𝕄 , `2 ∈ 𝕄` v;
    T2 <- `[ ∃ e ∈ 𝕄 . |c = e + |a and e ⋅ e + 2 ⋅ (e ⋅ |a) = |b ⋅ |b ]` -| T1e , T2a v;
    Od3 <- `[ x ; s col ∈ 𝕄 ] ⟹ (2 ⋅ x + 1) + 2 ⋅ s = 2 ⋅ (x + s) + 1` -| Ldist , +A , +C , ⋅∈𝕄 , `2 ∈ 𝕄` , 1. , 𝕄0s v;
    Od <- `[ t ; s col ∈ 𝕄 ] ⟹ (2 ⋅ t + 1) ⋅ (2 ⋅ t + 1) + 2 ⋅ s = 2 ⋅ (2 ⋅ (t ⋅ t + t) + s) + 1` -| Sx2k1 , Od3 , ⋅∈𝕄 , +∈𝕄 , `2 ∈ 𝕄` v;
    T3o <- `[ t ; k col ∈ 𝕄 ] and (2 ⋅ t + 1) ⋅ (2 ⋅ t + 1) + 2 ⋅ ((2 ⋅ t + 1) ⋅ |a) = (2 ⋅ k) ⋅ (2 ⋅ k) ⟹ ⊥` -| Od , Sx2k , Lne , ⋅∈𝕄 , +∈𝕄 , `2 ∈ 𝕄` , hy1 , 1. , 𝕄0s v;
    T3 <- `[ e ; k col ∈ 𝕄 ] and e ⋅ e + 2 ⋅ (e ⋅ |a) = (2 ⋅ k) ⋅ (2 ⋅ k) ⟹ [ ∃ v ∈ 𝕄 . e = 2 ⋅ v ]` -| Lpar , T3o v;
    T4b <- `[ v ; a col ∈ 𝕄 ] ⟹ (2 ⋅ v) ⋅ a = 2 ⋅ (v ⋅ a)` -| ⋅A , `2 ∈ 𝕄` v;
    T4c <- `[ x ; y col ∈ 𝕄 ] ⟹ 2 ⋅ (2 ⋅ x) + 2 ⋅ (2 ⋅ y) = 2 ⋅ (2 ⋅ (x + y))` -| Ldist , ⋅∈𝕄 , +∈𝕄 , `2 ∈ 𝕄` v;
    T4a <- `v ∈ 𝕄 ⟹ (2 ⋅ v) ⋅ (2 ⋅ v) + 2 ⋅ ((2 ⋅ v) ⋅ |a) = 2 ⋅ (2 ⋅ (v ⋅ (v + |a)))` -| Sx2k , T4b , T4c , Ldist , ⋅∈𝕄 , hy1 v;
    T4 <- `[ v ; k col ∈ 𝕄 ] and (2 ⋅ v) ⋅ (2 ⋅ v) + 2 ⋅ ((2 ⋅ v) ⋅ |a) = (2 ⋅ k) ⋅ (2 ⋅ k) ⟹ v ⋅ (v + |a) = k ⋅ k` -| T4a , Sx2k , L2K , ⋅∈𝕄 , +∈𝕄 , `2 ∈ 𝕄` , hy1 v;
    T5b <- `q ∈ ℙ and [ v ; k col ∈ 𝕄 ] and v ⋅ (v + |a) = k ⋅ k and q ∣ v ⟹ q ∣ k` -| ∣M , ∣k , Lℙ , +∈𝕄 , hy1 v;
    T5c <- `[ q ; k col ∈ 𝕄 ] and q ∣ k ⟹ q ∣ 2 ⋅ k` -| ∣M , ⋅C , `2 ∈ 𝕄` v;
    T5a <- `q ∈ ℙ and [ v ; k col ∈ 𝕄 ] and |b = 2 ⋅ k and v ⋅ (v + |a) = k ⋅ k and q ∣ v and q ∣ v + |a ⟹ ⊥` -| ∣sub , T5b , T5c , hyC , Lℙ , hy1 v;
    T5 <- `[ v ; k col ∈ 𝕄 ] and |b = 2 ⋅ k and v ⋅ (v + |a) = k ⋅ k ⟹ ¬ [ ∃ q ∈ ℙ . q ∣ v and q ∣ v + |a ]` -| T5a v;
    T6 <- `[ v ; k col ∈ 𝕄 ] and |b = 2 ⋅ k and v ⋅ (v + |a) = k ⋅ k ⟹ [ ∃ n ∈ 𝕄 . v = n ⋅ n ] and [ ∃ m ∈ 𝕄 . v + |a = m ⋅ m ]` -| T5 , Sq , ⋅C , hy1 , +∈𝕄 v;
    T7 <- `[ v ; k ; m ; n col ∈ 𝕄 ] and v ⋅ (v + |a) = k ⋅ k and v = n ⋅ n and v + |a = m ⋅ m ⟹ k = m ⋅ n` -| QK , ⋅A , ⋅C , ⋅∈𝕄 , hy1 v;
    hy2e <- `[ ∃ k ∈ 𝕄 . |b = 2 ⋅ k ]` -| hy2 / ∣. p;
    F1 <- `[ e ; v ; k ; m ; n col ∈ 𝕄 ] and |c = e + |a and e = 2 ⋅ v and |b = 2 ⋅ k and v = n ⋅ n and v + |a = m ⋅ m and k = m ⋅ n ⟹ |a + n ⋅ n = m ⋅ m and |b = 2 ⋅ (m ⋅ n) and |c = m ⋅ m + n ⋅ n` -| L2⋅ , +A , +C , ⋅∈𝕄 , hy1 v;
    F2 <- `[ e ; k col ∈ 𝕄 ] and |c = e + |a and e ⋅ e + 2 ⋅ (e ⋅ |a) = |b ⋅ |b and |b = 2 ⋅ k ⟹ [ ∃ m ∈ 𝕄 . [ ∃ n ∈ 𝕄 . |a + n ⋅ n = m ⋅ m and |b = 2 ⋅ (m ⋅ n) and |c = m ⋅ m + n ⋅ n ] ]` -| T3 , T4 , T6 , T7 , F1 , ⋅∈𝕄 , `2 ∈ 𝕄` v;
    LQ <- `[ ∃ m ∈ 𝕄 . [ ∃ n ∈ 𝕄 . |a + n ⋅ n = m ⋅ m and |b = 2 ⋅ (m ⋅ n) and |c = m ⋅ m + n ⋅ n ] ]` -| T2 , hy2e , F2 v;
    goal -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , 2. h[fix];

articles3/23.book

`articles3/23.book`