---

Step * 1 1 1 1 1 1 2 3 of Lemma real-path-comp-exists

.....antecedent..... 
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))
9. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (rmax(t;(r1/r(2))) = t)
10. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . ((r(2) * t) - r1 ∈ [r0, r1])
11. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) = g((r(2) * t) - r1))
12. ∀t:{x:ℝ| x ∈ [r0, r1]} . (f(r(2) * rmin(t;(r1/r(2)))) ∈ ℝ)
13. t : {x:ℝ| x ∈ [r0, r1]} 
14. f(r(2) * rmin(t;(r1/r(2)))) ∈ ℝ
15. g((r(2) * rmax(t;(r1/r(2)))) - r1) ∈ ℝ
16. ∀F:[r0, r1] ⟶ℝ
      ((∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) ⇒ (F(x) = F(y))))
      ⇒ (F((r1/r(2))) = r0)
      ⇒ (∀n:ℕ+. ∃m:ℕ+. ((|t - (r1/r(2))| ≤ (r1/r(m))) ⇒ (|F(t)| ≤ (r1/r(n))))))
⊢ λt.(f(r(2) * rmin(t;(r1/r(2)))) - g((r(2) * rmax(t;(r1/r(2)))) - r1))((r1/r(2))) = r0
BY
{ (RepUR ``r-ap`` 0
   THEN (Assert (r(2) * rmin((r1/r(2));(r1/r(2)))) = r1 BY
               ((RWO "rmin-req" 0 THEN Auto) THEN nRNorm 0 THEN Auto))
   THEN (Assert ((r(2) * rmax((r1/r(2));(r1/r(2)))) - r1) = r0 BY
               ((RWO "rmax-req" 0 THEN Auto) THEN nRNorm 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))
9. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (rmax(t;(r1/r(2))) = t)
10. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . ((r(2) * t) - r1 ∈ [r0, r1])
11. ∀t:{x:ℝ| x ∈ [(r1/r(2)), r1]} . (g((r(2) * rmax(t;(r1/r(2)))) - r1) = g((r(2) * t) - r1))
12. ∀t:{x:ℝ| x ∈ [r0, r1]} . (f(r(2) * rmin(t;(r1/r(2)))) ∈ ℝ)
13. t : {x:ℝ| x ∈ [r0, r1]} 
14. f(r(2) * rmin(t;(r1/r(2)))) ∈ ℝ
15. g((r(2) * rmax(t;(r1/r(2)))) - r1) ∈ ℝ
16. ∀F:[r0, r1] ⟶ℝ
      ((∀x,y:{x:ℝ| x ∈ [r0, r1]} .  ((x = y) ⇒ (F(x) = F(y))))
      ⇒ (F((r1/r(2))) = r0)
      ⇒ (∀n:ℕ+. ∃m:ℕ+. ((|t - (r1/r(2))| ≤ (r1/r(m))) ⇒ (|F(t)| ≤ (r1/r(n))))))
17. (r(2) * rmin((r1/r(2));(r1/r(2)))) = r1
18. ((r(2) * rmax((r1/r(2));(r1/r(2)))) - r1) = r0
⊢ ((f (r(2) * rmin((r1/r(2));(r1/r(2))))) - g ((r(2) * rmax((r1/r(2));(r1/r(2)))) - r1)) = r0

---

Latex:

---

Latex:
.....antecedent..... 
1.  f  :  [r0,  r1]  {}\mrightarrow{}\mBbbR{}
2.  g  :  [r0,  r1]  {}\mrightarrow{}\mBbbR{}
3.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .    ((x  =  y)  {}\mRightarrow{}  (f(x)  =  f(y)))
4.  \mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .    ((x  =  y)  {}\mRightarrow{}  (g(x)  =  g(y)))
5.  f(r1)  =  g(r0)
6.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  (r1/r(2))]\}  .  (rmin(t;(r1/r(2)))  =  t)
7.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  (r1/r(2))]\}  .  (r(2)  *  t  \mmember{}  [r0,  r1])
8.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  (r1/r(2))]\}  .  (f(r(2)  *  rmin(t;(r1/r(2))))  =  f(r(2)  *  t))
9.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [(r1/r(2)),  r1]\}  .  (rmax(t;(r1/r(2)))  =  t)
10.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [(r1/r(2)),  r1]\}  .  ((r(2)  *  t)  -  r1  \mmember{}  [r0,  r1])
11.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [(r1/r(2)),  r1]\}  .  (g((r(2)  *  rmax(t;(r1/r(2))))  -  r1)  =  g((r(2)  *  t)  -  r1))
12.  \mforall{}t:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .  (f(r(2)  *  rmin(t;(r1/r(2))))  \mmember{}  \mBbbR{})
13.  t  :  \{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\} 
14.  f(r(2)  *  rmin(t;(r1/r(2))))  \mmember{}  \mBbbR{}
15.  g((r(2)  *  rmax(t;(r1/r(2))))  -  r1)  \mmember{}  \mBbbR{}
16.  \mforall{}F:[r0,  r1]  {}\mrightarrow{}\mBbbR{}
            ((\mforall{}x,y:\{x:\mBbbR{}|  x  \mmember{}  [r0,  r1]\}  .    ((x  =  y)  {}\mRightarrow{}  (F(x)  =  F(y))))
            {}\mRightarrow{}  (F((r1/r(2)))  =  r0)
            {}\mRightarrow{}  (\mforall{}n:\mBbbN{}\msupplus{}.  \mexists{}m:\mBbbN{}\msupplus{}.  ((|t  -  (r1/r(2))|  \mleq{}  (r1/r(m)))  {}\mRightarrow{}  (|F(t)|  \mleq{}  (r1/r(n))))))
\mvdash{}  \mlambda{}t.(f(r(2)  *  rmin(t;(r1/r(2))))  -  g((r(2)  *  rmax(t;(r1/r(2))))  -  r1))((r1/r(2)))  =  r0


By

---

Latex:
(RepUR  ``r-ap``  0
  THEN  (Assert  (r(2)  *  rmin((r1/r(2));(r1/r(2))))  =  r1  BY
                          ((RWO  "rmin-req"  0  THEN  Auto)  THEN  nRNorm  0  THEN  Auto))
  THEN  (Assert  ((r(2)  *  rmax((r1/r(2));(r1/r(2))))  -  r1)  =  r0  BY
                          ((RWO  "rmax-req"  0  THEN  Auto)  THEN  nRNorm  0  THEN  Auto)))

---

Home Index