---

Step * 1 1 1 of Lemma interval-connected


1. I : Interval
2. [A] : {x:ℝ| x ∈ I}  ⟶ ℙ
3. [B] : {x:ℝ| x ∈ I}  ⟶ ℙ
4. ∀x:{x:ℝ| x ∈ I} . ∀y:{y:{x:ℝ| x ∈ I} | x = y} .  (A[y] ⇒ A[x])
5. ∀x:{x:ℝ| x ∈ I} . ∀y:{y:{x:ℝ| x ∈ I} | x = y} .  (B[y] ⇒ B[x])
6. a : {x:ℝ| x ∈ I} 
7. A[a]
8. b : {x:ℝ| x ∈ I} 
9. B[b]
10. ∀r:{x:ℝ| x ∈ I} . (A[r] ∨ B[r])
11. Connected({x:ℝ| x ∈ [rmin(a;b), rmax(a;b)]} )
12. [rmin(a;b), rmax(a;b)] ⊆ I 
⊢ ∃r:{x:ℝ| x ∈ I} . (A[r] ∧ B[r])
BY
{ ((D -2 With ⌜A⌝  THENA Auto)
   THEN (D -1 With ⌜B⌝  THENA Auto)
   THEN (D -1 THENA (Auto THEN InstHyp [⌜x⌝;⌜y⌝] 4⋅ THEN Auto))
   THEN (D -1 THENA (Auto THEN InstHyp [⌜x⌝;⌜y⌝] 5⋅ THEN Auto))
   THEN (D -1 THENA (D 0 With ⌜a⌝  THEN Auto))
   THEN (D -1 THENA (D 0 With ⌜b⌝  THEN Auto))) }

1
1. I : Interval
2. [A] : {x:ℝ| x ∈ I}  ⟶ ℙ
3. [B] : {x:ℝ| x ∈ I}  ⟶ ℙ
4. ∀x:{x:ℝ| x ∈ I} . ∀y:{y:{x:ℝ| x ∈ I} | x = y} .  (A[y] ⇒ A[x])
5. ∀x:{x:ℝ| x ∈ I} . ∀y:{y:{x:ℝ| x ∈ I} | x = y} .  (B[y] ⇒ B[x])
6. a : {x:ℝ| x ∈ I} 
7. A[a]
8. b : {x:ℝ| x ∈ I} 
9. B[b]
10. ∀r:{x:ℝ| x ∈ I} . (A[r] ∨ B[r])
11. [rmin(a;b), rmax(a;b)] ⊆ I 
12. (∀r:{x:ℝ| x ∈ [rmin(a;b), rmax(a;b)]} . (A[r] ∨ B[r])) ⇒ (∃r:{x:ℝ| x ∈ [rmin(a;b), rmax(a;b)]} . (A[r] ∧ B[r]))
⊢ ∃r:{x:ℝ| x ∈ I} . (A[r] ∧ B[r])

---

Latex:

---

Latex:

1.  I  :  Interval
2.  [A]  :  \{x:\mBbbR{}|  x  \mmember{}  I\}    {}\mrightarrow{}  \mBbbP{}
3.  [B]  :  \{x:\mBbbR{}|  x  \mmember{}  I\}    {}\mrightarrow{}  \mBbbP{}
4.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  x  \mmember{}  I\}  |  x  =  y\}  .    (A[y]  {}\mRightarrow{}  A[x])
5.  \mforall{}x:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  \mforall{}y:\{y:\{x:\mBbbR{}|  x  \mmember{}  I\}  |  x  =  y\}  .    (B[y]  {}\mRightarrow{}  B[x])
6.  a  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
7.  A[a]
8.  b  :  \{x:\mBbbR{}|  x  \mmember{}  I\} 
9.  B[b]
10.  \mforall{}r:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (A[r]  \mvee{}  B[r])
11.  Connected(\{x:\mBbbR{}|  x  \mmember{}  [rmin(a;b),  rmax(a;b)]\}  )
12.  [rmin(a;b),  rmax(a;b)]  \msubseteq{}  I 
\mvdash{}  \mexists{}r:\{x:\mBbbR{}|  x  \mmember{}  I\}  .  (A[r]  \mwedge{}  B[r])


By

---

Latex:
((D  -2  With  \mkleeneopen{}A\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  With  \mkleeneopen{}B\mkleeneclose{}    THENA  Auto)
  THEN  (D  -1  THENA  (Auto  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  4\mcdot{}  THEN  Auto))
  THEN  (D  -1  THENA  (Auto  THEN  InstHyp  [\mkleeneopen{}x\mkleeneclose{};\mkleeneopen{}y\mkleeneclose{}]  5\mcdot{}  THEN  Auto))
  THEN  (D  -1  THENA  (D  0  With  \mkleeneopen{}a\mkleeneclose{}    THEN  Auto))
  THEN  (D  -1  THENA  (D  0  With  \mkleeneopen{}b\mkleeneclose{}    THEN  Auto)))

---

Home Index