---

Step * of Lemma i-member-iff

No Annotations
∀I:Interval. ∀r:ℝ.  (r ∈ I ⇐⇒ ∃n:ℕ+. (r ∈ i-approx(I;n)))
BY
{ ((UnivCD 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 (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 ((InstConcl [⌜b⌝] ⋅ THEN Complete (Auto))⋅)
   THEN Try ((InstConcl [⌜m⌝]⋅ THEN Auto THEN RWO "-2 -2<" 0 THEN Auto THEN nRNorm 0 THEN Complete (Auto)))
   THEN Try ((InstConcl [⌜n⌝]⋅ THEN Auto THEN RWO "-2 -2<" 0 THEN Auto THEN nRNorm 0 THEN Complete (Auto)))) }

1
1. y : ℝ
2. y1 : ℝ
3. r : ℝ
4. b : ℕ+
5. r(-b) ≤ r
6. r ≤ r(b)
7. m1 : ℕ+
8. y ≤ (r - (r1/r(m1)))
9. m : ℕ+
10. r ≤ (y1 - (r1/r(m)))
⊢ ∃n:ℕ+. (((y + (r1/r(n))) ≤ r) ∧ (r ≤ (y1 - (r1/r(n)))))

2
1. y : ℝ
2. y1 : Top
3. r : ℝ
4. b : ℕ+
5. r(-b) ≤ r
6. r ≤ r(b)
7. m : ℕ+
8. y ≤ (r - (r1/r(m)))
⊢ ∃n:ℕ+. (((y + (r1/r(n))) ≤ r) ∧ (r ≤ r(n)))

3
1. y : Top
2. y1 : ℝ
3. r : ℝ
4. b : ℕ+
5. r(-b) ≤ r
6. r ≤ r(b)
7. m : ℕ+
8. r ≤ (y1 - (r1/r(m)))
⊢ ∃n:ℕ+. ((r(-n) ≤ r) ∧ (r ≤ (y1 - (r1/r(n)))))

---

Latex:

---

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


By

---

Latex:
((UnivCD  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  (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  ((InstConcl  [\mkleeneopen{}b\mkleeneclose{}]  \mcdot{}  THEN  Complete  (Auto))\mcdot{})
  THEN  Try  ((InstConcl  [\mkleeneopen{}m\mkleeneclose{}]\mcdot{}
                        THEN  Auto
                        THEN  RWO  "-2  -2<"  0
                        THEN  Auto
                        THEN  nRNorm  0
                        THEN  Complete  (Auto)))
  THEN  Try  ((InstConcl  [\mkleeneopen{}n\mkleeneclose{}]\mcdot{}
                        THEN  Auto
                        THEN  RWO  "-2  -2<"  0
                        THEN  Auto
                        THEN  nRNorm  0
                        THEN  Complete  (Auto))))

---

Home Index