---

Step * 1 of Lemma imax-list-unique


1. L : ℤ List
2. a : ℤ
3. (a ∈ L)
4. 0 < ||L||
5. (a ≤ imax-list(L)) ⇒ (∃b∈L. a ≤ b)
6. (a ≤ imax-list(L)) ⇐ (∃b∈L. a ≤ b)
7. (∀b∈L.b ≤ a)
8. imax-list(L) ≤ a
9. (∀b∈L.b ≤ a)
⊢ imax-list(L) = a ∈ ℤ
BY
{ (D -4 THEN Auto' THEN BLemma `l_exists_iff` THEN Auto THEN With ⌜a⌝ (D 0)⋅ THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  L  :  \mBbbZ{}  List
2.  a  :  \mBbbZ{}
3.  (a  \mmember{}  L)
4.  0  <  ||L||
5.  (a  \mleq{}  imax-list(L))  {}\mRightarrow{}  (\mexists{}b\mmember{}L.  a  \mleq{}  b)
6.  (a  \mleq{}  imax-list(L))  \mLeftarrow{}{}  (\mexists{}b\mmember{}L.  a  \mleq{}  b)
7.  (\mforall{}b\mmember{}L.b  \mleq{}  a)
8.  imax-list(L)  \mleq{}  a
9.  (\mforall{}b\mmember{}L.b  \mleq{}  a)
\mvdash{}  imax-list(L)  =  a


By

---

Latex:
(D  -4  THEN  Auto'  THEN  BLemma  `l\_exists\_iff`  THEN  Auto  THEN  With  \mkleeneopen{}a\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)\mcdot{}

---

Home Index