---

Step * 1 of Lemma isEmpty-nat-missing-prop


1. m : ℤ@i
2. (-1) ≤ m@i
3. s1 : ℕ List@i
4. l-ordered(ℕ;x,y.x < y;s1)@i
5. (∀x∈s1.x < m)@i
6. ∀x:ℕ. (¬((x ≤ m) ∧ (¬(x ∈ s1))))@i
⊢ m < 0
BY
{ (Decide ⌈m < 0⌉⋅
   THEN Auto
   THEN (InstHyp [⌈m⌉] (-2)⋅ THENA Auto)
   THEN (RWO "not_over_and" (-1) THENA Auto)
   THEN D (-1)
   THEN Auto
   THEN D (-1)
   THEN (D 0 THENA Auto)
   THEN (RWO "l_all_iff" (-4) THENA Auto)
   THEN InstHyp [⌈m⌉] (-4)⋅
   THEN Auto) }

---

Latex:



1.  m  :  \mBbbZ{}@i
2.  (-1)  \mleq{}  m@i
3.  s1  :  \mBbbN{}  List@i
4.  l-ordered(\mBbbN{};x,y.x  <  y;s1)@i
5.  (\mforall{}x\mmember{}s1.x  <  m)@i
6.  \mforall{}x:\mBbbN{}.  (\mneg{}((x  \mleq{}  m)  \mwedge{}  (\mneg{}(x  \mmember{}  s1))))@i
\mvdash{}  m  <  0


By

(Decide  \mkleeneopen{}m  <  0\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  (InstHyp  [\mkleeneopen{}m\mkleeneclose{}]  (-2)\mcdot{}  THENA  Auto)
  THEN  (RWO  "not\_over\_and"  (-1)  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto
  THEN  D  (-1)
  THEN  (D  0  THENA  Auto)
  THEN  (RWO  "l\_all\_iff"  (-4)  THENA  Auto)
  THEN  InstHyp  [\mkleeneopen{}m\mkleeneclose{}]  (-4)\mcdot{}
  THEN  Auto)

---

Home Index