---

Step * of Lemma rabs-rmul-rleq

No Annotations
∀[x,y,a,b:ℝ].  (|x * y| ≤ (a * b)) supposing ((|y| ≤ b) and (|x| ≤ a))
BY
{ (Auto
   THEN ((InstLemma `rmul_functionality_wrt_rleq` [⌜|x|⌝; ⌜|y|⌝; ⌜a⌝])⋅ THENA Auto)
   THEN Assert ⌜r0 ≤ |x|⌝⋅
   THEN Auto
   THEN nRMul ⌜a⌝ (-3)⋅
   THEN Auto
   THEN RWO "rabs-rmul" 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[x,y,a,b:\mBbbR{}].    (|x  *  y|  \mleq{}  (a  *  b))  supposing  ((|y|  \mleq{}  b)  and  (|x|  \mleq{}  a))


By

---

Latex:
(Auto
  THEN  ((InstLemma  `rmul\_functionality\_wrt\_rleq`  [\mkleeneopen{}|x|\mkleeneclose{};  \mkleeneopen{}|y|\mkleeneclose{};  \mkleeneopen{}a\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  Assert  \mkleeneopen{}r0  \mleq{}  |x|\mkleeneclose{}\mcdot{}
  THEN  Auto
  THEN  nRMul  \mkleeneopen{}a\mkleeneclose{}  (-3)\mcdot{}
  THEN  Auto
  THEN  RWO  "rabs-rmul"  0
  THEN  Auto)

---

Home Index