---

Step * of Lemma omega-shadow

∀a,b:ℕ+. ∀c,d,x:ℤ.  ((c ≤ (a * x)) ⇒ ((b * x) ≤ d) ⇒ ((b * c) ≤ (a * d)))
BY
{ ((UnivCD THENA Auto) THEN Auto THEN Mul ⌜b⌝ (-2)⋅ THEN Mul ⌜a⌝ (-2)⋅ THEN Auto) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  Auto  THEN  Mul  \mkleeneopen{}b\mkleeneclose{}  (-2)\mcdot{}  THEN  Mul  \mkleeneopen{}a\mkleeneclose{}  (-2)\mcdot{}  THEN  Auto)

---

Home Index