---

Step * of Lemma rinv-positive

No Annotations
∀x:ℝ. ((r0 < x) ⇒ (r0 < rinv(x)))
BY
{ (Auto
   THEN (RWO "rpositive-rless" 0 THENA Auto)
   THEN DupHyp (-1)
   THEN (RWO "rpositive-rless" (-1) THENA Auto)
   THEN D -1
   THEN (BLemma `rpositive-iff` THENA Auto)) }

1
1. x : ℝ
2. r0 < x
3. n : ℕ+
4. [%6] : 4 < x n
⊢ rpositive2(rinv(x))

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  (RWO  "rpositive-rless"  0  THENA  Auto)
  THEN  DupHyp  (-1)
  THEN  (RWO  "rpositive-rless"  (-1)  THENA  Auto)
  THEN  D  -1
  THEN  (BLemma  `rpositive-iff`  THENA  Auto))

---

Home Index