未ログイン ／
ログイン
← ファイル一覧
（保存にはログインが要ります）
articles3/10.book
ヘッダ
行番号
title Fermat の小定理 import 44 80-1 formel /common/default thmel /common/zf option review quick:true;
section 素数は二項係数を割る txt \((k+1)\binom{n+1}{k+1} = (n+1)\binom{n}{k}\)（\(n\) についての帰納法）から、素数 \(p\) は \(0 \lt k \lt p\) のとき \(\binom{p}{k}\) を割ります（ユークリッドの補題）。 let/thm Labs <- `[ n ; k col ∈ 𝕄 ] ⟹ (k suc) ⋅ ((n suc) choose (k suc)) = (n suc) ⋅ (n choose k)` ◀ 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , choose𝕄 , 1. prf Lb <- `[ ∀ k ∈ 𝕄 . (k suc) ⋅ ((0 suc) choose (k suc)) = (0 suc) ⋅ (0 choose k) ]` -| choose𝕄 , Lpred , *𝕄 , +𝕄 , choose∈𝕄 , 𝕄0s v; LA0 <- `n ∈ 𝕄 ⟹ 0 ⋅ ((n suc) choose 0) + (n suc) ⋅ (n choose 0) = (n suc) ⋅ ((n suc) choose 0)` -| choose𝕄 , L0⋅ , L0+ , ⋅∈𝕄 , choose∈𝕄 , 𝕄0s p; LAs <- `n ∈ 𝕄 and [ ∀ k ∈ 𝕄 . (k suc) ⋅ ((n suc) choose (k suc)) = (n suc) ⋅ (n choose k) ] and k ∈ 𝕄 ⟹ (k suc) ⋅ ((n suc) choose (k suc)) + (n suc) ⋅ (n choose (k suc)) = (n suc) ⋅ ((n suc) choose (k suc))` -| choose𝕄 , Ldist , choose∈𝕄 , 𝕄0s v; LA <- `n ∈ 𝕄 and [ ∀ k ∈ 𝕄 . (k suc) ⋅ ((n suc) choose (k suc)) = (n suc) ⋅ (n choose k) ] and k ∈ 𝕄 ⟹ k ⋅ ((n suc) choose k) + (n suc) ⋅ (n choose k) = (n suc) ⋅ ((n suc) choose k)` -| LA0 , LAs , Lpred v; ARa <- `[ k ; c ; d col ∈ 𝕄 ] ⟹ (k suc) ⋅ (c + d) = (k ⋅ c + c) + (k suc) ⋅ d` -| Ldist , ⋅C , *𝕄 , ⋅∈𝕄 , 𝕄0s p; AR <- `[ k ; c ; d ; e ; n col ∈ 𝕄 ] and (k suc) ⋅ d = (n suc) ⋅ e and k ⋅ c + (n suc) ⋅ e = (n suc) ⋅ c ⟹ (k suc) ⋅ (c + d) = ((n suc) suc) ⋅ c` -| ARa , +CA , suc⋅ , ⋅∈𝕄 , 𝕄0s v; Ls <- `n ∈ 𝕄 and [ ∀ k ∈ 𝕄 . (k suc) ⋅ ((n suc) choose (k suc)) = (n suc) ⋅ (n choose k) ] ⟹ [ ∀ k ∈ 𝕄 . (k suc) ⋅ (((n suc) suc) choose (k suc)) = ((n suc) suc) ⋅ ((n suc) choose k) ]` -| AR , LA , choose𝕄 , choose∈𝕄 , 𝕄0s v; Labs -| IND𝕄[C_:=`\{ cls n | [ ∀ k ∈ 𝕄 . (k suc) ⋅ ((n suc) choose (k suc)) = (n suc) ⋅ (n choose k) ] \}`] , Lb , Ls , 𝕄0s v; Labs -| 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , choose𝕄 , 1. h; let/thm ∣choose <- `p ∈ ℙ and [ k ; j col ∈ 𝕄 ] and p = (k suc) + (j suc) ⟹ p ∣ p choose (k suc)` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , choose𝕄 , 1. prf C1 <- `[ k ; j col ∈ 𝕄 ] ⟹ (k suc) + (j suc) = (k + j suc) suc` -| Lsuc+ , +𝕄 , 𝕄0s p; C2 <- `[ k ; j col ∈ 𝕄 ] and p = (k suc) + (j suc) ⟹ p ∣ (k suc) ⋅ (p choose (k suc))` -| Labs , C1 , ∣⋅ , +∈𝕄 , choose∈𝕄 , 𝕄0s v; C3a <- `[ k ; j col ∈ 𝕄 ] ⟹ k suc < (k suc) + (j suc)` -| L<+ , +C , suc𝕄 , 𝕄0s p; C3b <- `[ x ; y col ∈ 𝕄 ] and x < y ⟹ ¬ (y ≤ x)` / <. -| L≤T , L<irr / <. , 𝕄0s p; C3 <- `[ p ; k ; j col ∈ 𝕄 ] and p = (k suc) + (j suc) ⟹ ¬ (p ∣ k suc)` -| ∣≤ , C3a , C3b , suc𝕄 , +∈𝕄 , 𝕄0s p; ∣choose -| Euclid , Lℙ , C2 , C3 , choose∈𝕄 , +∈𝕄 , 𝕄0s v; ∣choose -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , choose𝕄 , 1. h; section (a+1)^p と a^p+1 txt 和 \(s(n)(m) = \sum_{k\lt m} \binom{n}{k} a^k\) を、44 と同じく漸化式を満たす関数として仮定します（存在は示しません）。二項定理（44）で \((a+1)^p = s(p)(p+1)\)。\(0\lt k\lt p\) の項は \(p\) で割り切れるので、\((a+1)^p\) は \(a^p+1\) と \(p\) の倍数だけ違います。したがって Fermat の小定理（主定理）は、前件「どの \(x\) にも和の関数 \(s\) がある」の下での条件付きの形です。 let/thm LF <- `\\{ And p ∈ ℙ \\ a ∈ 𝕄 \\ [ ∀ n ∈ 𝕄 . s ap (n) ap (0) = 0 ] \\ [ ∀ k ∈ 𝕄 . [ ∀ j ∈ 𝕄 . s ap (k + j) ap (k suc) = s ap (k + j) ap (k) + ((k + j) choose k) ⋅ a ↑ k ] ] \\} ⟹ [ ∃ t ∈ 𝕄 . (a + 1) ↑ p = (a ↑ p + 1) + p ⋅ t ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , ↑𝕄 , choose𝕄 , 1. prf hyP <- `|p ∈ ℙ` ; hyA <- `|a ∈ 𝕄` ; hy0 <- `[ ∀ n ∈ 𝕄 . |s ap (n) ap (0) = 0 ]` ; hyR <- `[ ∀ k ∈ 𝕄 . [ ∀ j ∈ 𝕄 . |s ap (k + j) ap (k suc) = |s ap (k + j) ap (k) + ((k + j) choose k) ⋅ |a ↑ k ] ]` ; L1↑ <- `j ∈ 𝕄 ⟹ 1 ↑ j = 1` -| IND𝕄[C_:=`\{ cls j | 1 ↑ j = 1 \}`] , ↑𝕄 , L⋅1 , `1 ∈ 𝕄` , 𝕄0s v; hyR1 <- `[ ∀ k ∈ 𝕄 . [ ∀ j ∈ 𝕄 . |s ap (k + j) ap (k suc) = |s ap (k + j) ap (k) + ((k + j) choose k) ⋅ (|a ↑ k ⋅ 1 ↑ j) ] ]` -| hyR , L1↑ , L⋅1 , ↑∈𝕄 , hyA p; B44 <- `(|a + 1) ↑ |p = |s ap (|p) ap (|p suc)` -| `\\{ And [ a ; b col ∈ 𝕄 ] \\ [ ∀ n ∈ 𝕄 . s ap (n) ap (0) = 0 ] \\ [ ∀ k ∈ 𝕄 . [ ∀ j ∈ 𝕄 . s ap (k + j) ap (k suc) = s ap (k + j) ap (k) + ((k + j) choose k) ⋅ (a ↑ k ⋅ b ↑ j) ] ] \\} and n ∈ 𝕄 ⟹ (a + b) ↑ n = s ap (n) ap (n suc)` , hyA , hy0 , hyR1 , Lℙ , hyP , `1 ∈ 𝕄` v; AR2 <- `[ p ; t ; c ; x col ∈ 𝕄 ] ⟹ (1 + p ⋅ t) + (p ⋅ c) ⋅ x = 1 + p ⋅ (t + c ⋅ x)` -| +A , Ldist , ⋅A , ⋅∈𝕄 , +∈𝕄 , `1 ∈ 𝕄` v; LQb <- `[ ∀ j ∈ 𝕄 . (0 + (j suc) = |p ⟹ [ ∃ t ∈ 𝕄 . |s ap (|p) ap (0 suc) = 1 + |p ⋅ t ]) ]` -| hyR , hy0 , choose𝕄 , ↑𝕄 , L0+ , L⋅1 , *𝕄 , +𝕄 , hyA , Lℙ , hyP , 𝕄0s , `1 ∈ 𝕄` v; LQs <- `m ∈ 𝕄 and [ ∀ j ∈ 𝕄 . (m + (j suc) = |p ⟹ [ ∃ t ∈ 𝕄 . |s ap (|p) ap (m suc) = 1 + |p ⋅ t ]) ] ⟹ [ ∀ j ∈ 𝕄 . ((m suc) + (j suc) = |p ⟹ [ ∃ t ∈ 𝕄 . |s ap (|p) ap ((m suc) suc) = 1 + |p ⋅ t ]) ]` -| hyR , ∣choose / ∣. , AR2 , Lsuc+ , +𝕄 , hyP , choose∈𝕄 , ↑∈𝕄 , ⋅∈𝕄 , +∈𝕄 , hyA , Lℙ , 𝕄0s v; LQ <- `m ∈ 𝕄 ⟹ [ ∀ j ∈ 𝕄 . (m + (j suc) = |p ⟹ [ ∃ t ∈ 𝕄 . |s ap (|p) ap (m suc) = 1 + |p ⋅ t ]) ]` -| IND𝕄[C_:=`\{ cls m | [ ∀ j ∈ 𝕄 . (m + (j suc) = |p ⟹ [ ∃ t ∈ 𝕄 . |s ap (|p) ap (m suc) = 1 + |p ⋅ t ]) ] \}`] , LQb , LQs , 𝕄0s v; Lpp <- `[ ∃ t ∈ 𝕄 . |s ap (|p) ap (|p) = 1 + |p ⋅ t ]` -| LQ , Lpred , Lℙ , hyP , +𝕄 , 𝕄0s p; Ltop <- `|s ap (|p) ap (|p suc) = |s ap (|p) ap (|p) + |a ↑ |p` -| hyR , Lnn , +𝕄 , ⋅C , L⋅1 , ↑∈𝕄 , hyA , Lℙ , hyP , 𝕄0s , `1 ∈ 𝕄` v; Lfix <- `[ ∃ t ∈ 𝕄 . (|a + 1) ↑ |p = (|a ↑ |p + 1) + |p ⋅ t ]` -| B44 , Ltop , Lpp , +A , +C , ↑∈𝕄 , ⋅∈𝕄 , hyA , Lℙ , hyP , `1 ∈ 𝕄` v; LF -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , ↑𝕄 , choose𝕄 , 1. h[fix]; section Fermat の小定理 txt \(p\) が素数なら \(a^p\) は \(a\) と \(p\) の倍数だけ違う（\(a^p \equiv a \pmod p\)）。自然数には引き算が無いので \(a^p = a + pq\) と書きます。\(a\) についての帰納法で、\((a+1)^p = (a^p + 1) + pt = (a+1) + p(q+t)\)。 thm `p ∈ ℙ and a ∈ 𝕄 and [ ∀ x ∈ 𝕄 . ∃ s ( [ ∀ n ∈ 𝕄 . s ap (n) ap (0) = 0 ] and [ ∀ k ∈ 𝕄 . [ ∀ j ∈ 𝕄 . s ap (k + j) ap (k suc) = s ap (k + j) ap (k) + ((k + j) choose k) ⋅ x ↑ k ] ] ) ] ⟹ [ ∃ q ∈ 𝕄 . a ↑ p = a + p ⋅ q ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , ↑𝕄 , choose𝕄 , 1. prf hyP <- `|p ∈ ℙ` ; hyA <- `|a ∈ 𝕄` ; hyS <- `[ ∀ x ∈ 𝕄 . ∃ s ( [ ∀ n ∈ 𝕄 . s ap (n) ap (0) = 0 ] and [ ∀ k ∈ 𝕄 . [ ∀ j ∈ 𝕄 . s ap (k + j) ap (k suc) = s ap (k + j) ap (k) + ((k + j) choose k) ⋅ x ↑ k ] ] ) ]` ; M0 <- `[ ∃ q ∈ 𝕄 . 0 ↑ |p = 0 + |p ⋅ q ]` -| Lpred , ↑𝕄 , *𝕄 , L0+ , ↑∈𝕄 , Lℙ , hyP , 𝕄0s v; MF <- `x ∈ 𝕄 ⟹ [ ∃ t ∈ 𝕄 . (x + 1) ↑ |p = (x ↑ |p + 1) + |p ⋅ t ]` -| LF , hyS , hyP v; MA <- `[ x ; y ; p ; q ; t col ∈ 𝕄 ] and y = x + p ⋅ q ⟹ (y + 1) + p ⋅ t = (x + 1) + p ⋅ (q + t)` -| +A , +C , Ldist , ⋅∈𝕄 , +∈𝕄 , `1 ∈ 𝕄` v; Ms <- `x ∈ 𝕄 and [ ∃ q ∈ 𝕄 . x ↑ |p = x + |p ⋅ q ] ⟹ [ ∃ q ∈ 𝕄 . (x suc) ↑ |p = x suc + |p ⋅ q ]` -| MF , MA , +1 , ↑∈𝕄 , ⋅∈𝕄 , +∈𝕄 , Lℙ , hyP , 𝕄0s v; Lall <- `x ∈ 𝕄 ⟹ [ ∃ q ∈ 𝕄 . x ↑ |p = x + |p ⋅ q ]` -| IND𝕄[C_:=`\{ cls x | [ ∃ q ∈ 𝕄 . x ↑ |p = x + |p ⋅ q ] \}`] , M0 , Ms , 𝕄0s v; Lfix <- `[ ∃ q ∈ 𝕄 . |a ↑ |p = |a + |p ⋅ q ]` -| Lall , hyA p; goal -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , ↑𝕄 , choose𝕄 , 1. h[fix];
表示（保存しません）
保存にはMatheliaへのログインが要ります。