---

Step * of Lemma i-member-implies

No Annotations
∀I:Interval. ∀r:ℝ.
  ((r ∈ I)
  ⇒ (∃n,M:ℕ+
       ((r ∈ i-approx(I;n))
       ∧ (∀y:{y:ℝ| y ∈ I} . ((|y - r| ≤ (r1/r(M))) ⇒ (y ∈ i-approx(I;n))))
       ∧ (iproper(I) ⇒ iproper(i-approx(I;n))))))
BY
{ (((UnivCD THENA Auto) THEN (MoveToConcl (-1)) THEN (RWO "rabs-difference-bound-rleq" 0 THENA Auto))
   THEN ((InstLemma `r-bound-property` [⌜r⌝])⋅ THENA Auto)
   THEN (MoveToConcl (-1))
   THEN (GenConclAtAddr [1; 2; 2;1])⋅
   THEN (Thin (-1))
   THEN ((RenameVar `b' (-1)) THEN (Assert r(b) < r(b + 1) BY Auto) THEN (Assert r(-(b + 1)) < r(-b) BY Auto))
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN D 1
   THEN (D 1 THENL [D 1; Id])
   THEN (D 2 THENL [D 2; Id])
   THEN RepUR ``i-approx`` 0
   THEN RepUR ``i-member`` 0
   THEN Try ((RWO "rless-iff-rleq" 0 THENA Auto))
   THEN (D 0 THENA Auto)
   THEN ExRepD
   THEN RepUR ``iproper i-finite left-endpoint right-endpoint endpoints`` 0) }

1
1. x1 : ℝ
2. x2 : ℝ
3. r : ℝ
4. b : ℕ+
5. r(b) < r(b + 1)
6. r(-(b + 1)) < r(-b)
7. r(-b) ≤ r
8. r ≤ r(b)
9. x1 ≤ r
10. r ≤ x2
⊢ ∃n,M:ℕ+
   (((x1 ≤ r) ∧ (r ≤ x2))
   ∧ (∀y:{y:ℝ| (x1 ≤ y) ∧ (y ≤ x2)} . ((((r - (r1/r(M))) ≤ y) ∧ (y ≤ (r + (r1/r(M))))) ⇒ ((x1 ≤ y) ∧ (y ≤ x2))))
   ∧ (((True ∧ True) ⇒ (x1 < x2)) ⇒ (True ∧ True) ⇒ (x1 < x2)))

2
1. x1 : ℝ
2. y : ℝ
3. r : ℝ
4. b : ℕ+
5. r(b) < r(b + 1)
6. r(-(b + 1)) < r(-b)
7. r(-b) ≤ r
8. r ≤ r(b)
9. x1 ≤ r
10. m : ℕ+
11. r ≤ (y - (r1/r(m)))
⊢ ∃n,M:ℕ+
   (((x1 ≤ r) ∧ (r ≤ (y - (r1/r(n)))))
   ∧ (∀y@0:{y@0:ℝ| (x1 ≤ y@0) ∧ (y@0 < y)} 
        ((((r - (r1/r(M))) ≤ y@0) ∧ (y@0 ≤ (r + (r1/r(M))))) ⇒ ((x1 ≤ y@0) ∧ (y@0 ≤ (y - (r1/r(n)))))))
   ∧ (((True ∧ True) ⇒ (x1 < y)) ⇒ (True ∧ True) ⇒ (x1 < (y - (r1/r(n))))))

3
1. x1 : ℝ
2. y : Top
3. r : ℝ
4. b : ℕ+
5. r(b) < r(b + 1)
6. r(-(b + 1)) < r(-b)
7. r(-b) ≤ r
8. r ≤ r(b)
9. x1 ≤ r
⊢ ∃n,M:ℕ+
   (((x1 ≤ r) ∧ (r ≤ r(n)))
   ∧ (∀y@0:{y@0:ℝ| x1 ≤ y@0} . ((((r - (r1/r(M))) ≤ y@0) ∧ (y@0 ≤ (r + (r1/r(M))))) ⇒ ((x1 ≤ y@0) ∧ (y@0 ≤ r(n)))))
   ∧ (((True ∧ False) ⇒ (x1 < case ⊥ of inl(b) => b | inr(b) => b)) ⇒ (True ∧ True) ⇒ (x1 < r(n))))

4
1. y : ℝ
2. x1 : ℝ
3. r : ℝ
4. b : ℕ+
5. r(b) < r(b + 1)
6. r(-(b + 1)) < r(-b)
7. r(-b) ≤ r
8. r ≤ r(b)
9. m : ℕ+
10. y ≤ (r - (r1/r(m)))
11. r ≤ x1
⊢ ∃n,M:ℕ+
   ((((y + (r1/r(n))) ≤ r) ∧ (r ≤ x1))
   ∧ (∀y@0:{y@0:ℝ| (y < y@0) ∧ (y@0 ≤ x1)} 
        ((((r - (r1/r(M))) ≤ y@0) ∧ (y@0 ≤ (r + (r1/r(M))))) ⇒ (((y + (r1/r(n))) ≤ y@0) ∧ (y@0 ≤ x1))))
   ∧ (((True ∧ True) ⇒ (y < x1)) ⇒ (True ∧ True) ⇒ ((y + (r1/r(n))) < x1)))

5
1. y : ℝ
2. y1 : ℝ
3. r : ℝ
4. b : ℕ+
5. r(b) < r(b + 1)
6. r(-(b + 1)) < r(-b)
7. r(-b) ≤ r
8. r ≤ r(b)
9. m1 : ℕ+
10. y ≤ (r - (r1/r(m1)))
11. m : ℕ+
12. r ≤ (y1 - (r1/r(m)))
⊢ ∃n,M:ℕ+
   ((((y + (r1/r(n))) ≤ r) ∧ (r ≤ (y1 - (r1/r(n)))))
   ∧ (∀y@0:{y@0:ℝ| (y < y@0) ∧ (y@0 < y1)} 
        ((((r - (r1/r(M))) ≤ y@0) ∧ (y@0 ≤ (r + (r1/r(M))))) ⇒ (((y + (r1/r(n))) ≤ y@0) ∧ (y@0 ≤ (y1 - (r1/r(n)))))))
   ∧ (((True ∧ True) ⇒ (y < y1)) ⇒ (True ∧ True) ⇒ ((y + (r1/r(n))) < (y1 - (r1/r(n))))))

6
1. y : ℝ
2. y1 : Top
3. r : ℝ
4. b : ℕ+
5. r(b) < r(b + 1)
6. r(-(b + 1)) < r(-b)
7. r(-b) ≤ r
8. r ≤ r(b)
9. m : ℕ+
10. y ≤ (r - (r1/r(m)))
⊢ ∃n,M:ℕ+
   ((((y + (r1/r(n))) ≤ r) ∧ (r ≤ r(n)))
   ∧ (∀y@0:{y@0:ℝ| y < y@0} 
        ((((r - (r1/r(M))) ≤ y@0) ∧ (y@0 ≤ (r + (r1/r(M))))) ⇒ (((y + (r1/r(n))) ≤ y@0) ∧ (y@0 ≤ r(n)))))
   ∧ (((True ∧ False) ⇒ (y < case ⊥ of inl(b) => b | inr(b) => b)) ⇒ (True ∧ True) ⇒ ((y + (r1/r(n))) < r(n))))

7
1. y : Top
2. x1 : ℝ
3. r : ℝ
4. b : ℕ+
5. r(b) < r(b + 1)
6. r(-(b + 1)) < r(-b)
7. r(-b) ≤ r
8. r ≤ r(b)
9. r ≤ x1
⊢ ∃n,M:ℕ+
   (((r(-n) ≤ r) ∧ (r ≤ x1))
   ∧ (∀y@0:{y@0:ℝ| y@0 ≤ x1} . ((((r - (r1/r(M))) ≤ y@0) ∧ (y@0 ≤ (r + (r1/r(M))))) ⇒ ((r(-n) ≤ y@0) ∧ (y@0 ≤ x1))))
   ∧ (((False ∧ True) ⇒ (case ⊥ of inl(a) => a | inr(a) => a < x1)) ⇒ (True ∧ True) ⇒ (r(-n) < x1)))

8
1. y : Top
2. y1 : ℝ
3. r : ℝ
4. b : ℕ+
5. r(b) < r(b + 1)
6. r(-(b + 1)) < r(-b)
7. r(-b) ≤ r
8. r ≤ r(b)
9. m : ℕ+
10. r ≤ (y1 - (r1/r(m)))
⊢ ∃n,M:ℕ+
   (((r(-n) ≤ r) ∧ (r ≤ (y1 - (r1/r(n)))))
   ∧ (∀y@0:{y@0:ℝ| y@0 < y1} 
        ((((r - (r1/r(M))) ≤ y@0) ∧ (y@0 ≤ (r + (r1/r(M))))) ⇒ ((r(-n) ≤ y@0) ∧ (y@0 ≤ (y1 - (r1/r(n)))))))
   ∧ (((False ∧ True) ⇒ (case ⊥ of inl(a) => a | inr(a) => a < y1)) ⇒ (True ∧ True) ⇒ (r(-n) < (y1 - (r1/r(n))))))

9
1. y : Top
2. y1 : Top
3. r : ℝ
4. b : ℕ+
5. r(b) < r(b + 1)
6. r(-(b + 1)) < r(-b)
7. r(-b) ≤ r
8. r ≤ r(b)
9. True
⊢ ∃n,M:ℕ+
   (((r(-n) ≤ r) ∧ (r ≤ r(n)))
   ∧ (∀y@0:{y@0:ℝ| True} . ((((r - (r1/r(M))) ≤ y@0) ∧ (y@0 ≤ (r + (r1/r(M))))) ⇒ ((r(-n) ≤ y@0) ∧ (y@0 ≤ r(n)))))
   ∧ (((False ∧ False) ⇒ (case ⊥ of inl(a) => a | inr(a) => a < case ⊥ of inl(b) => b | inr(b) => b))
     ⇒ (True ∧ True)
     ⇒ (r(-n) < r(n))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:Interval.  \mforall{}r:\mBbbR{}.
    ((r  \mmember{}  I)
    {}\mRightarrow{}  (\mexists{}n,M:\mBbbN{}\msupplus{}
              ((r  \mmember{}  i-approx(I;n))
              \mwedge{}  (\mforall{}y:\{y:\mBbbR{}|  y  \mmember{}  I\}  .  ((|y  -  r|  \mleq{}  (r1/r(M)))  {}\mRightarrow{}  (y  \mmember{}  i-approx(I;n))))
              \mwedge{}  (iproper(I)  {}\mRightarrow{}  iproper(i-approx(I;n))))))


By

---

Latex:
(((UnivCD  THENA  Auto)  THEN  (MoveToConcl  (-1))  THEN  (RWO  "rabs-difference-bound-rleq"  0  THENA  Auto))
  THEN  ((InstLemma  `r-bound-property`  [\mkleeneopen{}r\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  (MoveToConcl  (-1))
  THEN  (GenConclAtAddr  [1;  2;  2;1])\mcdot{}
  THEN  (Thin  (-1))
  THEN  ((RenameVar  `b'  (-1))
              THEN  (Assert  r(b)  <  r(b  +  1)  BY
                                      Auto)
              THEN  (Assert  r(-(b  +  1))  <  r(-b)  BY
                                      Auto))
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  D  1
  THEN  (D  1  THENL  [D  1;  Id])
  THEN  (D  2  THENL  [D  2;  Id])
  THEN  RepUR  ``i-approx``  0
  THEN  RepUR  ``i-member``  0
  THEN  Try  ((RWO  "rless-iff-rleq"  0  THENA  Auto))
  THEN  (D  0  THENA  Auto)
  THEN  ExRepD
  THEN  RepUR  ``iproper  i-finite  left-endpoint  right-endpoint  endpoints``  0)

---

Home Index