---

Step * of Lemma mul-initial-seg-step

∀[f:ℕ ⟶ ℕ]. ∀[m:ℕ+].  ((mul-initial-seg(f) m) = ((mul-initial-seg(f) (m - 1)) * (f (m - 1))) ∈ ℤ)
BY
{ xxxInductionOnNatxxx }

1
.....basecase..... 
1. f : ℕ ⟶ ℕ
2. m : ℕ+
⊢ (mul-initial-seg(f) 1) = ((mul-initial-seg(f) (1 - 1)) * (f (1 - 1))) ∈ ℤ

2
.....upcase..... 
1. f : ℕ ⟶ ℕ
2. m : ℤ
3. 0 < m
4. (mul-initial-seg(f) m) = ((mul-initial-seg(f) (m - 1)) * (f (m - 1))) ∈ ℤ
⊢ (mul-initial-seg(f) (m + 1)) = ((mul-initial-seg(f) ((m + 1) - 1)) * (f ((m + 1) - 1))) ∈ ℤ

---

Latex:

---

Latex:
\mforall{}[f:\mBbbN{}  {}\mrightarrow{}  \mBbbN{}].  \mforall{}[m:\mBbbN{}\msupplus{}].    ((mul-initial-seg(f)  m)  =  ((mul-initial-seg(f)  (m  -  1))  *  (f  (m  -  1))))


By

---

Latex:
xxxInductionOnNatxxx

---

Home Index