---

Step * 1 of Lemma from-upto-member-nat


1. n : ℕ
2. m : ℕ
3. k : ℕ
4. (k ∈ [n, m))
⊢ (n ≤ k) ∧ k < m
BY
{ (RepeatFor 2 (D (-1)) THEN (RWO "length-from-upto" (-2) THENA Auto) THEN (SplitOnHypITE -2  THENA Auto)) }

1
.....truecase..... 
1. n : ℕ
2. m : ℕ
3. k : ℕ
4. i : ℕ
5. i < m - n
6. k = [n, m)[i] ∈ ℕ
7. n < m
⊢ (n ≤ k) ∧ k < m

2
.....falsecase..... 
1. n : ℕ
2. m : ℕ
3. k : ℕ
4. i : ℕ
5. i < 0
6. k = [n, m)[i] ∈ ℕ
7. ¬n < m
⊢ (n ≤ k) ∧ k < m

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  m  :  \mBbbN{}
3.  k  :  \mBbbN{}
4.  (k  \mmember{}  [n,  m))
\mvdash{}  (n  \mleq{}  k)  \mwedge{}  k  <  m


By

---

Latex:
(RepeatFor  2  (D  (-1))
  THEN  (RWO  "length-from-upto"  (-2)  THENA  Auto)
  THEN  (SplitOnHypITE  -2    THENA  Auto))

---

Home Index