---

Step * 1 of Lemma rmul-rinv1


1. x : ℝ
2. ∃n:ℕ+. 4 < |x n|
⊢ bdd-diff(reg-seq-mul(x;eval n = mu-ge(λn.4 <z |x n|;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 );r1)
BY
{ ((Assert ∃n:{1...}. (↑4 <z |x n|) BY
          (ExRepD THEN With ⌜n⌝ (D 0)⋅ THEN Auto))
   THEN (InstLemma `mu-ge-property` [⌜1⌝;⌜λn.4 <z |x n|⌝]⋅ THENA Auto)
   THEN Reduce (-1)
   THEN MoveToConcl (-1)
   THEN (GenConclTerm ⌜mu-ge(λn.4 <z |x n|;1)⌝⋅ THENA Auto)
   THEN RepeatFor 2 (Thin 2)
   THEN RenameVar `a' 2
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN (RW assert_pushdownC (-2) THENA Auto)
   THEN ((Assert ∀[i:ℕ+a]. (¬4 < |x i|) BY (ParallelLast THEN RW assert_pushdownC (-1) THEN Auto)) THEN Thin (-2))
   THEN (InstLemma `rnonzero-lemma1` [⌜x⌝;⌜a⌝]⋅ THEN Auto)
   THEN (CallByValueReduce 0 THENA Auto)
   THEN AutoSplit)⋅ }

1
1. x : ℝ
2. a : {1...}
3. mu-ge(λn.4 <z |x n|;1) = a ∈ {1...}
4. 4 < |x a|
5. ∀[i:ℕ+a]. (¬4 < |x i|)
6. ∀m:ℕ+. ((a ≤ m) ⇒ (m ≤ (a * |x m|)))
7. a = 1 ∈ ℤ
⊢ bdd-diff(reg-seq-mul(x;accelerate(5;reg-seq-inv(x)));r1)

2
1. x : ℝ
2. a : {2...}
3. mu-ge(λn.4 <z |x n|;1) = a ∈ {1...}
4. 4 < |x a|
5. ∀[i:ℕ+a]. (¬4 < |x i|)
6. ∀m:ℕ+. ((a ≤ m) ⇒ (m ≤ (a * |x m|)))
⊢ bdd-diff(reg-seq-mul(x;accelerate(4 * ((4 * a * a) + 1);reg-seq-inv(reg-seq-adjust(a;x))));r1)

---

Latex:

---

Latex:

1.  x  :  \mBbbR{}
2.  \mexists{}n:\mBbbN{}\msupplus{}.  4  <  |x  n|
\mvdash{}  bdd-diff(reg-seq-mul(x;eval  n  =  mu-ge(\mlambda{}n.4  <z  |x  n|;1)  in
                                                  if  (n  =\msubz{}  1)
                                                  then  accelerate(5;reg-seq-inv(x))
                                                  else  accelerate(4  *  ((4  *  n  *  n)  +  1);reg-seq-inv(reg-seq-adjust(n;x)))
                                                  fi  );r1)


By

---

Latex:
((Assert  \mexists{}n:\{1...\}.  (\muparrow{}4  <z  |x  n|)  BY
                (ExRepD  THEN  With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto))
  THEN  (InstLemma  `mu-ge-property`  [\mkleeneopen{}1\mkleeneclose{};\mkleeneopen{}\mlambda{}n.4  <z  |x  n|\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  Reduce  (-1)
  THEN  MoveToConcl  (-1)
  THEN  (GenConclTerm  \mkleeneopen{}mu-ge(\mlambda{}n.4  <z  |x  n|;1)\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  RepeatFor  2  (Thin  2)
  THEN  RenameVar  `a'  2
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  (RW  assert\_pushdownC  (-2)  THENA  Auto)
  THEN  ((Assert  \mforall{}[i:\mBbbN{}\msupplus{}a].  (\mneg{}4  <  |x  i|)  BY
                            (ParallelLast  THEN  RW  assert\_pushdownC  (-1)  THEN  Auto))
              THEN  Thin  (-2)
              )
  THEN  (InstLemma  `rnonzero-lemma1`  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THEN  Auto)
  THEN  (CallByValueReduce  0  THENA  Auto)
  THEN  AutoSplit)\mcdot{}

---

Home Index