Step
*
1
1
1
1
2
2
of Lemma
genfact-unbounded
1. f : ℕ+ ⟶ ℤ
2. ∀m:ℕ+. 1 < f[m]
3. b : ℕ+
4. N : ℤ
5. [n] : ℕ
6. ∀[m:ℕn]. ∀k:ℕ. ∀x:{x:ℤ| x = genfact(k;b;m.f[m]) ∈ ℤ} . ∃n:ℕ [(N ≤ genfact(n;b;m.f[m]))] supposing N ≤ (x + m)
7. k : ℕ
8. x : {x:ℤ| x = genfact(k;b;m.f[m]) ∈ ℤ}
9. N ≤ (x + n)
10. ¬(N ≤ x)
11. k' : ℤ
12. k' = (k + 1) ∈ ℤ
13. z : ℤ
14. z = f[k'] ∈ ℤ
15. x' : ℤ
16. x' = (z * x) ∈ ℤ
17. x' = genfact(k';b;m.f[m]) ∈ ℤ
18. x ∈ ℕ+
⊢ ∃n:ℕ [(N ≤ genfact(n;b;m.f[m]))]
BY
{ ((Assert 1 < f[k'] BY Auto) THEN Mul ⌜x⌝ (-1)⋅ THEN (Subst' x * f[k'] ~ x' -1 THENA (RWO "-7<" 0 THEN Auto))) }
1
1. f : ℕ+ ⟶ ℤ
2. ∀m:ℕ+. 1 < f[m]
3. b : ℕ+
4. N : ℤ
5. [n] : ℕ
6. ∀[m:ℕn]. ∀k:ℕ. ∀x:{x:ℤ| x = genfact(k;b;m.f[m]) ∈ ℤ} . ∃n:ℕ [(N ≤ genfact(n;b;m.f[m]))] supposing N ≤ (x + m)
7. k : ℕ
8. x : {x:ℤ| x = genfact(k;b;m.f[m]) ∈ ℤ}
9. N ≤ (x + n)
10. ¬(N ≤ x)
11. k' : ℤ
12. k' = (k + 1) ∈ ℤ
13. z : ℤ
14. z = f[k'] ∈ ℤ
15. x' : ℤ
16. x' = (z * x) ∈ ℤ
17. x' = genfact(k';b;m.f[m]) ∈ ℤ
18. x ∈ ℕ+
19. 1 < f[k']
20. x * 1 < x'
⊢ ∃n:ℕ [(N ≤ genfact(n;b;m.f[m]))]
Latex:
Latex:
1. f : \mBbbN{}\msupplus{} {}\mrightarrow{} \mBbbZ{}
2. \mforall{}m:\mBbbN{}\msupplus{}. 1 < f[m]
3. b : \mBbbN{}\msupplus{}
4. N : \mBbbZ{}
5. [n] : \mBbbN{}
6. \mforall{}[m:\mBbbN{}n]
\mforall{}k:\mBbbN{}. \mforall{}x:\{x:\mBbbZ{}| x = genfact(k;b;m.f[m])\} .
\mexists{}n:\mBbbN{} [(N \mleq{} genfact(n;b;m.f[m]))] supposing N \mleq{} (x + m)
7. k : \mBbbN{}
8. x : \{x:\mBbbZ{}| x = genfact(k;b;m.f[m])\}
9. N \mleq{} (x + n)
10. \mneg{}(N \mleq{} x)
11. k' : \mBbbZ{}
12. k' = (k + 1)
13. z : \mBbbZ{}
14. z = f[k']
15. x' : \mBbbZ{}
16. x' = (z * x)
17. x' = genfact(k';b;m.f[m])
18. x \mmember{} \mBbbN{}\msupplus{}
\mvdash{} \mexists{}n:\mBbbN{} [(N \mleq{} genfact(n;b;m.f[m]))]
By
Latex:
((Assert 1 < f[k'] BY
Auto)
THEN Mul \mkleeneopen{}x\mkleeneclose{} (-1)\mcdot{}
THEN (Subst' x * f[k'] \msim{} x' -1 THENA (RWO "-7<" 0 THEN Auto)))
Home
Index