---

Step * 1 1 1 of Lemma equipollent_interval


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

---

Latex:

---

Latex:

1.  a  :  \mBbbZ{}@i
2.  b  :  \mBbbZ{}@i
3.  b@0  :  \mBbbN{}b  -  a@i
\mvdash{}  \mexists{}a@0:\{a..b\msupminus{}\}.  ((a@0  -  a)  =  b@0)


By

---

Latex:
(InstConcl  [\mkleeneopen{}b@0  +  a\mkleeneclose{}]\mcdot{}  THEN  Auto')

---

Home Index