---

Step * of Lemma rabs-rmul-rleq-rabs

∀[x,y,a,b:ℝ].  (|x * y| ≤ |a * b|) supposing ((|y| ≤ |b|) and (|x| ≤ |a|))
BY
{ (Auto THEN RW (AddrC [2] (LemmaC `rabs-rmul`)) 0 THEN EAuto 1) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  RW  (AddrC  [2]  (LemmaC  `rabs-rmul`))  0  THEN  EAuto  1)

---

Home Index