---

Step * 2 1 1 of Lemma iproper-approx


1. I : Interval
2. iproper(I)
3. n : ℕ+
4. left-endpoint(i-approx(I;n)) ≤ right-endpoint(i-approx(I;n))
5. (r1/r(n + 1)) < (r1/r(n))
6. r(n) < r(n + 1)
⊢ iproper(i-approx(I;n + 1))
BY
{ ((D 0 THENA Auto)
   THEN D 1
   THEN D 2
   THEN D 1
   THEN All (RepUR ``i-approx``)⋅
   THEN ((DVar `x' THEN All Reduce) ORELSE Auto)
   THEN Try ((DVar `x1'
              THEN All
               (RepUR  ``iproper left-endpoint right-endpoint endpoints i-finite ``)⋅
              THEN All
              Reduce⋅))) }

1
1. x : ℝ
2. x2 : ℝ
3. (True ∧ True) ⇒ (x < x2)
4. n : ℕ+
5. x ≤ x2
6. (r1/r(n + 1)) < (r1/r(n))
7. r(n) < r(n + 1)
8. True ∧ True
⊢ x < x2

2
1. y : ℝ
2. x2 : ℝ
3. (True ∧ True) ⇒ (y < x2)
4. n : ℕ+
5. (y + (r1/r(n))) ≤ x2
6. (r1/r(n + 1)) < (r1/r(n))
7. r(n) < r(n + 1)
8. True ∧ True
⊢ (y + (r1/r(n + 1))) < x2

3
1. x : ℝ
2. y : ℝ
3. (True ∧ True) ⇒ (x < y)
4. n : ℕ+
5. x ≤ (y - (r1/r(n)))
6. (r1/r(n + 1)) < (r1/r(n))
7. r(n) < r(n + 1)
8. True ∧ True
⊢ x < (y - (r1/r(n + 1)))

4
1. y1 : ℝ
2. y : ℝ
3. (True ∧ True) ⇒ (y1 < y)
4. n : ℕ+
5. (y1 + (r1/r(n))) ≤ (y - (r1/r(n)))
6. (r1/r(n + 1)) < (r1/r(n))
7. r(n) < r(n + 1)
8. True ∧ True
⊢ (y1 + (r1/r(n + 1))) < (y - (r1/r(n + 1)))

5
1. y : Top
2. x1 : ℕ+ ⟶ ℤ
3. [%10] : regular-seq(x1)
4. (False ∧ True) ⇒ (case ⊥ of inl(a) => a | inr(a) => a < x1)
5. n : ℕ+
6. r(-n) ≤ x1
7. (r1/r(n + 1)) < (r1/r(n))
8. r(n) < r(n + 1)
9. True ∧ True
⊢ r(-(n + 1)) < x1

6
1. y : Top
2. y1 : ℝ
3. iproper(<inr y , inl (inr y1 )>)
4. n : ℕ+
5. r(-n) ≤ (y1 - (r1/r(n)))
6. (r1/r(n + 1)) < (r1/r(n))
7. r(n) < r(n + 1)
8. i-finite([r(-(n + 1)), y1 - (r1/r(n + 1))])
⊢ r(-(n + 1)) < (y1 - (r1/r(n + 1)))

7
1. x1 : ℕ+ ⟶ ℤ
2. [%10] : regular-seq(x1)
3. y : Top
4. (True ∧ False) ⇒ (x1 < case ⊥ of inl(b) => b | inr(b) => b)
5. n : ℕ+
6. x1 ≤ r(n)
7. (r1/r(n + 1)) < (r1/r(n))
8. r(n) < r(n + 1)
9. True ∧ True
⊢ x1 < r(n + 1)

8
1. y1 : ℝ
2. y : Top
3. iproper(<inl (inr y1 ), inr y >)
4. n : ℕ+
5. (y1 + (r1/r(n))) ≤ r(n)
6. (r1/r(n + 1)) < (r1/r(n))
7. r(n) < r(n + 1)
8. i-finite([y1 + (r1/r(n + 1)), r(n + 1)])
⊢ (y1 + (r1/r(n + 1))) < r(n + 1)

---

Latex:

---

Latex:

1.  I  :  Interval
2.  iproper(I)
3.  n  :  \mBbbN{}\msupplus{}
4.  left-endpoint(i-approx(I;n))  \mleq{}  right-endpoint(i-approx(I;n))
5.  (r1/r(n  +  1))  <  (r1/r(n))
6.  r(n)  <  r(n  +  1)
\mvdash{}  iproper(i-approx(I;n  +  1))


By

---

Latex:
((D  0  THENA  Auto)
  THEN  D  1
  THEN  D  2
  THEN  D  1
  THEN  All  (RepUR  ``i-approx``)\mcdot{}
  THEN  ((DVar  `x'  THEN  All  Reduce)  ORELSE  Auto)
  THEN  Try  ((DVar  `x1'
                        THEN  All
                          (RepUR    ``iproper  left-endpoint  right-endpoint  endpoints  i-finite  ``)\mcdot{}
                        THEN  All
                        Reduce\mcdot{})))

---

Home Index