---

Step * 2 1 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. (¬(n1 ≤ x)) ∨ (¬x < n2)
⊢ x < n1 ∨ (x ≥ n2 )
BY
{ D (-1) }

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. ¬(n1 ≤ x)
⊢ x < n1 ∨ (x ≥ n2 )

2
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 )

---

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{}(n1  \mleq{}  x))  \mvee{}  (\mneg{}x  <  n2)
\mvdash{}  x  <  n1  \mvee{}  (x  \mgeq{}  n2  )


By

---

Latex:
D  (-1)

---

Home Index