---

Step * of Lemma mul_preserves_le2

∀[a,c:ℕ]. ∀[b,d:ℤ].  ((a * c) ≤ (b * d)) supposing ((a ≤ b) and (c ≤ d))
BY
{ ((UnivCD THENA Auto)
   THEN Mul ⌜c⌝ (-1)⋅
   THEN Mul ⌜b⌝ (-3)⋅
   THEN (RW IntNormC  (-2) THENA Auto)
   THEN (RW IntNormC  (-1) THENA Auto)
   THEN RW IntNormC  0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,c:\mBbbN{}].  \mforall{}[b,d:\mBbbZ{}].    ((a  *  c)  \mleq{}  (b  *  d))  supposing  ((a  \mleq{}  b)  and  (c  \mleq{}  d))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Mul  \mkleeneopen{}c\mkleeneclose{}  (-1)\mcdot{}
  THEN  Mul  \mkleeneopen{}b\mkleeneclose{}  (-3)\mcdot{}
  THEN  (RW  IntNormC    (-2)  THENA  Auto)
  THEN  (RW  IntNormC    (-1)  THENA  Auto)
  THEN  RW  IntNormC    0
  THEN  Auto)

---

Home Index