---

Step * 1 1 1 1 2 1 1 of Lemma genfact-unbounded


1. f : ℕ+ ⟶ ℤ
2. b : ℕ+
3. k : ℕ
4. ∀m:ℕ+. 1 < f[m]
⊢ genfact(k;b;m.f[m]) ∈ ℕ+
BY
{ ((MemTypeCD THEN Auto) THEN NatInd (-2) THEN Auto THEN (RWO  "genfact-step" 0 THENA Auto) THEN AutoSplit) }

1
1. f : ℕ+ ⟶ ℤ
2. b : ℕ+
3. ∀m:ℕ+. 1 < f[m]
4. k : ℤ
5. ¬k < 1
6. 0 < k
7. 0 < genfact(k - 1;b;m.f[m])
⊢ 0 < f[k] * genfact(k - 1;b;m.f[m])

---

Latex:

---

Latex:

1.  f  :  \mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}
2.  b  :  \mBbbN{}\msupplus{}
3.  k  :  \mBbbN{}
4.  \mforall{}m:\mBbbN{}\msupplus{}.  1  <  f[m]
\mvdash{}  genfact(k;b;m.f[m])  \mmember{}  \mBbbN{}\msupplus{}


By

---

Latex:
((MemTypeCD  THEN  Auto)
  THEN  NatInd  (-2)
  THEN  Auto
  THEN  (RWO    "genfact-step"  0  THENA  Auto)
  THEN  AutoSplit)

---

Home Index