---

Step * 1 of Lemma derivative-rinv-basic

.....antecedent..... 
x≠r0 for x ∈ (r0, ∞)
BY
{ (D 0 THEN Auto) }

1
1. m : {m:ℕ+| icompact(i-approx((r0, ∞);m))} @i
⊢ ∃c:ℝ [((r0 < c) ∧ (∀x:ℝ. ((x ∈ i-approx((r0, ∞);m)) ⇒ (c ≤ |x|))))]

---

Latex:

---

Latex:
.....antecedent..... 
x\mneq{}r0  for  x  \mmember{}  (r0,  \minfty{})


By

---

Latex:
(D  0  THEN  Auto)

---

Home Index