---

Step * of Lemma real-path-comp-exists

No Annotations
∀f,g:[r0, r1] ⟶ℝ.
  ((∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) ⇒ (f(x) = f(y))))
  ⇒ (∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) ⇒ (g(x) = g(y))))
  ⇒ (f(r1) = g(r0))
  ⇒ (∃h:[r0, r1] ⟶ℝ
       ((∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (h(t) = f(r(2) * t)))
       ∧ (∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (h(t) = g((r(2) * t) - r1)))
       ∧ (∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) ⇒ (h(x) = h(y)))))))
BY
{ (Auto
   THEN (Assert ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (rmin(t;(r1/r(2))) = t) BY
               (Auto THEN BLemma `rmin-req2` THEN Auto))
   THEN (Assert ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (r(2) * t ∈ [r0, r1]) BY
               (Auto THEN All Reduce THEN Auto THEN (Assert t ≤ (r1/r(2)) BY Auto) THEN nRMul ⌜r(2)⌝ (-1)⋅ THEN Auto))
   THEN (Assert ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (f(r(2) * rmin(t;(r1/r(2)))) = f(r(2) * t)) BY
               (Auto THEN BackThruSomeHyp THEN Auto THEN Try ((MemTypeCD THEN Auto)) THEN RWO  "6" 0 THEN Auto))) }

1
1. f : [r0, r1] ⟶ℝ
2. g : [r0, r1] ⟶ℝ
3. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) ⇒ (f(x) = f(y)))
4. ∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) ⇒ (g(x) = g(y)))
5. f(r1) = g(r0)
6. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (rmin(t;(r1/r(2))) = t)
7. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (r(2) * t ∈ [r0, r1])
8. ∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (f(r(2) * rmin(t;(r1/r(2)))) = f(r(2) * t))
⊢ ∃h:[r0, r1] ⟶ℝ
   ((∀t:{x:ℝ| x ∈ [r0, (r1/r(2))]} . (h(t) = f(r(2) * t)))
   ∧ (∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (h(t) = g((r(2) * t) - r1)))
   ∧ (∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) ⇒ (h(x) = h(y)))))

---

Latex:

---

Latex:
No  Annotations
\mforall{}f,g:[r0,  r1]  {}\mrightarrow{}\mBbbR{}.
    ((\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y))))
    {}\mRightarrow{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .    ((x  =  y)  {}\mRightarrow{}  (g(x)  =  g(y))))
    {}\mRightarrow{}  (f(r1)  =  g(r0))
    {}\mRightarrow{}  (\mexists{}h:[r0,  r1]  {}\mrightarrow{}\mBbbR{}
              ((\mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  (r1/r(2))]\}  .  (h(t)  =  f(r(2)  *  t)))
              \mwedge{}  (\mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [(r1/r(2)),  r1]\}  .  (h(t)  =  g((r(2)  *  t)  -  r1)))
              \mwedge{}  (\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .    ((x  =  y)  {}\mRightarrow{}  (h(x)  =  h(y)))))))


By

---

Latex:
(Auto
  THEN  (Assert  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  (r1/r(2))]\}  .  (rmin(t;(r1/r(2)))  =  t)  BY
                          (Auto  THEN  BLemma  `rmin-req2`  THEN  Auto))
  THEN  (Assert  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  (r1/r(2))]\}  .  (r(2)  *  t  \mmember{}  [r0,  r1])  BY
                          (Auto
                            THEN  All  Reduce
                            THEN  Auto
                            THEN  (Assert  t  \mleq{}  (r1/r(2))  BY
                                                    Auto)
                            THEN  nRMul  \mkleeneopen{}r(2)\mkleeneclose{}  (-1)\mcdot{}
                            THEN  Auto))
  THEN  (Assert  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  (r1/r(2))]\}  .  (f(r(2)  *  rmin(t;(r1/r(2))))  =  f(r(2)  *  t))  BY
                          (Auto
                            THEN  BackThruSomeHyp
                            THEN  Auto
                            THEN  Try  ((MemTypeCD  THEN  Auto))
                            THEN  RWO    "6"  0
                            THEN  Auto)))

---

Home Index