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 Lz <- `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 ⟹ z suc ∈ 𝕄` -| Lfval ,, 𝕄1 p;
    Lmap <- `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 ⟹ (h ∪ \{ set \< pr k suc ; z suc \> \}) ∈ k suc suc → 𝕄` -| L→suc ,, Lirr ,, 𝕄1 ,, Lz p;
    Lold <- `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 i ∈ k suc and \< pr i ; u \> ∈ h ∪ \{ set \< pr k suc ; z suc \> \} ⟹ \< pr i ; u \> ∈ h` / ∪. / set1. -| pr:0 ,, Lirr ,, 𝕄1 p;
    Lstep <- `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 and i ∈ k suc and \< pr i ; u \> ∈ h ⟹ \< pr i suc ; u suc \> ∈ h ∪ \{ set \< pr k suc ; z suc \> \}` / ∪. / set1. -| suc.' ,, Lfuniq ,, Lsucin ,, pr:0 p;
    Lstep2 <- `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 and i ∈ k suc and \< pr i ; u \> ∈ h ∪ \{ set \< pr k suc ; z suc \> \} ⟹ \< pr i suc ; u suc \> ∈ h ∪ \{ set \< pr k suc ; z suc \> \}` -| Lold ,, Lstep p;
    LAS -| Lmap ,, Lstep2 ,, 𝕄1 ,, ∪. p;
    LAS -| W. ,, ax_s h;
!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 B_ := `\{ 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) ] ]) ] \}` ;
    LBs <- `B_ ⊂_ 𝕄` -| O p;
    LBe <- `Exi B_` -| LBs ,, `∃ Z \, B_ ⊂_ Z ⟹ Exi B_` p;
    LBm <- `B =_ B_ ⟹ [ ∀ k (k ∈ B ⟺ k ∈ 𝕄 and [ ∃ 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) ] ]) ]) ]` -| O p;
    LEb <- `[ ∀ k (k ∈ B ⟺ k ∈ 𝕄 and [ ∃ 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 m ∈ 𝕄 ⟹ 0 ∈ B` -| LA0 p;
    LE1 <- `[ ∀ k (k ∈ B ⟺ k ∈ 𝕄 and [ ∃ 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) ] ]) ]) ] ⟹ [ ∀ j ∈ 𝕄 . (j ∈ B ⟹ j suc ∈ B) ]` -| LAS ,, Lftot ,, Lsucin p;
    LE2 <- `[ ∀ k (k ∈ B ⟺ k ∈ 𝕄 and [ ∃ 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 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) ] ]) ]` -| LEb ,, LE1 ,, INDS v;
    LAE -| LBe ,, LBm ,, LE2 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 B_ := `\{ cls n ∈ 𝕄 | [ ∀ y1 ; y2 (\< pr n ; y1 \> ∈ h1 and \< pr n ; y2 \> ∈ h2 ⟹ y1 = y2) ] \}` ;
    LBs <- `B_ ⊂_ 𝕄` -| O p;
    LBe <- `Exi B_` -| LBs ,, `∃ Z \, B_ ⊂_ Z ⟹ Exi B_` p;
    LBm <- `B =_ B_ ⟹ [ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and [ ∀ y1 ; y2 (\< pr n ; y1 \> ∈ h1 and \< pr n ; y2 \> ∈ h2 ⟹ y1 = y2) ]) ]` -| O p;
    L0 <- `0 ∈ 𝕄` / 𝕄. -| O p;
    LU0 <- `h1 ∈ k1 suc → 𝕄 and h2 ∈ k2 suc → 𝕄 and \< pr 0 ; m \> ∈ h1 and \< pr 0 ; m \> ∈ h2 and \< pr 0 ; y1 \> ∈ h1 and \< pr 0 ; y2 \> ∈ h2 ⟹ y1 = y2` -| Lfuniq ,, Lfdom p;
    LUs <- `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 [ ∀ 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` -| LAP p;
    LUa <- `[ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and [ ∀ y1 ; y2 (\< pr n ; y1 \> ∈ h1 and \< pr n ; y2 \> ∈ h2 ⟹ y1 = y2) ]) ] and 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) ] ] ⟹ 0 ∈ B` -| L0 ,, LU0 p;
    LUb <- `[ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and [ ∀ y1 ; y2 (\< pr n ; y1 \> ∈ h1 and \< pr n ; y2 \> ∈ h2 ⟹ y1 = y2) ]) ] and 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) ] ] ⟹ [ ∀ j ∈ 𝕄 . (j ∈ B ⟹ j suc ∈ B) ]` -| LUs ,, 𝕄1 v;
    LU2 <- `[ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and [ ∀ y1 ; y2 (\< pr n ; y1 \> ∈ h1 and \< pr n ; y2 \> ∈ h2 ⟹ y1 = y2) ]) ] and 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 ∈ 𝕄 ⟹ n ∈ B` -| LUa ,, LUb ,, INDS v;
    LAU -| LBe ,, LBm ,, LU2 v;
    LAU -| W. ,, ax_s h;
!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 Ls <- `n suc ∈ 𝕄 and h ∈ n suc suc → 𝕄 and \< pr 0 ; m \> ∈ h and [ ∀ i ∈ n suc . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u suc \> ∈ h) ] ] and \< pr n ; z \> ∈ h ⟹ m + n suc = (m + n) suc` -| Lval ,, Lsucin p;
    Le <- `m ∈ 𝕄 and n ∈ 𝕄 ⟹ [ ∃ h \, (n suc ∈ 𝕄 and h ∈ n suc suc → 𝕄 and \< pr 0 ; m \> ∈ h and [ ∀ i ∈ n suc . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u suc \> ∈ h) ] ] and [ ∃ z \, \< pr n ; z \> ∈ h ]) ]` -| LAE ,, 𝕄1 ,, Lftot ,, Lsucin ,, suc.' p;
    +𝕄 -| LA0 ,, Lval ,, Ls ,, Le 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 Lz <- `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 ⟹ z + m ∈ 𝕄` -| Lfval ,, +∈𝕄 p;
    Lmap <- `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 ⟹ (h ∪ \{ set \< pr k suc ; z + m \> \}) ∈ k suc suc → 𝕄` -| L→suc ,, Lirr ,, 𝕄1 ,, Lz p;
    Lold <- `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 i ∈ k suc and \< pr i ; u \> ∈ h ∪ \{ set \< pr k suc ; z + m \> \} ⟹ \< pr i ; u \> ∈ h` / ∪. / set1. -| pr:0 ,, Lirr ,, 𝕄1 p;
    Lstep <- `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 and i ∈ k suc and \< pr i ; u \> ∈ h ⟹ \< pr i suc ; u + m \> ∈ h ∪ \{ set \< pr k suc ; z + m \> \}` / ∪. / set1. -| suc.' ,, Lfuniq ,, Lsucin ,, pr:0 p;
    Lstep2 <- `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 and i ∈ k suc and \< pr i ; u \> ∈ h ∪ \{ set \< pr k suc ; z + m \> \} ⟹ \< pr i suc ; u + m \> ∈ h ∪ \{ set \< pr k suc ; z + m \> \}` -| Lold ,, Lstep p;
    LMS -| Lmap ,, Lstep2 ,, 𝕄1 ,, ∪. p;
    LMS -| W. ,, ax_s h;
!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 B_ := `\{ 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) ] ]) ] \}` ;
    LBs <- `B_ ⊂_ 𝕄` -| O p;
    LBe <- `Exi B_` -| LBs ,, `∃ Z \, B_ ⊂_ Z ⟹ Exi B_` p;
    LBm <- `B =_ B_ ⟹ [ ∀ k (k ∈ B ⟺ k ∈ 𝕄 and [ ∃ 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) ] ]) ]) ]` -| O p;
    LEb <- `[ ∀ k (k ∈ B ⟺ k ∈ 𝕄 and [ ∃ 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 m ∈ 𝕄 ⟹ 0 ∈ B` -| LM0 p;
    LE1 <- `[ ∀ k (k ∈ B ⟺ k ∈ 𝕄 and [ ∃ 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 m ∈ 𝕄 ⟹ [ ∀ j ∈ 𝕄 . (j ∈ B ⟹ j suc ∈ B) ]` -| LMS ,, Lftot ,, Lsucin p;
    LE2 <- `[ ∀ k (k ∈ B ⟺ k ∈ 𝕄 and [ ∃ 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 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) ] ]) ]` -| LEb ,, LE1 ,, INDS v;
    LME -| LBe ,, LBm ,, LE2 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 B_ := `\{ cls n ∈ 𝕄 | [ ∀ y1 ; y2 (\< pr n ; y1 \> ∈ h1 and \< pr n ; y2 \> ∈ h2 ⟹ y1 = y2) ] \}` ;
    LBs <- `B_ ⊂_ 𝕄` -| O p;
    LBe <- `Exi B_` -| LBs ,, `∃ Z \, B_ ⊂_ Z ⟹ Exi B_` p;
    LBm <- `B =_ B_ ⟹ [ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and [ ∀ y1 ; y2 (\< pr n ; y1 \> ∈ h1 and \< pr n ; y2 \> ∈ h2 ⟹ y1 = y2) ]) ]` -| O p;
    L0 <- `0 ∈ 𝕄` / 𝕄. -| O p;
    LU0 <- `h1 ∈ k1 suc → 𝕄 and h2 ∈ k2 suc → 𝕄 and \< pr 0 ; 0 \> ∈ h1 and \< pr 0 ; 0 \> ∈ h2 and \< pr 0 ; y1 \> ∈ h1 and \< pr 0 ; y2 \> ∈ h2 ⟹ y1 = y2` -| Lfuniq ,, Lfdom p;
    LUs <- `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 [ ∀ 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` -| LMP p;
    LUa <- `[ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and [ ∀ y1 ; y2 (\< pr n ; y1 \> ∈ h1 and \< pr n ; y2 \> ∈ h2 ⟹ y1 = y2) ]) ] and 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) ] ] ⟹ 0 ∈ B` -| L0 ,, LU0 p;
    LUb <- `[ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and [ ∀ y1 ; y2 (\< pr n ; y1 \> ∈ h1 and \< pr n ; y2 \> ∈ h2 ⟹ y1 = y2) ]) ] and 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) ] ] ⟹ [ ∀ j ∈ 𝕄 . (j ∈ B ⟹ j suc ∈ B) ]` -| LUs ,, 𝕄1 v;
    LU2 <- `[ ∀ n (n ∈ B ⟺ n ∈ 𝕄 and [ ∀ y1 ; y2 (\< pr n ; y1 \> ∈ h1 and \< pr n ; y2 \> ∈ h2 ⟹ y1 = y2) ]) ] and 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 ∈ 𝕄 ⟹ n ∈ B` -| LUa ,, LUb ,, INDS v;
    LMU -| LBe ,, LBm ,, LU2 v;
    LMU -| W. ,, ax_s h;
!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 Lm <- `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 ⟹ n ∈ 𝕄` -| Lfdom ,, 𝕄1 ,, LinM p;
    Ldef <- `m ∈ 𝕄 and n ∈ 𝕄 ⟹ ( m ⋅ n = y ⇔ [ ∃ 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 ; y \> ∈ h) ] )` -| ⋅. ,, L⋅! v;
    LMval -| Ldef ,, Lm v;
    LMval -| W. ,, ax_s h;
prop/thm *𝕄 ◀ W. ,, ax_s
prf Ls <- `m ∈ 𝕄 and n suc ∈ 𝕄 and h ∈ n suc suc → 𝕄 and \< pr 0 ; 0 \> ∈ h and [ ∀ i ∈ n suc . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u + m \> ∈ h) ] ] and \< pr n ; z \> ∈ h ⟹ m ⋅ n suc = (m ⋅ n) + m` -| LMval ,, Lsucin p;
    Le <- `m ∈ 𝕄 and n ∈ 𝕄 ⟹ [ ∃ h \, (n suc ∈ 𝕄 and h ∈ n suc suc → 𝕄 and \< pr 0 ; 0 \> ∈ h and [ ∀ i ∈ n suc . [ ∀ u (\< pr i ; u \> ∈ h ⟹ \< pr i suc ; u + m \> ∈ h) ] ] and [ ∃ z \, \< pr n ; z \> ∈ h ]) ]` -| LME ,, 𝕄1 ,, Lftot ,, Lsucin ,, suc.' p;
    *𝕄 -| LM0 ,, LMval ,, Ls ,, Le v;
    *𝕄 -| 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`