---

Step * of Lemma rinv_preserves_rless

∀a,b:ℝ.  ((r0 < a) ⇒ (a < b) ⇒ ((r1/b) < (r1/a)))
BY
{ (Auto THEN nRMul ⌜a⌝ 0⋅ THEN nRMul ⌜b⌝ 0⋅ THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,b:\mBbbR{}.    ((r0  <  a)  {}\mRightarrow{}  (a  <  b)  {}\mRightarrow{}  ((r1/b)  <  (r1/a)))


By

---

Latex:
(Auto  THEN  nRMul  \mkleeneopen{}a\mkleeneclose{}  0\mcdot{}  THEN  nRMul  \mkleeneopen{}b\mkleeneclose{}  0\mcdot{}  THEN  Auto)

---

Home Index