---

Step * of Lemma rabs-diff-rdiv

∀[a,b,c,d,x,y:ℝ].
  (c ≠ r0 ⇒ d ≠ r0 ⇒ (|a - b| ≤ x) ⇒ (|(r1/c) - (r1/d)| ≤ y) ⇒ (|(a/c) - (b/d)| ≤ ((|a| * y) + (|(r1/d)| * x))))
BY
{ (Auto
   THEN InstLemma `rabs-diff-rmul` [⌜a⌝;⌜b⌝;⌜(r1/c)⌝;⌜(r1/d)⌝;⌜x⌝;⌜y⌝]⋅
   THEN Auto
   THEN (RWO "-1<" 0 THENA Auto)
   THEN nRNorm 0
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[a,b,c,d,x,y:\mBbbR{}].
    (c  \mneq{}  r0
    {}\mRightarrow{}  d  \mneq{}  r0
    {}\mRightarrow{}  (|a  -  b|  \mleq{}  x)
    {}\mRightarrow{}  (|(r1/c)  -  (r1/d)|  \mleq{}  y)
    {}\mRightarrow{}  (|(a/c)  -  (b/d)|  \mleq{}  ((|a|  *  y)  +  (|(r1/d)|  *  x))))


By

---

Latex:
(Auto
  THEN  InstLemma  `rabs-diff-rmul`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}(r1/c)\mkleeneclose{};\mkleeneopen{}(r1/d)\mkleeneclose{};\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]\mcdot{}
  THEN  Auto
  THEN  (RWO  "-1<"  0  THENA  Auto)
  THEN  nRNorm  0
  THEN  Auto)

---

Home Index