Step * 3 1 of Lemma path-comp-for-reals


1. {f:{x:ℝ(r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ| ∀t,t':{x:ℝ(r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t')  t ≠ t'))} 
2. {f:{x:ℝ(r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ| ∀t,t':{x:ℝ(r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t')  t ≠ t'))} 
3. ¬f@r1 ≠ g@r0
4. [r0, r1] ⟶ℝ
5. ∀t:{x:ℝx ∈ [r0, (r1/r(2))]} (h(t) f(r(2) t))
6. ∀t:{x:ℝx ∈ [(r1/r(2)), r1]} (h(t) g((r(2) t) r1))
7. ∀x,y:{x:ℝx ∈ [r0, r1]} .  ((x y)  (h(x) h(y)))
8. h1 {f:{x:ℝ(r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ| ∀t,t':{x:ℝ(r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t')  t ≠ t'))} 
9. : ∀t:{x:ℝ(r0 ≤ x) ∧ (x ≤ (r1/r(2)))} h1 t ≠ (r(2) t))
10. {x:ℝ((r1/r(2)) ≤ x) ∧ (x ≤ r1)} 
⊢ (r(2) t) r1 ∈ {x:ℝ(r0 ≤ x) ∧ (x ≤ r1)} 
BY
(DSetVars THEN ExRepD THEN MemTypeCD THEN Auto) }

1
1. {x:ℝ(r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ
2. ∀t,t':{x:ℝ(r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t')  t ≠ t'))
3. {x:ℝ(r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ
4. ∀t,t':{x:ℝ(r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t')  t ≠ t'))
5. ¬f@r1 ≠ g@r0
6. [r0, r1] ⟶ℝ
7. ∀t:{x:ℝx ∈ [r0, (r1/r(2))]} (h(t) f(r(2) t))
8. ∀t:{x:ℝx ∈ [(r1/r(2)), r1]} (h(t) g((r(2) t) r1))
9. ∀x,y:{x:ℝx ∈ [r0, r1]} .  ((x y)  (h(x) h(y)))
10. h1 {x:ℝ(r0 ≤ x) ∧ (x ≤ r1)}  ⟶ ℝ
11. ∀t,t':{x:ℝ(r0 ≤ x) ∧ (x ≤ r1)} .  ((¬t ≠ t')  h1 t ≠ h1 t'))
12. : ∀t:{x:ℝ(r0 ≤ x) ∧ (x ≤ (r1/r(2)))} h1 t ≠ (r(2) t))
13. : ℝ
14. r1 ≤ (r(2) t)
15. t ≤ r1
16. r0 ≤ ((r(2) t) r1)
⊢ ((r(2) t) r1) ≤ r1


Latex:


Latex:

1.  f  :  \{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  \mBbbR{}| 
                \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    ((\mneg{}t  \mneq{}  t')  {}\mRightarrow{}  (\mneg{}f  t  \mneq{}  f  t'))\} 
2.  g  :  \{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  \mBbbR{}| 
                \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    ((\mneg{}t  \mneq{}  t')  {}\mRightarrow{}  (\mneg{}f  t  \mneq{}  f  t'))\} 
3.  \mneg{}f@r1  \mneq{}  g@r0
4.  h  :  [r0,  r1]  {}\mrightarrow{}\mBbbR{}
5.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  (r1/r(2))]\}  .  (h(t)  =  f(r(2)  *  t))
6.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [(r1/r(2)),  r1]\}  .  (h(t)  =  g((r(2)  *  t)  -  r1))
7.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .    ((x  =  y)  {}\mRightarrow{}  (h(x)  =  h(y)))
8.  h1  :  \{f:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}    {}\mrightarrow{}  \mBbbR{}| 
                  \mforall{}t,t':\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\}  .    ((\mneg{}t  \mneq{}  t')  {}\mRightarrow{}  (\mneg{}f  t  \mneq{}  f  t'))\} 
9.  x  :  \mforall{}t:\{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  (r1/r(2)))\}  .  (\mneg{}h1  t  \mneq{}  f  (r(2)  *  t))
10.  t  :  \{x:\mBbbR{}|  ((r1/r(2))  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\} 
\mvdash{}  (r(2)  *  t)  -  r1  \mmember{}  \{x:\mBbbR{}|  (r0  \mleq{}  x)  \mwedge{}  (x  \mleq{}  r1)\} 


By


Latex:
(DSetVars  THEN  ExRepD  THEN  MemTypeCD  THEN  Auto)




Home Index