---

Step * 1 1 1 1 1 of Lemma rv-inner-Pasch3


1. n : ℕ
2. a : ℝ^n
3. b : ℝ^n
4. c : ℝ^n
5. p : ℝ^n
6. q : ℝ^n
7. b ≠ c
8. (¬a ≠ c) ⇒ (¬p ≠ c)
9. rv-T(n;b;q;c)
10. a ≠ c
11. t : ℝ
12. t ∈ [r0, r1]
13. req-vec(n;p;t*a + r1 - t*c)
14. d(a;p) = (|r1 - t| * d(a;c))
15. d(p;c) = (|t| * d(a;c))
16. r0 < |r1 - t|
17. r0 < d(a;c)
18. r0 < |t|
19. r0 < d(a;c)
⊢ t ∈ (r0, r1)
BY
{ (All Reduce
   THEN (RWO "rabs-of-nonneg" (-2) THENA Auto)
   THEN (RWO "rabs-of-nonneg" (-4) THENA (Auto THEN nRAdd ⌜t⌝ 0⋅ THEN Auto))
   THEN nRAdd ⌜t⌝ (-4)⋅
   THEN Auto) }

---

Latex:

---

Latex:

1.  n  :  \mBbbN{}
2.  a  :  \mBbbR{}\^{}n
3.  b  :  \mBbbR{}\^{}n
4.  c  :  \mBbbR{}\^{}n
5.  p  :  \mBbbR{}\^{}n
6.  q  :  \mBbbR{}\^{}n
7.  b  \mneq{}  c
8.  (\mneg{}a  \mneq{}  c)  {}\mRightarrow{}  (\mneg{}p  \mneq{}  c)
9.  rv-T(n;b;q;c)
10.  a  \mneq{}  c
11.  t  :  \mBbbR{}
12.  t  \mmember{}  [r0,  r1]
13.  req-vec(n;p;t*a  +  r1  -  t*c)
14.  d(a;p)  =  (|r1  -  t|  *  d(a;c))
15.  d(p;c)  =  (|t|  *  d(a;c))
16.  r0  <  |r1  -  t|
17.  r0  <  d(a;c)
18.  r0  <  |t|
19.  r0  <  d(a;c)
\mvdash{}  t  \mmember{}  (r0,  r1)


By

---

Latex:
(All  Reduce
  THEN  (RWO  "rabs-of-nonneg"  (-2)  THENA  Auto)
  THEN  (RWO  "rabs-of-nonneg"  (-4)  THENA  (Auto  THEN  nRAdd  \mkleeneopen{}t\mkleeneclose{}  0\mcdot{}  THEN  Auto))
  THEN  nRAdd  \mkleeneopen{}t\mkleeneclose{}  (-4)\mcdot{}
  THEN  Auto)

---

Home Index