Step
*
of Lemma
case-real3-req1
∀[f:ℕ+ ⟶ 𝔹]
  ∀[b,a:ℝ].  case-real3(a;b;f) = a supposing ∀n,m:ℕ+.  ((↑(f n)) 
⇒ (¬↑(f m)) 
⇒ (|(a m) - b m| ≤ 4)) 
  supposing ∃n:ℕ+. (↑(f n))
BY
{ (((Auto THEN ExRepD) THEN BLemma `req-iff-bdd-diff`)
   THEN Auto
   THEN (Assert bdd-diff(case-real3(a;b;f);case-real3-seq(a;b;f)) BY
               (Unfold `case-real3` 0 THEN Auto))
   THEN (RWO "-1" 0 THENA Auto)
   THEN (BLemma `bdd-diff_inversion` THENA Auto)
   THEN D 0 With ⌜4⌝ 
   THEN Auto
   THEN RepUR ``case-real3-seq`` 0
   THEN AutoSplit
   THEN RW IntNormC 0
   THEN Auto) }
Latex:
Latex:
\mforall{}[f:\mBbbN{}\msupplus{}  {}\mrightarrow{}  \mBbbB{}]
    \mforall{}[b,a:\mBbbR{}].
        case-real3(a;b;f)  =  a  supposing  \mforall{}n,m:\mBbbN{}\msupplus{}.    ((\muparrow{}(f  n))  {}\mRightarrow{}  (\mneg{}\muparrow{}(f  m))  {}\mRightarrow{}  (|(a  m)  -  b  m|  \mleq{}  4)) 
    supposing  \mexists{}n:\mBbbN{}\msupplus{}.  (\muparrow{}(f  n))
By
Latex:
(((Auto  THEN  ExRepD)  THEN  BLemma  `req-iff-bdd-diff`)
  THEN  Auto
  THEN  (Assert  bdd-diff(case-real3(a;b;f);case-real3-seq(a;b;f))  BY
                          (Unfold  `case-real3`  0  THEN  Auto))
  THEN  (RWO  "-1"  0  THENA  Auto)
  THEN  (BLemma  `bdd-diff\_inversion`  THENA  Auto)
  THEN  D  0  With  \mkleeneopen{}4\mkleeneclose{} 
  THEN  Auto
  THEN  RepUR  ``case-real3-seq``  0
  THEN  AutoSplit
  THEN  RW  IntNormC  0
  THEN  Auto)
Home
Index