---

Step * of Lemma i-member-proper-iff

No Annotations
∀I:Interval. (iproper(I) ⇒ (∀r:ℝ. (r ∈ I ⇐⇒ ∃n:ℕ+. (iproper(i-approx(I;n)) ∧ (r ∈ i-approx(I;n))))))
BY
{ ((UnivCD THENA Auto)
   THEN ((InstLemma `r-strict-bound-property` [⌜r⌝])⋅ THENA Auto)
   THEN (MoveToConcl (-1))
   THEN (GenConcl ⌜(r-bound(r) + 1) = b ∈ {2...}⌝⋅ THENA Auto)
   THEN (Thin (-1))
   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 Auto
   THEN ExRepD
   THEN Auto
   THEN Try ((With ⌜b⌝ (D 0)⋅ THEN Auto THEN All (RepUR ``iproper``) THEN Complete (Auto))⋅)
   THEN Try ((UnfoldTop `iproper` (-3)
              THEN InstConcl [⌜n⌝]⋅
              THEN Auto
              THEN RWO "-2<" 0
              THEN Auto
              THEN nRNorm 0
              THEN Auto))
   THEN Try ((RepUR ``iproper`` 3
              THEN RW (AddrC [2] (SubC (TagC (mk_tag_term 9)))) 3
              THEN (D 3 THENA (RepUR ``i-finite`` 0 THEN Complete (Auto)))))) }

1
1. x1 : ℝ
2. y : ℝ
3. r : ℝ
4. b : {2...}
5. r(-b) < r
6. r < r(b)
7. x1 ≤ r
8. m : ℕ+
9. r ≤ (y - (r1/r(m)))
10. x1 < y
⊢ ∃n:ℕ+. (iproper([x1, y - (r1/r(n))]) ∧ (x1 ≤ r) ∧ (r ≤ (y - (r1/r(n)))))

2
1. y : ℝ
2. x1 : ℝ
3. r : ℝ
4. b : {2...}
5. r(-b) < r
6. r < r(b)
7. m : ℕ+
8. y ≤ (r - (r1/r(m)))
9. r ≤ x1
10. y < x1
⊢ ∃n:ℕ+. (iproper([y + (r1/r(n)), x1]) ∧ ((y + (r1/r(n))) ≤ r) ∧ (r ≤ x1))

3
1. y : ℝ
2. y1 : ℝ
3. r : ℝ
4. b : {2...}
5. r(-b) < r
6. r < r(b)
7. m1 : ℕ+
8. y ≤ (r - (r1/r(m1)))
9. m : ℕ+
10. r ≤ (y1 - (r1/r(m)))
11. y < y1
⊢ ∃n:ℕ+. (iproper([y + (r1/r(n)), y1 - (r1/r(n))]) ∧ ((y + (r1/r(n))) ≤ r) ∧ (r ≤ (y1 - (r1/r(n)))))

4
1. y : ℝ
2. y1 : Top
3. iproper(<inl (inr y ), inr y1 >)
4. r : ℝ
5. b : {2...}
6. r(-b) < r
7. r < r(b)
8. m : ℕ+
9. y ≤ (r - (r1/r(m)))
⊢ ∃n:ℕ+. (iproper([y + (r1/r(n)), r(n)]) ∧ ((y + (r1/r(n))) ≤ r) ∧ (r ≤ r(n)))

5
1. y : Top
2. y1 : ℝ
3. iproper(<inr y , inl (inr y1 )>)
4. r : ℝ
5. b : {2...}
6. r(-b) < r
7. r < r(b)
8. m : ℕ+
9. r ≤ (y1 - (r1/r(m)))
⊢ ∃n:ℕ+. (iproper([r(-n), y1 - (r1/r(n))]) ∧ (r(-n) ≤ r) ∧ (r ≤ (y1 - (r1/r(n)))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}I:Interval
    (iproper(I)  {}\mRightarrow{}  (\mforall{}r:\mBbbR{}.  (r  \mmember{}  I  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}\msupplus{}.  (iproper(i-approx(I;n))  \mwedge{}  (r  \mmember{}  i-approx(I;n))))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  ((InstLemma  `r-strict-bound-property`  [\mkleeneopen{}r\mkleeneclose{}])\mcdot{}  THENA  Auto)
  THEN  (MoveToConcl  (-1))
  THEN  (GenConcl  \mkleeneopen{}(r-bound(r)  +  1)  =  b\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  (Thin  (-1))
  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  Auto
  THEN  ExRepD
  THEN  Auto
  THEN  Try  ((With  \mkleeneopen{}b\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto  THEN  All  (RepUR  ``iproper``)  THEN  Complete  (Auto))\mcdot{})
  THEN  Try  ((UnfoldTop  `iproper`  (-3)
                        THEN  InstConcl  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
                        THEN  Auto
                        THEN  RWO  "-2<"  0
                        THEN  Auto
                        THEN  nRNorm  0
                        THEN  Auto))
  THEN  Try  ((RepUR  ``iproper``  3
                        THEN  RW  (AddrC  [2]  (SubC  (TagC  (mk\_tag\_term  9))))  3
                        THEN  (D  3  THENA  (RepUR  ``i-finite``  0  THEN  Complete  (Auto))))))

---

Home Index