未ログイン ／
ログイン
← ファイル一覧
（保存にはログインが要ります）
articles3/80.book
ヘッダ
行番号
title 素因数分解 import 80-1 formel /common/default thmel /common/zf option review quick:true;
section 列の積 txt 列 \(f\) は \(f(0), f(1), \ldots\) を値に持つものとし、\(f \prod k\) は最初の \(k\) 項の積 \(f(0) \cdot \ldots \cdot f(k-1)\)。\(+\)・\(\cdot\) と同じく漸化式を満たす演算として仮定します。 txt 列の頭に1項を足せること（seq𝕄）も仮定します。 word ap word prod prop prod𝕄 <- `\\{ And f prod 0 = 1 \\ k ∈ 𝕄 ⟹ f prod (k suc) = (f prod k) ⋅ f ap (k) \\}` prop seq𝕄 <- `[ ∃ g \, (g ap (0) = p and [ ∀ i ∈ 𝕄 . g ap (i suc) = f ap (i) ]) ]` txt \(f\) の最初の \(k\) 項が素数で昇順のとき \(f\) ℙasc \(k\) と書きます。 word ℙasc prop ℙasc. <- `f ℙasc k ⟺ [ ∀ i ∈ 𝕄 . (i < k ⟹ f ap (i) ∈ ℙ) ] and [ ∀ i ∈ 𝕄 . (i suc < k ⟹ f ap (i) ≤ f ap (i suc)) ]` !let/thm Lres <- `k ∈ 𝕄 and f ℙasc (k suc) ⟹ f ℙasc k` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 prf Lres / ℙasc. -| L<K , 𝕄0s p; Lres -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 h; !let/thm LPH <- `f ℙasc k and i ∈ 𝕄 and i < k ⟹ f ap (i) ∈ ℙ and f ap (i) ∈ 𝕄` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 prf LPH / ℙasc. -| Lℙ p; LPH -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 h; !let/thm Π∈𝕄 <- `k ∈ 𝕄 and f ℙasc k ⟹ f prod k ∈ 𝕄` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , prod𝕄 prf Pb <- `f prod 0 ∈ 𝕄` -| prod𝕄 , 1. , 𝕄0s p; Ps <- `k ∈ 𝕄 and (f ℙasc k ⟹ f prod k ∈ 𝕄) and f ℙasc (k suc) ⟹ f prod (k suc) ∈ 𝕄` -| prod𝕄 , Lres , LPH , L<s , ⋅∈𝕄 v; Π∈𝕄 -| IND𝕄[C_:=`\{ cls k | f ℙasc k ⟹ f prod k ∈ 𝕄 \}`] , Pb , Ps , 𝕄0s v; Π∈𝕄 -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , prod𝕄 h; let/thm EuclidΠ <- `p ∈ ℙ and k ∈ 𝕄 and f ℙasc k and p ∣ f prod k ⟹ [ ∃ j ∈ 𝕄 . j < k and p ∣ f ap (j) ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , prod𝕄 prf Eb <- `p ∈ ℙ ⟹ ¬ (p ∣ f prod 0)` -| prod𝕄 , ℙ∤1 p; Es <- `p ∈ ℙ and k ∈ 𝕄 and (f ℙasc k and p ∣ f prod k ⟹ [ ∃ j ∈ 𝕄 . j < k and p ∣ f ap (j) ]) and f ℙasc (k suc) and p ∣ f prod (k suc) ⟹ [ ∃ j ∈ 𝕄 . j < k suc and p ∣ f ap (j) ]` -| prod𝕄 , Euclid , Π∈𝕄 , Lres , LPH , L<K , L<s , Lℙ v; EuclidΠ -| IND𝕄[C_:=`\{ cls k | f ℙasc k and p ∣ f prod k ⟹ [ ∃ j ∈ 𝕄 . j < k and p ∣ f ap (j) ] \}`] , Eb , Es , 𝕄0s v; EuclidΠ -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , prod𝕄 h; let/thm Mono <- `l ∈ 𝕄 and f ℙasc l and [ m ; j col ∈ 𝕄 ] and m + j < l ⟹ f ap (j) ≤ f ap (m + j)` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 prf L+< <- `[ m ; j ; l col ∈ 𝕄 ] and m + j < l ⟹ j < l` / <. / ≤. -| +A , +𝕄 , +∈𝕄 p; Mb <- `l ∈ 𝕄 and f ℙasc l ⟹ [ ∀ j ∈ 𝕄 . (0 + j < l ⟹ f ap (j) ≤ f ap (0 + j)) ]` -| L0+ , L≤R , LPH p; Ms1 <- `l ∈ 𝕄 and f ℙasc l and [ m ; j col ∈ 𝕄 ] and f ap (j) ≤ f ap (m + j) and (m + j) suc < l ⟹ f ap (j) ≤ f ap ((m + j) suc)` / ℙasc. -| L<W , L+< , L≤T , Lℙ , +∈𝕄 , 𝕄0s v; Ms <- `l ∈ 𝕄 and f ℙasc l and m ∈ 𝕄 and [ ∀ j ∈ 𝕄 . (m + j < l ⟹ f ap (j) ≤ f ap (m + j)) ] ⟹ [ ∀ j ∈ 𝕄 . (m suc + j < l ⟹ f ap (j) ≤ f ap (m suc + j)) ]` -| Ms1 , Lsuc+ , L<W , +∈𝕄 , 𝕄0s v; Mono -| IND𝕄[C_:=`\{ cls m | [ ∀ j ∈ 𝕄 . (m + j < l ⟹ f ap (j) ≤ f ap (m + j)) ] \}`] , Mb , Ms , 𝕄0s v; Mono -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 h; let/thm Lmin <- `n ∈ 𝕄 and 2 ≤ n ⟹ [ ∃ p ∈ 𝕄 . 2 ≤ p and p ∣ n and [ ∀ e ∈ 𝕄 . (2 ≤ e and e ∣ n ⟹ p ≤ e) ] ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 prf hN <- `|n ∈ 𝕄` ; h2 <- `2 ≤ |n` ; hNo <- `¬ [ ∃ p ∈ 𝕄 . 2 ≤ p and p ∣ |n and [ ∀ e ∈ 𝕄 . (2 ≤ e and e ∣ |n ⟹ p ≤ e) ] ]` ; Nst <- `x ∈ 𝕄 and [ ∀ z ∈ 𝕄 . (z < x ⟹ ¬ (2 ≤ z and z ∣ |n)) ] ⟹ ¬ (2 ≤ x and x ∣ |n)` -| Ltot , hNo v; NI <- `¬ (2 ≤ |n and |n ∣ |n)` -| SIND𝕄[D_:=`\{ cls x | ¬ (2 ≤ x and x ∣ |n) \}`] , Nst , hN v; Nf <- `⊥` -| NI , h2 , ∣R , hN p; Ngen <- `n ∈ 𝕄 and 2 ≤ n and ¬ [ ∃ p ∈ 𝕄 . 2 ≤ p and p ∣ n and [ ∀ e ∈ 𝕄 . (2 ≤ e and e ∣ n ⟹ p ≤ e) ] ] ⟹ ⊥` -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 h[fix]; Lmin -| Ngen p; Lmin -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 h; let/thm Lmp <- `n ∈ 𝕄 and n {/}= 0 and p ∈ 𝕄 and 2 ≤ p and p ∣ n and [ ∀ e ∈ 𝕄 . (2 ≤ e and e ∣ n ⟹ p ≤ e) ] ⟹ p ∈ ℙ` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 prf L0∣ <- `p ∈ 𝕄 and 0 ∣ p ⟹ p = 0` / ∣. -| ⋅C , *𝕄 , 𝕄0s p; Mp1 <- `[ n ; p ; d col ∈ 𝕄 ] and n {/}= 0 and 2 ≤ p and p ∣ n and [ ∀ e ∈ 𝕄 . (2 ≤ e and e ∣ n ⟹ p ≤ e) ] and d ∣ p ⟹ d = 1 or d = p` -| L0∣ , L≠0 , L2≤ , ∣T , ∣≤ , L≤A v; Lmp -| ℙ.' , Mp1 p; Lmp -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 h; section 主定理 subsection 一意性 txt 昇順の素数の列 \(f\)（長さ \(k\)）・\(g\)（長さ \(l\)）の積が等しければ、長さも項も等しい。 txt 最後の項 \(a = f(k-1)\)・\(b = g(l-1)\) はそれぞれ最大の項で、\(a\) は \(g\) のどれかの項に等しいので \(a \le b\)、同様に \(b \le a\)。積から \(a\) を消して（消去律 ⋅K）長さについての帰納法。 let/thm Uniq <- `[ k ; l col ∈ 𝕄 ] and f ℙasc k and g ℙasc l and f prod k = g prod l ⟹ k = l and [ ∀ i ∈ 𝕄 . (i < k ⟹ f ap (i) = g ap (i)) ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , prod𝕄 prf L∣ℙ <- `p ∈ ℙ and q ∈ ℙ and p ∣ q ⟹ p = q` -| ℙ.' , Lℙ p; L≠1 <- `[ x ; b col ∈ 𝕄 ] and b ∈ ℙ ⟹ x ⋅ b {/}= 1` -| ℙ∤1 , ∣⋅R , Lℙ p; MonoL <- `l ∈ 𝕄 and f ℙasc (l suc) and j ∈ 𝕄 and j < l suc ⟹ f ap (j) ≤ f ap (l)` -| L<S , L<≤ / ≤. , Mono , L<s , L≤R , LPH , 𝕄0s v; hK <- `|K ∈ 𝕄` ; hL <- `|L ∈ 𝕄` ; hI <- `[ ∀ l ∈ 𝕄 . (|f ℙasc |K and |g ℙasc l and |f prod |K = |g prod l ⟹ |K = l and [ ∀ i ∈ 𝕄 . (i < |K ⟹ |f ap (i) = |g ap (i)) ]) ]` ; hPf <- `|f ℙasc (|K suc)` ; hPg <- `|g ℙasc (|L suc)` ; hE <- `|f prod (|K suc) = |g prod (|L suc)` ; Rf <- `|f ℙasc |K` -| Lres , hK , hPf p; Rg <- `|g ℙasc |L` -| Lres , hL , hPg p; Ta <- `|f ap (|K) ∈ ℙ and |g ap (|L) ∈ ℙ and |f prod |K ∈ 𝕄 and |g prod |L ∈ 𝕄` -| LPH , hPf , hPg , L<s , hK , hL , Π∈𝕄 , Rf , Rg p; Te <- `|f prod |K ⋅ |f ap (|K) = |g prod |L ⋅ |g ap (|L)` -| hE , prod𝕄 , hK , hL p; Tab1 <- `|f ap (|K) ∣ |g prod (|L suc)` / ∣. -| hE , prod𝕄 , hK , hL , ⋅C , Ta , Lℙ v; Tab2 <- `[ ∃ j ∈ 𝕄 . j < |L suc and |f ap (|K) ∣ |g ap (j) ]` -| EuclidΠ , Tab1 , Ta , hPg , hL , 𝕄0s p; Tab3 <- `j ∈ 𝕄 and j < |L suc and |f ap (|K) ∣ |g ap (j) ⟹ |f ap (|K) ≤ |g ap (|L)` -| L∣ℙ , LPH , hPg , Ta , MonoL , hL p; Tab <- `|f ap (|K) ≤ |g ap (|L)` -| Tab2 , Tab3 p; Tba1 <- `|g ap (|L) ∣ |f prod (|K suc)` / ∣. -| hE , prod𝕄 , hK , hL , ⋅C , Ta , Lℙ v; Tba2 <- `[ ∃ j ∈ 𝕄 . j < |K suc and |g ap (|L) ∣ |f ap (j) ]` -| EuclidΠ , Tba1 , Ta , hPf , hK , 𝕄0s p; Tba3 <- `j ∈ 𝕄 and j < |K suc and |g ap (|L) ∣ |f ap (j) ⟹ |g ap (|L) ≤ |f ap (|K)` -| L∣ℙ , LPH , hPf , Ta , MonoL , hK p; Tba <- `|g ap (|L) ≤ |f ap (|K)` -| Tba2 , Tba3 p; T= <- `|f ap (|K) = |g ap (|L) and |f prod |K = |g prod |L` -| Tab , Tba , L≤A , Ta , Lℙ , Te , ⋅K p; TI <- `|K = |L and [ ∀ i ∈ 𝕄 . (i < |K ⟹ |f ap (i) = |g ap (i)) ]` -| hI , hL , Rf , Rg , T= p; TS <- `|K suc = |L suc and [ ∀ i ∈ 𝕄 . (i < |K suc ⟹ |f ap (i) = |g ap (i)) ]` -| TI , T= , L<S , hK p; Lgen <- `K ∈ 𝕄 and L ∈ 𝕄 and [ ∀ l ∈ 𝕄 . (f ℙasc K and g ℙasc l and f prod K = g prod l ⟹ K = l and [ ∀ i ∈ 𝕄 . (i < K ⟹ f ap (i) = g ap (i)) ]) ] and f ℙasc (K suc) and g ℙasc (L suc) and f prod (K suc) = g prod (L suc) ⟹ K suc = L suc and [ ∀ i ∈ 𝕄 . (i < K suc ⟹ f ap (i) = g ap (i)) ]` -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , prod𝕄 h[fix]; Ub <- `[ ∀ l ∈ 𝕄 . (f ℙasc 0 and g ℙasc l and f prod 0 = g prod l ⟹ 0 = l and [ ∀ i ∈ 𝕄 . (i < 0 ⟹ f ap (i) = g ap (i)) ]) ]` -| Lpred , prod𝕄 , L≠1 , Π∈𝕄 , Lres , LPH , L<s , L<0 v; Us <- `K ∈ 𝕄 and [ ∀ l ∈ 𝕄 . (f ℙasc K and g ℙasc l and f prod K = g prod l ⟹ K = l and [ ∀ i ∈ 𝕄 . (i < K ⟹ f ap (i) = g ap (i)) ]) ] ⟹ [ ∀ l ∈ 𝕄 . (f ℙasc (K suc) and g ℙasc l and f prod (K suc) = g prod l ⟹ K suc = l and [ ∀ i ∈ 𝕄 . (i < K suc ⟹ f ap (i) = g ap (i)) ]) ]` -| Lgen , Lpred , prod𝕄 , L≠1 , Π∈𝕄 , Lres , LPH , L<s v; Uniq -| IND𝕄[C_:=`\{ cls k | [ ∀ l ∈ 𝕄 . (f ℙasc k and g ℙasc l and f prod k = g prod l ⟹ k = l and [ ∀ i ∈ 𝕄 . (i < k ⟹ f ap (i) = g ap (i)) ]) ] \}`] , Ub , Us , 𝕄0s v; Uniq -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , prod𝕄 h; subsection 存在 txt \(n \ge 2\) の最小の約数 \(p \ge 2\) は素数で、\(n = p m\)。\(m\) の素因数はどれも \(n\) を割るので \(p\) 以上。\(m\) の列の頭に \(p\) を足す。\(n\) についての強い帰納法。 let/thm Exist <- `n ∈ 𝕄 and 2 ≤ n ⟹ [ ∃ k ∈ 𝕄 . [ ∃ f \, (f ℙasc k and n = f prod k) ] ]` ◀ W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , prod𝕄 , seq𝕄 prf Db <- `[ ∀ j ∈ 𝕄 . (j < 0 ⟹ f ap (j) ∣ f prod 0) ]` -| L<0 p; Ds <- `k ∈ 𝕄 and (f ℙasc k ⟹ [ ∀ j ∈ 𝕄 . (j < k ⟹ f ap (j) ∣ f prod k) ]) and f ℙasc (k suc) ⟹ [ ∀ j ∈ 𝕄 . (j < k suc ⟹ f ap (j) ∣ f prod (k suc)) ]` -| prod𝕄 , Lres , LPH , L<s , L<S , Π∈𝕄 , ∣M , ∣⋅R v; ∣Π <- `k ∈ 𝕄 and f ℙasc k and j ∈ 𝕄 and j < k ⟹ f ap (j) ∣ f prod k` -| IND𝕄[C_:=`\{ cls k | f ℙasc k ⟹ [ ∀ j ∈ 𝕄 . (j < k ⟹ f ap (j) ∣ f prod k) ] \}`] , Db , Ds , 𝕄0s v; Lasc <- `f ℙasc k and i ∈ 𝕄 and i suc < k ⟹ f ap (i) ≤ f ap (i suc)` / ℙasc. -| 𝕄0s p; Lmk <- `[ ∀ i ∈ 𝕄 . (i < k ⟹ f ap (i) ∈ ℙ) ] and [ ∀ i ∈ 𝕄 . (i suc < k ⟹ f ap (i) ≤ f ap (i suc)) ] ⟹ f ℙasc k` / ℙasc. -| 𝕄0s p; Qb <- `g ap (0) = p and p ∈ 𝕄 ⟹ g prod (0 suc) = p ⋅ (f prod 0)` -| prod𝕄 , L⋅1 , ⋅C , 1. , 𝕄0s p; Qs <- `g ap (0) = p and [ ∀ i ∈ 𝕄 . g ap (i suc) = f ap (i) ] and p ∈ 𝕄 and k ∈ 𝕄 and (f ℙasc k ⟹ g prod (k suc) = p ⋅ (f prod k)) and f ℙasc (k suc) ⟹ g prod (k suc suc) = p ⋅ (f prod (k suc))` -| prod𝕄 , ⋅A , Lres , LPH , L<s , Π∈𝕄 , 𝕄0s v; Pre <- `g ap (0) = p and [ ∀ i ∈ 𝕄 . g ap (i suc) = f ap (i) ] and p ∈ 𝕄 and k ∈ 𝕄 and f ℙasc k ⟹ g prod (k suc) = p ⋅ (f prod k)` -| IND𝕄[C_:=`\{ cls k | f ℙasc k ⟹ g prod (k suc) = p ⋅ (f prod k) \}`] , Qb , Qs , 𝕄0s v; C1 <- `k ∈ 𝕄 and p ∈ ℙ and f ℙasc k and g ap (0) = p and [ ∀ i ∈ 𝕄 . g ap (i suc) = f ap (i) ] ⟹ [ ∀ i ∈ 𝕄 . (i < k suc ⟹ g ap (i) ∈ ℙ) ]` / ℙasc. -| Lpred , Lss , 𝕄0s v; C2a <- `[ n ; m ; k col ∈ 𝕄 ] and p ∈ ℙ and [ ∀ e ∈ 𝕄 . (2 ≤ e and e ∣ n ⟹ p ≤ e) ] and n = p ⋅ m and f ℙasc k and m = f prod k and 0 < k ⟹ p ≤ f ap (0)` -| ∣Π , LPH , ∣T , ∣. , ⋅C , Lℙ , 𝕄0s v; C2 <- `[ n ; m ; k col ∈ 𝕄 ] and p ∈ ℙ and [ ∀ e ∈ 𝕄 . (2 ≤ e and e ∣ n ⟹ p ≤ e) ] and n = p ⋅ m and f ℙasc k and m = f prod k and g ap (0) = p and [ ∀ i ∈ 𝕄 . g ap (i suc) = f ap (i) ] ⟹ [ ∀ i ∈ 𝕄 . (i suc < k suc ⟹ g ap (i) ≤ g ap (i suc)) ]` -| C2a , Lasc , Lpred , Lss , 𝕄0s v; C3 <- `[ n ; m ; k col ∈ 𝕄 ] and p ∈ ℙ and [ ∀ e ∈ 𝕄 . (2 ≤ e and e ∣ n ⟹ p ≤ e) ] and n = p ⋅ m and f ℙasc k and m = f prod k and g ap (0) = p and [ ∀ i ∈ 𝕄 . g ap (i suc) = f ap (i) ] ⟹ g ℙasc (k suc)` -| C1 , C2 , Lmk v; C4 <- `[ n ; m ; k col ∈ 𝕄 ] and p ∈ ℙ and [ ∀ e ∈ 𝕄 . (2 ≤ e and e ∣ n ⟹ p ≤ e) ] and n = p ⋅ m and f ℙasc k and m = f prod k and g ap (0) = p and [ ∀ i ∈ 𝕄 . g ap (i suc) = f ap (i) ] ⟹ [ ∃ k ∈ 𝕄 . [ ∃ f \, (f ℙasc k and n = f prod k) ] ]` -| C3 , Pre , Lℙ , 𝕄0s v; X1 <- `[ ∃ k ∈ 𝕄 . [ ∃ f \, (f ℙasc k and 1 = f prod k) ] ]` / ℙasc. -| prod𝕄 , L<0 , 𝕄0s v; hN <- `|n ∈ 𝕄` ; hI <- `[ ∀ z ∈ 𝕄 . (z < |n ⟹ (z {/}= 0 ⟹ [ ∃ k ∈ 𝕄 . [ ∃ f \, (f ℙasc k and z = f prod k) ] ])) ]` ; h2 <- `2 ≤ |n` ; hp <- `|p ∈ ℙ` ; hmin <- `[ ∀ e ∈ 𝕄 . (2 ≤ e and e ∣ |n ⟹ |p ≤ e) ]` ; hM <- `|m ∈ 𝕄` ; hD <- `|n = |p ⋅ |m` ; Y1 <- `|m {/}= 0 and |m < |n` -| hD , *𝕄 , L≠0 , h2 , hN , Llt , hp , Lℙ , hM p; Y2 <- `[ ∃ k ∈ 𝕄 . [ ∃ f \, (f ℙasc k and |m = f prod k) ] ]` -| hI , Y1 , hM p; Y3 <- `[ ∃ k ∈ 𝕄 . [ ∃ f \, (f ℙasc k and |n = f prod k) ] ]` -| Y2 , seq𝕄 , C4 , hp , hmin , hD , hN , hM v; Ygen <- `[ n ; m col ∈ 𝕄 ] and [ ∀ z ∈ 𝕄 . (z < n ⟹ (z {/}= 0 ⟹ [ ∃ k ∈ 𝕄 . [ ∃ f \, (f ℙasc k and z = f prod k) ] ])) ] and 2 ≤ n and p ∈ ℙ and [ ∀ e ∈ 𝕄 . (2 ≤ e and e ∣ n ⟹ p ≤ e) ] and n = p ⋅ m ⟹ [ ∃ k ∈ 𝕄 . [ ∃ f \, (f ℙasc k and n = f prod k) ] ]` -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , prod𝕄 , seq𝕄 h[fix]; Xs <- `n ∈ 𝕄 and [ ∀ z ∈ 𝕄 . (z < n ⟹ (z {/}= 0 ⟹ [ ∃ k ∈ 𝕄 . [ ∃ f \, (f ℙasc k and z = f prod k) ] ])) ] and 2 ≤ n ⟹ [ ∃ k ∈ 𝕄 . [ ∃ f \, (f ℙasc k and n = f prod k) ] ]` -| Lmin , Lmp , ∣. , Ygen , L≠0 v; Qn <- `n ∈ 𝕄 and [ ∀ z ∈ 𝕄 . (z < n ⟹ (z {/}= 0 ⟹ [ ∃ k ∈ 𝕄 . [ ∃ f \, (f ℙasc k and z = f prod k) ] ])) ] ⟹ (n {/}= 0 ⟹ [ ∃ k ∈ 𝕄 . [ ∃ f \, (f ℙasc k and n = f prod k) ] ])` -| X1 , Xs , L2≤ v; Exist -| SIND𝕄[D_:=`\{ cls x | x {/}= 0 ⟹ [ ∃ k ∈ 𝕄 . [ ∃ f \, (f ℙasc k and x = f prod k) ] ] \}`] , Qn , L≠0 v; Exist -| W. , 𝕄0s , IND𝕄 , suc𝕄 , +𝕄 , *𝕄 , 1. , prod𝕄 , seq𝕄 h;
表示（保存しません）
保存にはMatheliaへのログインが要ります。