---

Step * of Lemma rinv-negative

∀x:ℝ. ((x < r0) ⇒ (rinv(x) < r0))
BY
{ (Auto
   THEN FLemma `rminus-reverses-rless` [-1]
   THEN Auto
   THEN (nRNorm (-1) THENA Auto)
   THEN (RW IntNormC (-1) THENA Auto)) }

1
1. x : ℝ
2. x < r0
3. r0 < -(x)
⊢ rinv(x) < r0

---

Latex:

---

Latex:
\mforall{}x:\mBbbR{}.  ((x  <  r0)  {}\mRightarrow{}  (rinv(x)  <  r0))


By

---

Latex:
(Auto
  THEN  FLemma  `rminus-reverses-rless`  [-1]
  THEN  Auto
  THEN  (nRNorm  (-1)  THENA  Auto)
  THEN  (RW  IntNormC  (-1)  THENA  Auto))

---

Home Index