---

Step * of Lemma common-limit-midpoints

No Annotations
∀a,b:ℕ ⟶ ℝ.
  ((∀n:ℕ
      (((a[n + 1] = a[n]) ∧ (b[n + 1] = (a[n] + b[n]/r(2)))) ∨ ((a[n + 1] = (a[n] + b[n]/r(2))) ∧ (b[n + 1] = b[n]))))
  ⇒ (∃y:ℝ. (lim n→∞.a[n] = y ∧ lim n→∞.b[n] = y)))
BY
{ (Auto
   THEN (Assert ∀n:ℕ. ((r(2^n) * |a[n] - b[n]|) ≤ |a[0] - b[0]|) BY
               (InductionOnNat
                THENL [(Reduce 0 THEN nRNorm 0⋅ THEN Auto)
                      ; ((Assert |a[n] - b[n]| = (|a[n - 1] - b[n - 1]|/r(2)) BY
                                ((InstHyp [⌜n - 1⌝] 3⋅ THENA Auto)
                                 THEN (Subst' (n - 1) + 1 ~ n -1 THENA Auto)
                                 THEN (Assert r(2) = |r(2)| BY
                                             (RWO "rabs-int" 0 THEN Auto))
                                 THEN (Assert r0 < r(2) BY
                                             Auto)
                                 THEN (Assert r0 < |r(2)| BY
                                             Auto)
                                 THEN (RWO "-3" 0 THENA Auto)
                                 THEN (RWO  "rabs-rdiv<" 0 THENA Auto)
                                 THEN RepeatFor 2 (D -4)
                                 THEN (RWO  "-4 -5" 0 THENA Auto)
                                 THEN (BLemma `rabs_functionality` THENA Auto)
                                 THEN nRMul ⌜r(2)⌝ 0⋅
                                 THEN Auto))
                         THEN (RWO "-1" 0 THENA Auto)
                         THEN (Assert r(2^n) = (r(2^(n - 1)) * r(2^1)) BY
                                     (RWO  "rmul-int" 0 THEN Auto THEN RWO  "exp_add<" 0 THEN Auto))
                         THEN (RWO "exp1" (-1) THENA Auto)
                         THEN (RWO  "-1" 0 THENA Auto)
                         THEN (RWO "rmul_assoc" 0 THENA Auto)
                         THEN (RWO "-3<" 0 THENA Auto)
                         THEN GenConclTerms Auto [⌜r(2^(n - 1))⌝;⌜|a[n - 1] - b[n - 1]|⌝]⋅
                         THEN nRNorm 0
                         THEN Auto)]
               ))
   ) }

1
1. a : ℕ ⟶ ℝ
2. b : ℕ ⟶ ℝ
3. ∀n:ℕ. (((a[n + 1] = a[n]) ∧ (b[n + 1] = (a[n] + b[n]/r(2)))) ∨ ((a[n + 1] = (a[n] + b[n]/r(2))) ∧ (b[n + 1] = b[n])))
4. ∀n:ℕ. ((r(2^n) * |a[n] - b[n]|) ≤ |a[0] - b[0]|)
⊢ ∃y:ℝ. (lim n→∞.a[n] = y ∧ lim n→∞.b[n] = y)

---

Latex:

---

Latex:
No  Annotations
\mforall{}a,b:\mBbbN{}  {}\mrightarrow{}  \mBbbR{}.
    ((\mforall{}n:\mBbbN{}
            (((a[n  +  1]  =  a[n])  \mwedge{}  (b[n  +  1]  =  (a[n]  +  b[n]/r(2))))
            \mvee{}  ((a[n  +  1]  =  (a[n]  +  b[n]/r(2)))  \mwedge{}  (b[n  +  1]  =  b[n]))))
    {}\mRightarrow{}  (\mexists{}y:\mBbbR{}.  (lim  n\mrightarrow{}\minfty{}.a[n]  =  y  \mwedge{}  lim  n\mrightarrow{}\minfty{}.b[n]  =  y)))


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}n:\mBbbN{}.  ((r(2\^{}n)  *  |a[n]  -  b[n]|)  \mleq{}  |a[0]  -  b[0]|)  BY
                          (InductionOnNat
                            THENL  [(Reduce  0  THEN  nRNorm  0\mcdot{}  THEN  Auto)
                                        ;  ((Assert  |a[n]  -  b[n]|  =  (|a[n  -  1]  -  b[n  -  1]|/r(2))  BY
                                                            ((InstHyp  [\mkleeneopen{}n  -  1\mkleeneclose{}]  3\mcdot{}  THENA  Auto)
                                                              THEN  (Subst'  (n  -  1)  +  1  \msim{}  n  -1  THENA  Auto)
                                                              THEN  (Assert  r(2)  =  |r(2)|  BY
                                                                                      (RWO  "rabs-int"  0  THEN  Auto))
                                                              THEN  (Assert  r0  <  r(2)  BY
                                                                                      Auto)
                                                              THEN  (Assert  r0  <  |r(2)|  BY
                                                                                      Auto)
                                                              THEN  (RWO  "-3"  0  THENA  Auto)
                                                              THEN  (RWO    "rabs-rdiv<"  0  THENA  Auto)
                                                              THEN  RepeatFor  2  (D  -4)
                                                              THEN  (RWO    "-4  -5"  0  THENA  Auto)
                                                              THEN  (BLemma  `rabs\_functionality`  THENA  Auto)
                                                              THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  0\mcdot{}
                                                              THEN  Auto))
                                              THEN  (RWO  "-1"  0  THENA  Auto)
                                              THEN  (Assert  r(2\^{}n)  =  (r(2\^{}(n  -  1))  *  r(2\^{}1))  BY
                                                                      (RWO    "rmul-int"  0  THEN  Auto  THEN  RWO    "exp\_add<"  0  THEN  Auto))
                                              THEN  (RWO  "exp1"  (-1)  THENA  Auto)
                                              THEN  (RWO    "-1"  0  THENA  Auto)
                                              THEN  (RWO  "rmul\_assoc"  0  THENA  Auto)
                                              THEN  (RWO  "-3<"  0  THENA  Auto)
                                              THEN  GenConclTerms  Auto  [\mkleeneopen{}r(2\^{}(n  -  1))\mkleeneclose{};\mkleeneopen{}|a[n  -  1]  -  b[n  -  1]|\mkleeneclose{}]\mcdot{}
                                              THEN  nRNorm  0
                                              THEN  Auto)]
                          ))
  )

---

Home Index