---

Step * of Lemma genfact-unbounded

∀f:ℕ+ ⟶ ℤ. ∀b:ℕ+. ∀N:ℤ.  (∃n:ℕ [(N ≤ genfact(n;b;m.f[m]))]) supposing ∀m:ℕ+. 1 < f[m]
BY
{ (Auto THEN (Evaluate ⌜M = N ∈ ℤ⌝⋅ THENA Auto) THEN RevHypSubst' (-1) 0 THEN ThinVar `N' THEN RenameVar `N' (-1)) }

1
1. f : ℕ+ ⟶ ℤ
2. ∀m:ℕ+. 1 < f[m]
3. b : ℕ+
4. N : ℤ
⊢ ∃n:ℕ [(N ≤ genfact(n;b;m.f[m]))]

---

Latex:

---

Latex:
\mforall{}f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbZ{}.  \mforall{}b:\mBbbN{}\msupplus{}.  \mforall{}N:\mBbbZ{}.    (\mexists{}n:\mBbbN{}  [(N  \mleq{}  genfact(n;b;m.f[m]))])  supposing  \mforall{}m:\mBbbN{}\msupplus{}.  1  <  f[m]


By

---

Latex:
(Auto
  THEN  (Evaluate  \mkleeneopen{}M  =  N\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RevHypSubst'  (-1)  0
  THEN  ThinVar  `N'
  THEN  RenameVar  `N'  (-1))

---

Home Index