---

Step * 1 of Lemma rinv-positive


1. x : ℝ
2. r0 < x
3. n : ℕ+
4. [%6] : 4 < x n
⊢ rpositive2(rinv(x))
BY
{ (Unfold `rinv` 0
   THEN (Assert ∃m:{1...}. (↑((λn.eval k = x n in 4 <z |k|) m)) BY
               (Reduce 0 THEN With ⌜n⌝ (D 0)⋅ THEN Auto THEN CallByValueReduce 0 THEN Auto))
   THEN (FLemma `mu-ge-property` [-1] THENA Auto)
   THEN Reduce (-1)
   THEN MoveToConcl (-1)
   THEN (GenConcl ⌜mu-ge(λn.eval k = x n in 4 <z |k|;1) = a ∈ ℕ+⌝⋅ THENA Auto)
   THEN ThinVar `n'⋅
   THEN Thin (-1)
   THEN Reduce 0
   THEN Auto
   THEN ((CallByValueReduce (-2) THENA Auto)
         THEN (RW assert_pushdownC (-2) THENA Auto)
         THEN InstLemma `rnonzero-lemma1` [⌜x⌝;⌜a⌝]⋅
         THEN Auto
         THEN (Assert ∀[i:ℕ+a]. (|x i| ≤ 4) BY
                     (ParallelOp -2
                      THEN (CallByValueReduce (-1)⋅ THENA Auto)
                      THEN RW assert_pushdownC (-1)
                      THEN Auto
                      THEN Unhide
                      THEN Auto))⋅
         THEN Thin (-3))
   THEN (CallByValueReduce 0 THENA Auto)⋅
   THEN AutoSplit) }

1
1. x : ℝ
2. r0 < x
3. ∃m:{1...}. (↑((λn.eval k = x n in 4 <z |k|) m))
4. a : ℕ+
5. 4 < |x a|
6. ∀m:ℕ+. ((a ≤ m) ⇒ (m ≤ (a * |x m|)))
7. ∀[i:ℕ+a]. (|x i| ≤ 4)
8. a = 1 ∈ ℤ
⊢ rpositive2(accelerate(5;reg-seq-inv(x)))

2
1. x : ℝ
2. r0 < x
3. ∃m:{1...}. (↑((λn.eval k = x n in 4 <z |k|) m))
4. a : ℕ+
5. a ≠ 1
6. 4 < |x a|
7. ∀m:ℕ+. ((a ≤ m) ⇒ (m ≤ (a * |x m|)))
8. ∀[i:ℕ+a]. (|x i| ≤ 4)
⊢ rpositive2(accelerate(4 * ((4 * a * a) + 1);reg-seq-inv(reg-seq-adjust(a;x))))

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  r0  <  x
3.  n  :  \mBbbN{}\msupplus{}
4.  [\%6]  :  4  <  x  n
\mvdash{}  rpositive2(rinv(x))


By

---

Latex:
(Unfold  `rinv`  0
  THEN  (Assert  \mexists{}m:\{1...\}.  (\muparrow{}((\mlambda{}n.eval  k  =  x  n  in  4  <z  |k|)  m))  BY
                          (Reduce  0  THEN  With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  CallByValueReduce  0  THEN  Auto))
  THEN  (FLemma  `mu-ge-property`  [-1]  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  MoveToConcl  (-1)
  THEN  (GenConcl  \mkleeneopen{}mu-ge(\mlambda{}n.eval  k  =  x  n  in  4  <z  |k|;1)  =  a\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  ThinVar  `n'\mcdot{}
  THEN  Thin  (-1)
  THEN  Reduce  0
  THEN  Auto
  THEN  ((CallByValueReduce  (-2)  THENA  Auto)
              THEN  (RW  assert\_pushdownC  (-2)  THENA  Auto)
              THEN  InstLemma  `rnonzero-lemma1`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}
              THEN  Auto
              THEN  (Assert  \mforall{}[i:\mBbbN{}\msupplus{}a].  (|x  i|  \mleq{}  4)  BY
                                      (ParallelOp  -2
                                        THEN  (CallByValueReduce  (-1)\mcdot{}  THENA  Auto)
                                        THEN  RW  assert\_pushdownC  (-1)
                                        THEN  Auto
                                        THEN  Unhide
                                        THEN  Auto))\mcdot{}
              THEN  Thin  (-3))
  THEN  (CallByValueReduce  0  THENA  Auto)\mcdot{}
  THEN  AutoSplit)

---

Home Index