---

Step * of Lemma rinv_functionality

∀[x,y:ℝ].  (rnonzero(x) ⇒ (x = y) ⇒ (rinv(x) = rinv(y)))
BY
{ (InstLemma `rnonzero_functionality` []
   THEN RepeatFor 2 (ParallelLast')
   THEN Auto
   THEN Thin (-2)
   THEN (BLemma `req-iff-bdd-diff`  THENA Auto)
   THEN D 3
   THEN UnfoldTopAb (-1)
   THEN Unfold `rinv` 0
   THEN All (Unfold `rnonzero`)
   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 (ExRepD THENA Auto)
         THEN (Assert ∃m:{1...}. (↑((λn.eval k = y 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 = y n in 4 <z |k|;1) = b ∈ ℕ+⌝⋅ THENA Auto)
         THEN ThinVar `n'⋅
         THEN (ExRepD THENA Auto))⋅) }

1
1. x : ℝ
2. y : ℝ
3. x = y
4. m : {1...}
5. ↑((λn.eval k = x n in 4 <z |k|) m)
6. a : ℕ+
7. mu-ge(λn.eval k = x n in 4 <z |k|;1) = a ∈ ℕ+
8. ↑eval k = x a in
    4 <z |k|
9. ∀[i:ℕ+a]. (¬↑eval k = x i in 4 <z |k|)
10. m1 : {1...}
11. ↑((λn.eval k = y n in 4 <z |k|) m1)
12. b : ℕ+
13. mu-ge(λn.eval k = y n in 4 <z |k|;1) = b ∈ ℕ+
14. ↑eval k = y b in
     4 <z |k|
15. ∀[i:ℕ+b]. (¬↑eval k = y i in 4 <z |k|)
⊢ bdd-diff(eval n = a 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 ;eval n = b in
               if (n =z 1)
               then accelerate(5;reg-seq-inv(y))
               else accelerate(4 * ((4 * n * n) + 1);reg-seq-inv(reg-seq-adjust(n;y)))
               fi )

---

Latex:

---

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


By

---

Latex:
(InstLemma  `rnonzero\_functionality`  []
  THEN  RepeatFor  2  (ParallelLast')
  THEN  Auto
  THEN  Thin  (-2)
  THEN  (BLemma  `req-iff-bdd-diff`    THENA  Auto)
  THEN  D  3
  THEN  UnfoldTopAb  (-1)
  THEN  Unfold  `rinv`  0
  THEN  All  (Unfold  `rnonzero`)
  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  (ExRepD  THENA  Auto)
              THEN  (Assert  \mexists{}m:\{1...\}.  (\muparrow{}((\mlambda{}n.eval  k  =  y  n  in  4  <z  |k|)  m))  BY
                                      (Reduce  0  THEN  With  \mkleeneopen{}n\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  CallByValueReduce  0  THEN  Auto))\mcdot{}
              THEN  (FLemma  `mu-ge-property`  [-1]  THENA  Auto)
              THEN  Reduce  (-1)
              THEN  MoveToConcl  (-1)
              THEN  (GenConcl  \mkleeneopen{}mu-ge(\mlambda{}n.eval  k  =  y  n  in  4  <z  |k|;1)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  ThinVar  `n'\mcdot{}
              THEN  (ExRepD  THENA  Auto))\mcdot{})

---

Home Index