Step
*
1
1
1
1
1
2
1
1
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)
11. n + 1 < k
12. ∃k:K. (((n + 1) ≤ k) ∧ (∀j:ℕ. (((n + 1) ≤ j) ⇒ (j ∈ K) ⇒ (k ≤ j))))
⊢ ∃k:K. ((n ≤ k) ∧ (∀j:ℕ. ((n ≤ j) ⇒ (j ∈ K) ⇒ (k ≤ j))))
BY
{ RepeatFor 2 (ParallelLast) }
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
12. k1 : K
13. ∀j:ℕ. (((n + 1) ≤ j) ⇒ (j ∈ K) ⇒ (k1 ≤ j))
14. (n + 1) ≤ k1
⊢ n ≤ k1
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
12. k1 : K
13. (n + 1) ≤ k1
14. ∀j:ℕ. (((n + 1) ≤ j) ⇒ (j ∈ K) ⇒ (k1 ≤ j))
⊢ ∀j:ℕ. ((n ≤ j) ⇒ (j ∈ K) ⇒ (k1 ≤ 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)
11. n + 1 < k
12. \mexists{}k:K. (((n + 1) \mleq{} k) \mwedge{} (\mforall{}j:\mBbbN{}. (((n + 1) \mleq{} j) {}\mRightarrow{} (j \mmember{} K) {}\mRightarrow{} (k \mleq{} j))))
\mvdash{} \mexists{}k:K. ((n \mleq{} k) \mwedge{} (\mforall{}j:\mBbbN{}. ((n \mleq{} j) {}\mRightarrow{} (j \mmember{} K) {}\mRightarrow{} (k \mleq{} j))))
By
Latex:
RepeatFor 2 (ParallelLast)
Home
Index