---

Step * 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|) ∧ (r0 < d(a;c))) ∨ ((|r1 - t| < r0) ∧ (d(a;c) < r0))
17. ((r0 < |t|) ∧ (r0 < d(a;c))) ∨ ((|t| < r0) ∧ (d(a;c) < r0))
⊢ a-p-c
BY
{ ((D -2 THEN ExRepD)
   THENL [(D -1 THENL [(D 0 With ⌜t⌝  THEN Auto); ((Assert r0 ≤ |t| BY Auto) THEN (Assert r0 < r0 BY Auto) THEN Auto)])
         ; ((Assert r0 ≤ |r1 - t| BY Auto) THEN (Assert r0 < r0 BY Auto) THEN Auto)]
) }

1
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)

---

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|)  \mwedge{}  (r0  <  d(a;c)))  \mvee{}  ((|r1  -  t|  <  r0)  \mwedge{}  (d(a;c)  <  r0))
17.  ((r0  <  |t|)  \mwedge{}  (r0  <  d(a;c)))  \mvee{}  ((|t|  <  r0)  \mwedge{}  (d(a;c)  <  r0))
\mvdash{}  a-p-c


By

---

Latex:
((D  -2  THEN  ExRepD)
  THENL  [(D  -1
                  THENL  [(D  0  With  \mkleeneopen{}t\mkleeneclose{}    THEN  Auto)
                              ;  ((Assert  r0  \mleq{}  |t|  BY  Auto)  THEN  (Assert  r0  <  r0  BY  Auto)  THEN  Auto)]
              )
              ;  ((Assert  r0  \mleq{}  |r1  -  t|  BY  Auto)  THEN  (Assert  r0  <  r0  BY  Auto)  THEN  Auto)]
)

---

Home Index