---

Step * of Lemma omega-shadow-exact1

∀b:ℕ+. ∀c,d:ℤ.  (∃x:ℤ. ((c ≤ x) ∧ ((b * x) ≤ d)) ⇐⇒ (b * c) ≤ d)
BY
{ (Auto THEN ExRepD THEN (Assert c ≤ (1 * x) BY Auto) THEN FLemma `omega-shadow` [-1;-2] THEN Auto) }

---

Latex:

---

Latex:
\mforall{}b:\mBbbN{}\msupplus{}.  \mforall{}c,d:\mBbbZ{}.    (\mexists{}x:\mBbbZ{}.  ((c  \mleq{}  x)  \mwedge{}  ((b  *  x)  \mleq{}  d))  \mLeftarrow{}{}\mRightarrow{}  (b  *  c)  \mleq{}  d)


By

---

Latex:
(Auto  THEN  ExRepD  THEN  (Assert  c  \mleq{}  (1  *  x)  BY  Auto)  THEN  FLemma  `omega-shadow`  [-1;-2]  THEN  Auto)

---

Home Index