---

Step * 1 1 1 1 1 2 of Lemma unbounded-decidable-nset-infinite


1. K : Type
2. K ⊆r ℕ
3. D : ℤ
4. [%3] : 0 < D
5. ∀n:ℕ. ∀k:K.  (n < k ⇒ (k ≤ (n + (D - 1))) ⇒ (∃k:K. ((n ≤ k) ∧ (∀j:ℕ. ((n ≤ j) ⇒ (j ∈ K) ⇒ (k ≤ j))))))
6. n : ℕ
7. k : K
8. n < k
9. k ≤ (n + D)
10. ¬(n ∈ K)
⊢ ∃k:K. ((n ≤ k) ∧ (∀j:ℕ. ((n ≤ j) ⇒ (j ∈ K) ⇒ (k ≤ j))))
BY
{ (Decide ⌜n + 1 < k⌝⋅ THENA Auto) }

1
1. K : Type
2. K ⊆r ℕ
3. D : ℤ
4. [%3] : 0 < D
5. ∀n:ℕ. ∀k:K.  (n < k ⇒ (k ≤ (n + (D - 1))) ⇒ (∃k:K. ((n ≤ k) ∧ (∀j:ℕ. ((n ≤ j) ⇒ (j ∈ K) ⇒ (k ≤ j))))))
6. n : ℕ
7. k : K
8. n < k
9. k ≤ (n + D)
10. ¬(n ∈ K)
11. n + 1 < k
⊢ ∃k:K. ((n ≤ k) ∧ (∀j:ℕ. ((n ≤ j) ⇒ (j ∈ K) ⇒ (k ≤ j))))

2
1. K : Type
2. K ⊆r ℕ
3. D : ℤ
4. [%3] : 0 < D
5. ∀n:ℕ. ∀k:K.  (n < k ⇒ (k ≤ (n + (D - 1))) ⇒ (∃k:K. ((n ≤ k) ∧ (∀j:ℕ. ((n ≤ j) ⇒ (j ∈ K) ⇒ (k ≤ j))))))
6. n : ℕ
7. k : K
8. n < k
9. k ≤ (n + D)
10. ¬(n ∈ K)
11. ¬n + 1 < k
⊢ ∃k:K. ((n ≤ k) ∧ (∀j:ℕ. ((n ≤ j) ⇒ (j ∈ K) ⇒ (k ≤ j))))

---

Latex:

---

Latex:

1.  K  :  Type
2.  K  \msubseteq{}r  \mBbbN{}
3.  D  :  \mBbbZ{}
4.  [\%3]  :  0  <  D
5.  \mforall{}n:\mBbbN{}.  \mforall{}k:K.
          (n  <  k  {}\mRightarrow{}  (k  \mleq{}  (n  +  (D  -  1)))  {}\mRightarrow{}  (\mexists{}k:K.  ((n  \mleq{}  k)  \mwedge{}  (\mforall{}j:\mBbbN{}.  ((n  \mleq{}  j)  {}\mRightarrow{}  (j  \mmember{}  K)  {}\mRightarrow{}  (k  \mleq{}  j))))))
6.  n  :  \mBbbN{}
7.  k  :  K
8.  n  <  k
9.  k  \mleq{}  (n  +  D)
10.  \mneg{}(n  \mmember{}  K)
\mvdash{}  \mexists{}k:K.  ((n  \mleq{}  k)  \mwedge{}  (\mforall{}j:\mBbbN{}.  ((n  \mleq{}  j)  {}\mRightarrow{}  (j  \mmember{}  K)  {}\mRightarrow{}  (k  \mleq{}  j))))


By

---

Latex:
(Decide  \mkleeneopen{}n  +  1  <  k\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index