---

Step * of Lemma rinv_functionality-tst

No Annotations
∀[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))⋅) }

---

Latex:

---

Latex:
No  Annotations
\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