---

Step * 2 1 2 of Lemma l_disjoint_from-upto


1. [L] : ℤ List
2. n1 : ℤ@i
3. [n2] : ℤ
4. ∀x:ℤ. (¬((x ∈ L) ∧ (x ∈ [n1, n2))))
5. x : ℤ@i
6. (x ∈ L)@i
7. ¬(x ∈ [n1, n2))
8. ¬x < n2
⊢ x < n1 ∨ (x ≥ n2 )
BY
{ (OrRight THENA Auto) }

1
1. [L] : ℤ List
2. n1 : ℤ@i
3. [n2] : ℤ
4. ∀x:ℤ. (¬((x ∈ L) ∧ (x ∈ [n1, n2))))
5. x : ℤ@i
6. (x ∈ L)@i
7. ¬(x ∈ [n1, n2))
8. ¬x < n2
⊢ x ≥ n2 

---

Latex:

---

Latex:

1.  [L]  :  \mBbbZ{}  List
2.  n1  :  \mBbbZ{}@i
3.  [n2]  :  \mBbbZ{}
4.  \mforall{}x:\mBbbZ{}.  (\mneg{}((x  \mmember{}  L)  \mwedge{}  (x  \mmember{}  [n1,  n2))))
5.  x  :  \mBbbZ{}@i
6.  (x  \mmember{}  L)@i
7.  \mneg{}(x  \mmember{}  [n1,  n2))
8.  \mneg{}x  <  n2
\mvdash{}  x  <  n1  \mvee{}  (x  \mgeq{}  n2  )


By

---

Latex:
(OrRight  THENA  Auto)

---

Home Index