---

Step * 1 of Lemma dense-in-interval-implies

.....assertion..... 
1. I : Interval
2. [X] : {a:ℝ| a ∈ I}  ⟶ ℙ
3. dense-in-interval(I;X)
4. a : {a:ℝ| a ∈ I} 
5. ∃b:{b:ℝ| b ∈ I} . ((X b) ∧ b ≠ a)
⊢ ∀b:{b:ℝ| (b ∈ I) ∧ b ≠ a} . ∃c:{c:ℝ| (c ∈ I) ∧ c ≠ a} . ((X c) ∧ (|c - a| ≤ ((r1/r(2)) * |b - a|)))
BY
{ ((Thin (-1) THEN Auto)
   THEN (Assert b ≠ a BY
               (D -1 THEN Unhide THEN Auto))
   THEN UnfoldTopAb 3
   THEN (D -1
         THENL [((InstLemma `ravg-between` [⌜b⌝;⌜a⌝]⋅ THENA Auto)
                 THEN (InstLemma `i-member-between` [⌜I⌝;⌜b⌝;⌜a⌝;⌜ravg(b;a)⌝]⋅ THENA Auto)
                 THEN D -2
                 THEN (FHyp 3 [-2] THENA Auto))
               ; ((InstLemma `ravg-between` [⌜a⌝;⌜b⌝]⋅ THENA Auto)
                  THEN (InstLemma `i-member-between` [⌜I⌝;⌜a⌝;⌜b⌝;⌜ravg(a;b)⌝]⋅ THENA Auto)
                  THEN D -2
                  THEN (FHyp 3 [-3] THENA Auto))]
   )
   THEN ParallelLast
   THEN Auto) }

1
1. I : Interval
2. X : {a:ℝ| a ∈ I}  ⟶ ℙ
3. ∀a,b:{r:ℝ| r ∈ I} .  ((a < b) ⇒ (∃x:ℝ. ((X x) ∧ (a < x) ∧ (x < b))))
4. a : {a:ℝ| a ∈ I} 
5. b : {b:ℝ| (b ∈ I) ∧ b ≠ a} 
6. b < a
7. b < ravg(b;a)
8. ravg(b;a) < a
9. ravg(b;a) ∈ I
10. x : ℝ
11. X x
12. ravg(b;a) < x
13. x < a
⊢ x ∈ {c:ℝ| (c ∈ I) c∧ c ≠ a} 

2
1. I : Interval
2. [X] : {a:ℝ| a ∈ I}  ⟶ ℙ
3. ∀a,b:{r:ℝ| r ∈ I} .  ((a < b) ⇒ (∃x:ℝ. ((X x) ∧ (a < x) ∧ (x < b))))
4. a : {a:ℝ| a ∈ I} 
5. b : {b:ℝ| (b ∈ I) ∧ b ≠ a} 
6. b < a
7. b < ravg(b;a)
8. ravg(b;a) < a
9. ravg(b;a) ∈ I
10. x : ℝ
11. X x
12. ravg(b;a) < x
13. x < a
14. X x
⊢ |x - a| ≤ ((r1/r(2)) * |b - a|)

3
1. I : Interval
2. X : {a:ℝ| a ∈ I}  ⟶ ℙ
3. ∀a,b:{r:ℝ| r ∈ I} .  ((a < b) ⇒ (∃x:ℝ. ((X x) ∧ (a < x) ∧ (x < b))))
4. a : {a:ℝ| a ∈ I} 
5. b : {b:ℝ| (b ∈ I) ∧ b ≠ a} 
6. a < b
7. a < ravg(a;b)
8. ravg(a;b) < b
9. ravg(a;b) ∈ I
10. x : ℝ
11. X x
12. a < x
13. x < ravg(a;b)
⊢ x ∈ {c:ℝ| (c ∈ I) c∧ c ≠ a} 

4
1. I : Interval
2. [X] : {a:ℝ| a ∈ I}  ⟶ ℙ
3. ∀a,b:{r:ℝ| r ∈ I} .  ((a < b) ⇒ (∃x:ℝ. ((X x) ∧ (a < x) ∧ (x < b))))
4. a : {a:ℝ| a ∈ I} 
5. b : {b:ℝ| (b ∈ I) ∧ b ≠ a} 
6. a < b
7. a < ravg(a;b)
8. ravg(a;b) < b
9. ravg(a;b) ∈ I
10. x : ℝ
11. X x
12. a < x
13. x < ravg(a;b)
14. X x
⊢ |x - a| ≤ ((r1/r(2)) * |b - a|)

---

Latex:

---

Latex:
.....assertion..... 
1.  I  :  Interval
2.  [X]  :  \{a:\mBbbR{}|  a  \mmember{}  I\}    {}\mrightarrow{}  \mBbbP{}
3.  dense-in-interval(I;X)
4.  a  :  \{a:\mBbbR{}|  a  \mmember{}  I\} 
5.  \mexists{}b:\{b:\mBbbR{}|  b  \mmember{}  I\}  .  ((X  b)  \mwedge{}  b  \mneq{}  a)
\mvdash{}  \mforall{}b:\{b:\mBbbR{}|  (b  \mmember{}  I)  \mwedge{}  b  \mneq{}  a\}  .  \mexists{}c:\{c:\mBbbR{}|  (c  \mmember{}  I)  \mwedge{}  c  \mneq{}  a\}  .  ((X  c)  \mwedge{}  (|c  -  a|  \mleq{}  ((r1/r(2))  *  |b  -  a|))\000C)


By

---

Latex:
((Thin  (-1)  THEN  Auto)
  THEN  (Assert  b  \mneq{}  a  BY
                          (D  -1  THEN  Unhide  THEN  Auto))
  THEN  UnfoldTopAb  3
  THEN  (D  -1
              THENL  [((InstLemma  `ravg-between`  [\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]\mcdot{}  THENA  Auto)
                              THEN  (InstLemma  `i-member-between`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}ravg(b;a)\mkleeneclose{}]\mcdot{}  THENA  Auto)
                              THEN  D  -2
                              THEN  (FHyp  3  [-2]  THENA  Auto))
                          ;  ((InstLemma  `ravg-between`  [\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                THEN  (InstLemma  `i-member-between`  [\mkleeneopen{}I\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}ravg(a;b)\mkleeneclose{}]\mcdot{}  THENA  Auto)
                                THEN  D  -2
                                THEN  (FHyp  3  [-3]  THENA  Auto))]
  )
  THEN  ParallelLast
  THEN  Auto)

---

Home Index