---

Step * 1 1 1 1 1 1 of Lemma common-limit-midpoints


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]|)
5. ∀n,d:ℕ.
     (((r(2^n) * |a[n] - a[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |a[n] - b[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |b[n] - a[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |b[n] - b[n + d]|) ≤ |a[0] - b[0]|))
6. k : ℕ+
7. n : ℕ
8. r(-n) ≤ |a[0] - b[0]|
9. |a[0] - b[0]| ≤ r(n)
10. (k * (n + 1)) ≤ 2^log(2;k * (n + 1))
11. j : ℕ
12. m : ℕ
13. log(2;k * (n + 1)) ≤ j
14. log(2;k * (n + 1)) ≤ m
15. ((k * (n + 1)) ≤ 2^j) ∧ ((k * (n + 1)) ≤ 2^m)
⊢ |a[j] - a[m]| ≤ (r1/r(k))
BY
{ ((Decide ⌜j ≤ m⌝⋅ THENA Auto)
   THENL [((Assert (r(2^j) * |a[j] - a[j + (m - j)]|) ≤ |a[0] - b[0]| BY
                  Auto)
           THEN (Subst' j + (m - j) ~ m -1 THENA Auto)
           THEN MoveToConcl (-1)
           THEN MoveToConcl 9
           THEN GenConclTerms Auto [⌜a[j] - a[m]⌝;⌜a[0] - b[0]⌝]⋅)
         ; ((Assert (r(2^m) * |a[m] - a[m + (j - m)]|) ≤ |a[0] - b[0]| BY
                   Auto)
            THEN (Subst' m + (j - m) ~ j -1 THENA Auto)
            THEN (RWO "rabs-difference-symmetry" 0 THENA Auto)
            THEN MoveToConcl (-1)
            THEN MoveToConcl 9
            THEN GenConclTerms Auto [⌜a[m] - a[j]⌝;⌜a[0] - b[0]⌝]⋅)]
) }

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]|)
5. ∀n,d:ℕ.
     (((r(2^n) * |a[n] - a[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |a[n] - b[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |b[n] - a[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |b[n] - b[n + d]|) ≤ |a[0] - b[0]|))
6. k : ℕ+
7. n : ℕ
8. r(-n) ≤ |a[0] - b[0]|
9. (k * (n + 1)) ≤ 2^log(2;k * (n + 1))
10. j : ℕ
11. m : ℕ
12. log(2;k * (n + 1)) ≤ j
13. log(2;k * (n + 1)) ≤ m
14. ((k * (n + 1)) ≤ 2^j) ∧ ((k * (n + 1)) ≤ 2^m)
15. j ≤ m
16. v : ℝ
17. (a[j] - a[m]) = v ∈ ℝ
18. v1 : ℝ
19. (a[0] - b[0]) = v1 ∈ ℝ
⊢ (|v1| ≤ r(n)) ⇒ ((r(2^j) * |v|) ≤ |v1|) ⇒ (|v| ≤ (r1/r(k)))

2
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]|)
5. ∀n,d:ℕ.
     (((r(2^n) * |a[n] - a[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |a[n] - b[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |b[n] - a[n + d]|) ≤ |a[0] - b[0]|)
     ∧ ((r(2^n) * |b[n] - b[n + d]|) ≤ |a[0] - b[0]|))
6. k : ℕ+
7. n : ℕ
8. r(-n) ≤ |a[0] - b[0]|
9. (k * (n + 1)) ≤ 2^log(2;k * (n + 1))
10. j : ℕ
11. m : ℕ
12. log(2;k * (n + 1)) ≤ j
13. log(2;k * (n + 1)) ≤ m
14. ((k * (n + 1)) ≤ 2^j) ∧ ((k * (n + 1)) ≤ 2^m)
15. ¬(j ≤ m)
16. v : ℝ
17. (a[m] - a[j]) = v ∈ ℝ
18. v1 : ℝ
19. (a[0] - b[0]) = v1 ∈ ℝ
⊢ (|v1| ≤ r(n)) ⇒ ((r(2^m) * |v|) ≤ |v1|) ⇒ (|v| ≤ (r1/r(k)))

---

Latex:

---

Latex:

1.  a  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
2.  b  :  \mBbbN{}  {}\mrightarrow{}  \mBbbR{}
3.  \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])))
4.  \mforall{}n:\mBbbN{}.  ((r(2\^{}n)  *  |a[n]  -  b[n]|)  \mleq{}  |a[0]  -  b[0]|)
5.  \mforall{}n,d:\mBbbN{}.
          (((r(2\^{}n)  *  |a[n]  -  a[n  +  d]|)  \mleq{}  |a[0]  -  b[0]|)
          \mwedge{}  ((r(2\^{}n)  *  |a[n]  -  b[n  +  d]|)  \mleq{}  |a[0]  -  b[0]|)
          \mwedge{}  ((r(2\^{}n)  *  |b[n]  -  a[n  +  d]|)  \mleq{}  |a[0]  -  b[0]|)
          \mwedge{}  ((r(2\^{}n)  *  |b[n]  -  b[n  +  d]|)  \mleq{}  |a[0]  -  b[0]|))
6.  k  :  \mBbbN{}\msupplus{}
7.  n  :  \mBbbN{}
8.  r(-n)  \mleq{}  |a[0]  -  b[0]|
9.  |a[0]  -  b[0]|  \mleq{}  r(n)
10.  (k  *  (n  +  1))  \mleq{}  2\^{}log(2;k  *  (n  +  1))
11.  j  :  \mBbbN{}
12.  m  :  \mBbbN{}
13.  log(2;k  *  (n  +  1))  \mleq{}  j
14.  log(2;k  *  (n  +  1))  \mleq{}  m
15.  ((k  *  (n  +  1))  \mleq{}  2\^{}j)  \mwedge{}  ((k  *  (n  +  1))  \mleq{}  2\^{}m)
\mvdash{}  |a[j]  -  a[m]|  \mleq{}  (r1/r(k))


By

---

Latex:
((Decide  \mkleeneopen{}j  \mleq{}  m\mkleeneclose{}\mcdot{}  THENA  Auto)
  THENL  [((Assert  (r(2\^{}j)  *  |a[j]  -  a[j  +  (m  -  j)]|)  \mleq{}  |a[0]  -  b[0]|  BY
                                Auto)
                  THEN  (Subst'  j  +  (m  -  j)  \msim{}  m  -1  THENA  Auto)
                  THEN  MoveToConcl  (-1)
                  THEN  MoveToConcl  9
                  THEN  GenConclTerms  Auto  [\mkleeneopen{}a[j]  -  a[m]\mkleeneclose{};\mkleeneopen{}a[0]  -  b[0]\mkleeneclose{}]\mcdot{})
              ;  ((Assert  (r(2\^{}m)  *  |a[m]  -  a[m  +  (j  -  m)]|)  \mleq{}  |a[0]  -  b[0]|  BY
                                  Auto)
                    THEN  (Subst'  m  +  (j  -  m)  \msim{}  j  -1  THENA  Auto)
                    THEN  (RWO  "rabs-difference-symmetry"  0  THENA  Auto)
                    THEN  MoveToConcl  (-1)
                    THEN  MoveToConcl  9
                    THEN  GenConclTerms  Auto  [\mkleeneopen{}a[m]  -  a[j]\mkleeneclose{};\mkleeneopen{}a[0]  -  b[0]\mkleeneclose{}]\mcdot{})]
)

---

Home Index