---

Step * 1 1 1 of Lemma int_seg-cardinality-le


1. i : ℤ
2. j : ℤ
3. i ≤ j
4. b : {i..j-}
⊢ ∃a:ℕj - i. ((i + a) = b ∈ {i..j-})
BY
{ (InstConcl [⌜b - i⌝] ⋅ THEN Auto') }

---

Latex:

---

Latex:

1.  i  :  \mBbbZ{}
2.  j  :  \mBbbZ{}
3.  i  \mleq{}  j
4.  b  :  \{i..j\msupminus{}\}
\mvdash{}  \mexists{}a:\mBbbN{}j  -  i.  ((i  +  a)  =  b)


By

---

Latex:
(InstConcl  [\mkleeneopen{}b  -  i\mkleeneclose{}]  \mcdot{}  THEN  Auto')

---

Home Index