book集

section 自然数の演算
subsection 準備
txt 2.book の隠し補題のうち、この Book で使うものを写しました（隠し補題は import で引き継がれないため）。
!let/thm Lfval <- `f ∈ X → Y and \< pr x ; y \> ∈ f ⟹ y ∈ Y` ◀ W.
prf Lfval / →.' -| pr:0 p; Lfval -| W. h;
!let/thm Lftot <- `f ∈ X → Y and x ∈ X ⟹ [ ∃ y \, \< pr x ; y \> ∈ f ]` ◀ W.
prf Lftot / →.' -| O p; Lftot -| W. h;
!let/thm Lfuniq <- `f ∈ X → Y and x ∈ X and \< pr x ; y0 \> ∈ f and \< pr x ; y1 \> ∈ f ⟹ y0 = y1` ◀ W.
prf Lfuniq / →.' -| O p; Lfuniq -| W. h;
!let/thm Lfdom <- `f ∈ X → Y and \< pr x ; y \> ∈ f ⟹ x ∈ X` ◀ W.
prf Lfdom / →.' -| pr:0 p; Lfdom -| W. h;
!let/thm Lirr <- `n ∈ 𝕄 ⟹ n {/}∈ n` ◀ W. , ax_s
prf Lirr -| <𝕄:l / ⊊.. p; Lirr -| W. , ax_s h;
!let/thm LinM <- `n ∈ 𝕄 and x ∈ n ⟹ x ∈ 𝕄` ◀ W. , ax_s
prf LinM -| <𝕄:i , ⊂. p; LinM -| W. , ax_s h;
!let/thm INDS <- `0 ∈ B and [ ∀ m ∈ 𝕄 . (m ∈ B ⟹ m suc ∈ B) ] and n ∈ 𝕄 ⟹ n ∈ B` ◀ W.
prf L0 <- `0 ∈ 𝕄` / 𝕄. -| O p;
    LI <- `0 ∈ B and [ ∀ m ∈ 𝕄 . (m ∈ B ⟹ m suc ∈ B) ] ⟹ 𝕄 ∩ B ∈_ Ind` / ⊂. / ^suc. / ∩. -| L0 , 𝕄1 p;
    LM <- `0 ∈ B and [ ∀ m ∈ 𝕄 . (m ∈ B ⟹ m suc ∈ B) ] ⟹ 𝕄 ⊂ 𝕄 ∩ B` -| LI , 𝕄. , ⊂. v;
    INDS -| LM , ⊂. , ∩. p;
    INDS -| W. h;
!let/thm Lsucin <- `n ∈ n suc` ◀ W.
prf Lsucin -| suc.' p; Lsucin -| W. h;
!let/thm Ltrans <- `[ chain x ∈ a ∈ b ∈ 𝕄 ] ⟹ x ∈ b` ◀ W. , ax_s
prf Ltrans -| <𝕄:l , ⊊.. , ⊂. p; Ltrans -| W. , ax_s h;
subsection 加法
txt 2.book では加法と乗法を定義せず、再帰の等式 +𝕄・*𝕄 を仮定として使います。この Book はその別案として、途中経過の列 \(h\) を使って \(+\)・\(\cdot\) を定義し、+𝕄・*𝕄 を定理として示したものです（2026-09-29 作成・2.book から移動）。
txt \(m + n\) は \(m\) から始めて \({\rm suc}\) を \(n\) 回施したものです。途中経過の列 \(h\)（\(h\) は \(k+1\) 上の写像で \(h(0)=m\)、\(h(i+1)=h(i)+1\)）を使って定義します。
prop +. <- `[ ∃！ w [ ∃ k ; h \, \\{ And k ∈ 𝕄 \\ h ∈ k suc → 𝕄 \\ \< pr 0 ; m \> ∈ h \\ [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u suc \> ∈ h) ] ] \\ \< pr n ; w \> ∈ h \\} ] ] ⟹ ( m + n = y ⇔ [ ∃ k ; h \, \\{ And k ∈ 𝕄 \\ h ∈ k suc → 𝕄 \\ \< pr 0 ; m \> ∈ h \\ [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u suc \> ∈ h) ] ] \\ \< pr n ; y \> ∈ h \\} ] )`
!let/thm L→suc <- `h ∈ D → Y and D {/}∈ D and c ∈ Y ⟹ h ∪ \{ set \< pr D ; c \> \} ∈ D suc → Y` ◀ W.
prf L→suc / →.' / ∪. / set1. -| suc.' , pr:0 p; L→suc -| W. h;
!let/thm Lsucinv <- `k ∈ 𝕄 and n suc ∈ k suc ⟹ n ∈ k` ◀ W. , ax_s
prf Lsucinv -| Ltrans , Lsucin , suc.' p; Lsucinv -| W. , ax_s h;
!let/thm LA0 <- `m ∈ 𝕄 ⟹ 0 ∈ 𝕄 and (\{ set \< pr 0 ; m \> \}) ∈ 0 suc → 𝕄 and \< pr 0 ; m \> ∈ (\{ set \< pr 0 ; m \> \}) and [ ∀ i ∈ 0 . [ ∀ u (\< pr i ; u \> ∈ (\{ set \< pr 0 ; m \> \}) ⟹ \< pr i suc ; u suc \> ∈ (\{ set \< pr 0 ; m \> \})) ] ]` ◀ W.
prf LA0 / →.' / set1. -| suc.' , 0.' , pr:0 , 𝕄. p; LA0 -| W. h;
!let/thm LAS <- `k ∈ 𝕄 and h ∈ k suc → 𝕄 and \< pr 0 ; m \> ∈ h and [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u suc \> ∈ h) ] ] and \< pr k ; z \> ∈ h ⟹ k suc ∈ 𝕄 and h ∪ \{ set \< pr k suc ; z suc \> \} ∈ k suc suc → 𝕄 and \< pr 0 ; m \> ∈ h ∪ \{ set \< pr k suc ; z suc \> \} and [ ∀ i ∈ k suc . [ ∀ u (\< pr i ; u \> ∈ h ∪ \{ set \< pr k suc ; z suc \> \} ⟹ \< pr i suc ; u suc \> ∈ h ∪ \{ set \< pr k suc ; z suc \> \}) ] ]` ◀ W. , ax_s
prf hyK <- `|k ∈ 𝕄` ;
    hyH <- `|h ∈ |k suc → 𝕄` ;
    hyS <- `[ ∀ i ∈ |k . [ ∀ u (\< pr i ; u \> ∈ |h ⟹ \< pr i suc ; u suc \> ∈ |h) ] ]` ;
    hyZ <- `\< pr |k ; |z \> ∈ |h` ;
    Lz <- `|z suc ∈ 𝕄` -| hyH , hyZ , Lfval , 𝕄1 p;
    Lmap <- `|h ∪ \{ set \< pr |k suc ; |z suc \> \} ∈ |k suc suc → 𝕄` -| hyK , hyH , L→suc , Lirr , 𝕄1 , Lz p;
    Lold <- `i ∈ |k suc and \< pr i ; u \> ∈ |h ∪ \{ set \< pr |k suc ; |z suc \> \} ⟹ \< pr i ; u \> ∈ |h` / ∪. / set1. -| hyK , pr:0 , Lirr , 𝕄1 p;
    Lstep <- `i ∈ |k suc and \< pr i ; u \> ∈ |h ⟹ \< pr i suc ; u suc \> ∈ |h ∪ \{ set \< pr |k suc ; |z suc \> \}` / ∪. / set1. -| hyH , hyS , hyZ , suc.' , Lfuniq , Lsucin , pr:0 p;
    Lfin <- `|k suc ∈ 𝕄 and |h ∪ \{ set \< pr |k suc ; |z suc \> \} ∈ |k suc suc → 𝕄 and \< pr 0 ; |m \> ∈ |h ∪ \{ set \< pr |k suc ; |z suc \> \} and [ ∀ i ∈ |k suc . [ ∀ u (\< pr i ; u \> ∈ |h ∪ \{ set \< pr |k suc ; |z suc \> \} ⟹ \< pr i suc ; u suc \> ∈ |h ∪ \{ set \< pr |k suc ; |z suc \> \}) ] ]` -| hyK , `\< pr 0 ; |m \> ∈ |h` , Lmap , Lold , Lstep , 𝕄1 , ∪. p;
    LAS -| W. , ax_s h[fix];
!let/thm LAE <- `m ∈ 𝕄 and k ∈ 𝕄 ⟹ [ ∃ h \, k ∈ 𝕄 and h ∈ k suc → 𝕄 and \< pr 0 ; m \> ∈ h and [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u suc \> ∈ h) ] ] ]` ◀ W. , ax_s
prf LAE -| INDC[D_:=`\{ cls k | [ ∃ h \, k ∈ 𝕄 and h ∈ k suc → 𝕄 and \< pr 0 ; m \> ∈ h and [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u suc \> ∈ h) ] ] ] \}`] , LA0 , LAS , Lftot , Lsucin v;
    LAE -| W. , ax_s h;
!let/thm LAP <- `k ∈ 𝕄 and h ∈ k suc → 𝕄 and \< pr 0 ; m \> ∈ h and [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u suc \> ∈ h) ] ] and \< pr n suc ; y \> ∈ h ⟹ [ ∃ z \, \< pr n ; z \> ∈ h and y = z suc ]` ◀ W. , ax_s
prf LAP -| Lfdom , Lsucinv , suc.' , Lftot , Lfuniq p; LAP -| W. , ax_s h;
!let/thm LAU <- `k1 ∈ 𝕄 and h1 ∈ k1 suc → 𝕄 and \< pr 0 ; m \> ∈ h1 and [ ∀ i ∈ k1 . [ ∀ u (\< pr i ; u \> ∈ h1 ⟹ \< pr i suc ; u suc \> ∈ h1) ] ] and k2 ∈ 𝕄 and h2 ∈ k2 suc → 𝕄 and \< pr 0 ; m \> ∈ h2 and [ ∀ i ∈ k2 . [ ∀ u (\< pr i ; u \> ∈ h2 ⟹ \< pr i suc ; u suc \> ∈ h2) ] ] and n ∈ 𝕄 and \< pr n ; y1 \> ∈ h1 and \< pr n ; y2 \> ∈ h2 ⟹ y1 = y2` ◀ W. , ax_s
prf hyH1 <- `|h1 ∈ |k1 suc → 𝕄` ;
    hy01 <- `\< pr 0 ; |m \> ∈ |h1` ;
    hyS1 <- `[ ∀ i ∈ |k1 . [ ∀ u (\< pr i ; u \> ∈ |h1 ⟹ \< pr i suc ; u suc \> ∈ |h1) ] ]` ;
    hyH2 <- `|h2 ∈ |k2 suc → 𝕄` ;
    hy02 <- `\< pr 0 ; |m \> ∈ |h2` ;
    hyS2 <- `[ ∀ i ∈ |k2 . [ ∀ u (\< pr i ; u \> ∈ |h2 ⟹ \< pr i suc ; u suc \> ∈ |h2) ] ]` ;
    LU0 <- `\< pr 0 ; y1 \> ∈ |h1 and \< pr 0 ; y2 \> ∈ |h2 ⟹ y1 = y2` -| hyH1 , hyH2 , hy01 , hy02 , Lfuniq , Lfdom p;
    LUs <- `[ ∀ y1 ; y2 (\< pr n ; y1 \> ∈ |h1 and \< pr n ; y2 \> ∈ |h2 ⟹ y1 = y2) ] and \< pr n suc ; y1 \> ∈ |h1 and \< pr n suc ; y2 \> ∈ |h2 ⟹ y1 = y2` -| `|k1 ∈ 𝕄` , hyH1 , hy01 , hyS1 , `|k2 ∈ 𝕄` , hyH2 , hy02 , hyS2 , LAP v;
    Lfin <- `|y1 = |y2` -| INDC[D_:=`\{ cls n | [ ∀ y1 ; y2 (\< pr n ; y1 \> ∈ |h1 and \< pr n ; y2 \> ∈ |h2 ⟹ y1 = y2) ] \}`] , LU0 , LUs , `|n ∈ 𝕄` , `\< pr |n ; |y1 \> ∈ |h1` , `\< pr |n ; |y2 \> ∈ |h2` v;
    LAU -| W. , ax_s h[fix];
!let/thm L+! <- `m ∈ 𝕄 and n ∈ 𝕄 ⟹ [ ∃！ w [ ∃ k ; h \, k ∈ 𝕄 and h ∈ k suc → 𝕄 and \< pr 0 ; m \> ∈ h and [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u suc \> ∈ h) ] ] and \< pr n ; w \> ∈ h ] ]` ◀ W. , ax_s
prf L+! -| LAE , Lsucin , Lftot , LAU v; L+! -| W. , ax_s h;
!let/thm Lval <- `k ∈ 𝕄 and h ∈ k suc → 𝕄 and \< pr 0 ; m \> ∈ h and [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u suc \> ∈ h) ] ] and \< pr n ; y \> ∈ h ⟹ m + n = y` ◀ W. , ax_s
prf Lm <- `k ∈ 𝕄 and h ∈ k suc → 𝕄 and \< pr 0 ; m \> ∈ h and [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u suc \> ∈ h) ] ] and \< pr n ; y \> ∈ h ⟹ m ∈ 𝕄 and n ∈ 𝕄` -| Lfval , Lfdom , 𝕄1 , LinM p;
    Ldef <- `m ∈ 𝕄 and n ∈ 𝕄 ⟹ ( m + n = y ⇔ [ ∃ k ; h \, k ∈ 𝕄 and h ∈ k suc → 𝕄 and \< pr 0 ; m \> ∈ h and [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u suc \> ∈ h) ] ] and \< pr n ; y \> ∈ h ] )` -| +. , L+! v;
    Lval -| Ldef , Lm v;
    Lval -| W. , ax_s h;
prop/thm +𝕄 ◀ W. , ax_s
prf LS0 <- `|m + |n suc = (|m + |n) suc` -| LAE , Lval , Lftot , Lsucin , suc.' , 𝕄1 , `|m ∈ 𝕄` , `|n ∈ 𝕄` v;
    L+S <- `m ∈ 𝕄 and n ∈ 𝕄 ⟹ m + n suc = (m + n) suc` -| W. , ax_s h[fix];
    +𝕄 -| LA0 , Lval , L+S p;
    +𝕄 -| W. , ax_s h;
let/thm +∈𝕄 <- `[ m ; n col ∈ 𝕄 ] ⟹ m + n ∈ 𝕄` ◀ W. , ax_s
prf +∈𝕄 -| LAE , Lsucin , Lftot , Lval , Lfval v; +∈𝕄 -| W. , ax_s h;

subsection 乗法
txt \(m \cdot n\) は \(0\) から始めて \(m\) を \(n\) 回足したものです。加法と同じく途中経過の列 \(h\)（\(h(0)=0\)、\(h(i+1)=h(i)+m\)）で定義します。
prop ⋅. <- `[ ∃！ w [ ∃ k ; h \, \\{ And k ∈ 𝕄 \\ h ∈ k suc → 𝕄 \\ \< pr 0 ; 0 \> ∈ h \\ [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u + m \> ∈ h) ] ] \\ \< pr n ; w \> ∈ h \\} ] ] ⟹ ( m ⋅ n = y ⇔ [ ∃ k ; h \, \\{ And k ∈ 𝕄 \\ h ∈ k suc → 𝕄 \\ \< pr 0 ; 0 \> ∈ h \\ [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u + m \> ∈ h) ] ] \\ \< pr n ; y \> ∈ h \\} ] )`
!let/thm LM0 <- `m ∈ 𝕄 ⟹ 0 ∈ 𝕄 and (\{ set \< pr 0 ; 0 \> \}) ∈ 0 suc → 𝕄 and \< pr 0 ; 0 \> ∈ (\{ set \< pr 0 ; 0 \> \}) and [ ∀ i ∈ 0 . [ ∀ u (\< pr i ; u \> ∈ (\{ set \< pr 0 ; 0 \> \}) ⟹ \< pr i suc ; u + m \> ∈ (\{ set \< pr 0 ; 0 \> \})) ] ]` ◀ W.
prf LM0 / →.' / set1. -| suc.' , 0.' , pr:0 , 𝕄. p; LM0 -| W. h;
!let/thm LMS <- `m ∈ 𝕄 and k ∈ 𝕄 and h ∈ k suc → 𝕄 and \< pr 0 ; 0 \> ∈ h and [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u + m \> ∈ h) ] ] and \< pr k ; z \> ∈ h ⟹ k suc ∈ 𝕄 and h ∪ \{ set \< pr k suc ; z + m \> \} ∈ k suc suc → 𝕄 and \< pr 0 ; 0 \> ∈ h ∪ \{ set \< pr k suc ; z + m \> \} and [ ∀ i ∈ k suc . [ ∀ u (\< pr i ; u \> ∈ h ∪ \{ set \< pr k suc ; z + m \> \} ⟹ \< pr i suc ; u + m \> ∈ h ∪ \{ set \< pr k suc ; z + m \> \}) ] ]` ◀ W. , ax_s
prf hyK <- `|k ∈ 𝕄` ;
    hyH <- `|h ∈ |k suc → 𝕄` ;
    hyS <- `[ ∀ i ∈ |k . [ ∀ u (\< pr i ; u \> ∈ |h ⟹ \< pr i suc ; u + |m \> ∈ |h) ] ]` ;
    hyZ <- `\< pr |k ; |z \> ∈ |h` ;
    Lz <- `|z + |m ∈ 𝕄` -| hyH , hyZ , Lfval , `|m ∈ 𝕄` , +∈𝕄 p;
    Lmap <- `|h ∪ \{ set \< pr |k suc ; |z + |m \> \} ∈ |k suc suc → 𝕄` -| hyK , hyH , L→suc , Lirr , 𝕄1 , Lz p;
    Lold <- `i ∈ |k suc and \< pr i ; u \> ∈ |h ∪ \{ set \< pr |k suc ; |z + |m \> \} ⟹ \< pr i ; u \> ∈ |h` / ∪. / set1. -| hyK , pr:0 , Lirr , 𝕄1 p;
    Lstep <- `i ∈ |k suc and \< pr i ; u \> ∈ |h ⟹ \< pr i suc ; u + |m \> ∈ |h ∪ \{ set \< pr |k suc ; |z + |m \> \}` / ∪. / set1. -| hyH , hyS , hyZ , suc.' , Lfuniq , Lsucin , pr:0 p;
    Lfin <- `|k suc ∈ 𝕄 and |h ∪ \{ set \< pr |k suc ; |z + |m \> \} ∈ |k suc suc → 𝕄 and \< pr 0 ; 0 \> ∈ |h ∪ \{ set \< pr |k suc ; |z + |m \> \} and [ ∀ i ∈ |k suc . [ ∀ u (\< pr i ; u \> ∈ |h ∪ \{ set \< pr |k suc ; |z + |m \> \} ⟹ \< pr i suc ; u + |m \> ∈ |h ∪ \{ set \< pr |k suc ; |z + |m \> \}) ] ]` -| hyK , `\< pr 0 ; 0 \> ∈ |h` , Lmap , Lold , Lstep , 𝕄1 , ∪. p;
    LMS -| W. , ax_s h[fix];
!let/thm LME <- `m ∈ 𝕄 and k ∈ 𝕄 ⟹ [ ∃ h \, k ∈ 𝕄 and h ∈ k suc → 𝕄 and \< pr 0 ; 0 \> ∈ h and [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u + m \> ∈ h) ] ] ]` ◀ W. , ax_s
prf LME -| INDC[D_:=`\{ cls k | [ ∃ h \, k ∈ 𝕄 and h ∈ k suc → 𝕄 and \< pr 0 ; 0 \> ∈ h and [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u + m \> ∈ h) ] ] ] \}`] , LM0 , LMS , Lftot , Lsucin v;
    LME -| W. , ax_s h;
!let/thm LMP <- `k ∈ 𝕄 and h ∈ k suc → 𝕄 and \< pr 0 ; 0 \> ∈ h and [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u + m \> ∈ h) ] ] and \< pr n suc ; y \> ∈ h ⟹ [ ∃ z \, \< pr n ; z \> ∈ h and y = z + m ]` ◀ W. , ax_s
prf LMP -| Lfdom , Lsucinv , suc.' , Lftot , Lfuniq p; LMP -| W. , ax_s h;
!let/thm LMU <- `k1 ∈ 𝕄 and h1 ∈ k1 suc → 𝕄 and \< pr 0 ; 0 \> ∈ h1 and [ ∀ i ∈ k1 . [ ∀ u (\< pr i ; u \> ∈ h1 ⟹ \< pr i suc ; u + m \> ∈ h1) ] ] and k2 ∈ 𝕄 and h2 ∈ k2 suc → 𝕄 and \< pr 0 ; 0 \> ∈ h2 and [ ∀ i ∈ k2 . [ ∀ u (\< pr i ; u \> ∈ h2 ⟹ \< pr i suc ; u + m \> ∈ h2) ] ] and n ∈ 𝕄 and \< pr n ; y1 \> ∈ h1 and \< pr n ; y2 \> ∈ h2 ⟹ y1 = y2` ◀ W. , ax_s
prf hyH1 <- `|h1 ∈ |k1 suc → 𝕄` ;
    hy01 <- `\< pr 0 ; 0 \> ∈ |h1` ;
    hyS1 <- `[ ∀ i ∈ |k1 . [ ∀ u (\< pr i ; u \> ∈ |h1 ⟹ \< pr i suc ; u + |m \> ∈ |h1) ] ]` ;
    hyH2 <- `|h2 ∈ |k2 suc → 𝕄` ;
    hy02 <- `\< pr 0 ; 0 \> ∈ |h2` ;
    hyS2 <- `[ ∀ i ∈ |k2 . [ ∀ u (\< pr i ; u \> ∈ |h2 ⟹ \< pr i suc ; u + |m \> ∈ |h2) ] ]` ;
    LU0 <- `\< pr 0 ; y1 \> ∈ |h1 and \< pr 0 ; y2 \> ∈ |h2 ⟹ y1 = y2` -| hyH1 , hyH2 , hy01 , hy02 , Lfuniq , Lfdom p;
    LUs <- `[ ∀ y1 ; y2 (\< pr n ; y1 \> ∈ |h1 and \< pr n ; y2 \> ∈ |h2 ⟹ y1 = y2) ] and \< pr n suc ; y1 \> ∈ |h1 and \< pr n suc ; y2 \> ∈ |h2 ⟹ y1 = y2` -| `|k1 ∈ 𝕄` , hyH1 , hy01 , hyS1 , `|k2 ∈ 𝕄` , hyH2 , hy02 , hyS2 , LMP v;
    Lfin <- `|y1 = |y2` -| INDC[D_:=`\{ cls n | [ ∀ y1 ; y2 (\< pr n ; y1 \> ∈ |h1 and \< pr n ; y2 \> ∈ |h2 ⟹ y1 = y2) ] \}`] , LU0 , LUs , `|n ∈ 𝕄` , `\< pr |n ; |y1 \> ∈ |h1` , `\< pr |n ; |y2 \> ∈ |h2` v;
    LMU -| W. , ax_s h[fix];
!let/thm L⋅! <- `m ∈ 𝕄 and n ∈ 𝕄 ⟹ [ ∃！ w [ ∃ k ; h \, k ∈ 𝕄 and h ∈ k suc → 𝕄 and \< pr 0 ; 0 \> ∈ h and [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u + m \> ∈ h) ] ] and \< pr n ; w \> ∈ h ] ]` ◀ W. , ax_s
prf L⋅! -| LME , Lsucin , Lftot , LMU v; L⋅! -| W. , ax_s h;
!let/thm LMval <- `m ∈ 𝕄 and k ∈ 𝕄 and h ∈ k suc → 𝕄 and \< pr 0 ; 0 \> ∈ h and [ ∀ i ∈ k . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u + m \> ∈ h) ] ] and \< pr n ; y \> ∈ h ⟹ m ⋅ n = y` ◀ W. , ax_s
prf hyK <- `|k ∈ 𝕄` ;
    hyH <- `|h ∈ |k suc → 𝕄` ;
    hyS <- `[ ∀ i ∈ |k . [ ∀ u (\< pr i ; u \> ∈ |h ⟹ \< pr i suc ; u + |m \> ∈ |h) ] ]` ;
    hyY <- `\< pr |n ; |y \> ∈ |h` ;
    Lm <- `|n ∈ 𝕄` -| hyK , hyH , hyY , Lfdom , 𝕄1 , LinM p;
    Lfin <- `|m ⋅ |n = |y` -| ⋅. , L⋅! , `|m ∈ 𝕄` , Lm , hyK , hyH , `\< pr 0 ; 0 \> ∈ |h` , hyS , hyY v;
    LMval -| W. , ax_s h[fix];
prop/thm *𝕄 ◀ W. , ax_s
prf LS0 <- `|m ⋅ |n suc = |m ⋅ |n + |m` -| LME , LMval , Lftot , Lsucin , suc.' , 𝕄1 , `|m ∈ 𝕄` , `|n ∈ 𝕄` v;
    L⋅S <- `m ∈ 𝕄 and n ∈ 𝕄 ⟹ m ⋅ n suc = m ⋅ n + m` -| W. , ax_s h[fix];
    *𝕄 -| LM0 , LMval , L⋅S p;
    *𝕄 -| W. , ax_s h;
let/thm ⋅∈𝕄 <- `[ m ; n col ∈ 𝕄 ] ⟹ m ⋅ n ∈ 𝕄` ◀ W. , ax_s
prf ⋅∈𝕄 -| LME , Lsucin , Lftot , LMval , Lfval v; ⋅∈𝕄 -| W. , ax_s h;

standard_math/2-def.book

`standard_math/2-def.book`