---

Step * of Lemma rinv_wf

∀[x:ℝ]. (rnonzero(x) ⇒ (rinv(x) ∈ ℝ))
BY
{ (Auto
   THEN (Unfold `rinv` 0 THEN Unfold `rnonzero` -1)
   THEN Assert ⌜mu-ge(λn.eval k = x n in 4 <z |k|;1) = mu-ge(λn.4 <z |x n|;1) ∈ {1...}⌝⋅) }

1
.....assertion..... 
1. x : ℝ
2. ∃n:ℕ+. 4 < |x n|
⊢ mu-ge(λn.eval k = x n in 4 <z |k|;1) = mu-ge(λn.4 <z |x n|;1) ∈ {1...}

2
1. x : ℝ
2. ∃n:ℕ+. 4 < |x n|
3. mu-ge(λn.eval k = x n in 4 <z |k|;1) = mu-ge(λn.4 <z |x n|;1) ∈ {1...}
⊢ eval n = mu-ge(λn.eval k = x n in
                    4 <z |k|;1) in
  if (n =z 1)
  then accelerate(5;reg-seq-inv(x))
  else accelerate(4 * ((4 * n * n) + 1);reg-seq-inv(reg-seq-adjust(n;x)))
  fi  ∈ ℝ

---

Latex:

---

Latex:
\mforall{}[x:\mBbbR{}].  (rnonzero(x)  {}\mRightarrow{}  (rinv(x)  \mmember{}  \mBbbR{}))


By

---

Latex:
(Auto
  THEN  (Unfold  `rinv`  0  THEN  Unfold  `rnonzero`  -1)
  THEN  Assert  \mkleeneopen{}mu-ge(\mlambda{}n.eval  k  =  x  n  in  4  <z  |k|;1)  =  mu-ge(\mlambda{}n.4  <z  |x  n|;1)\mkleeneclose{}\mcdot{})

---

Home Index