---

Step * of Lemma rv-line-circle-3

No Annotations
∀n:ℕ. ∀c,b,d,q:ℝ^n.
  (c_b_d
  ⇒ (d(c;d) < d(c;q))
  ⇒ (∃u:{u:ℝ^n| cd=cu ∧ q_u_b} 
       (∃v:ℝ^n [(cd=cv
               ∧ q_b_v
               ∧ (b ≠ d ⇒ (u ≠ v ∧ u ≠ b ∧ v ≠ b))
               ∧ (req-vec(n;b;d)
                 ⇒ ((u ≠ v ⇒ ((req-vec(n;u;b) ∧ (r0 < b - c⋅q - b)) ∨ (req-vec(n;v;b) ∧ (b - c⋅q - b < r0))))
                    ∧ (req-vec(n;u;v) ⇒ ((b - c⋅q - b = r0) ∧ req-vec(n;u;b))))))])))
BY
{ (Auto
   THEN (FLemma `rv-be-dist` [-2] THENA Auto)
   THEN (Assert (d(c;b) + d(b;d)) < (d(c;b) + d(b;q)) BY
               (InstLemma `real-vec-triangle-inequality` [⌜n⌝;⌜c⌝;⌜b⌝;⌜q⌝]⋅ THEN Auto))
   THEN (nRAdd ⌜-(d(c;b))⌝ (-1)⋅ THENA Auto)
   THEN (Assert b ≠ q BY
               (UnfoldTopAb 0 THEN (Assert r0 ≤ d(b;d) BY Auto) THEN Auto))
   THEN (InstLemma `rv-line-circle-0-ext` [⌜n⌝;⌜c⌝;⌜d⌝;⌜b⌝;⌜q⌝]⋅
         THENA (Auto THEN (RWO  "-3" 0 THEN Auto) THEN nRAdd ⌜-(d(c;b))⌝ 0⋅ THEN Auto)
         )
   THEN All (Fold  `rv-be`)
   THEN D -1
   THEN D -1
   THEN (D 0 With ⌜u⌝  THEN Auto)
   THEN D 0 With ⌜v⌝ 
   THEN Auto) }

1
1. n : ℕ
2. c : ℝ^n
3. b : ℝ^n
4. d : ℝ^n
5. q : ℝ^n
6. c_b_d
7. d(c;d) < d(c;q)
8. d(c;d) = (d(c;b) + d(b;d))
9. d(b;d) < d(b;q)
10. b ≠ q
11. u : ∃u:ℝ^n [(cd=cu ∧ q_u_b)]
12. v : ℝ^n
13. cd=cv
14. q_b_v
15. (d(c;b) < d(c;d)) ⇒ (q-b-v ∧ ((d(c;d) < d(c;q)) ⇒ q-u-b))
16. (d(c;b) = d(c;d))
⇒ ((u ≠ v ⇒ ((req-vec(n;u;b) ∧ (r0 < b - c⋅q - b)) ∨ (req-vec(n;v;b) ∧ (b - c⋅q - b < r0))))
   ∧ (req-vec(n;u;v) ⇒ ((b - c⋅q - b = r0) ∧ req-vec(n;u;b))))
17. cd=cv
18. q_b_v
19. b ≠ d
⊢ u ≠ v

2
1. n : ℕ
2. c : ℝ^n
3. b : ℝ^n
4. d : ℝ^n
5. q : ℝ^n
6. c_b_d
7. d(c;d) < d(c;q)
8. d(c;d) = (d(c;b) + d(b;d))
9. d(b;d) < d(b;q)
10. b ≠ q
11. u : ∃u:ℝ^n [(cd=cu ∧ q_u_b)]
12. v : ℝ^n
13. cd=cv
14. q_b_v
15. (d(c;b) < d(c;d)) ⇒ (q-b-v ∧ ((d(c;d) < d(c;q)) ⇒ q-u-b))
16. (d(c;b) = d(c;d))
⇒ ((u ≠ v ⇒ ((req-vec(n;u;b) ∧ (r0 < b - c⋅q - b)) ∨ (req-vec(n;v;b) ∧ (b - c⋅q - b < r0))))
   ∧ (req-vec(n;u;v) ⇒ ((b - c⋅q - b = r0) ∧ req-vec(n;u;b))))
17. cd=cv
18. q_b_v
19. b ≠ d
20. u ≠ v
⊢ u ≠ b

3
1. n : ℕ
2. c : ℝ^n
3. b : ℝ^n
4. d : ℝ^n
5. q : ℝ^n
6. c_b_d
7. d(c;d) < d(c;q)
8. d(c;d) = (d(c;b) + d(b;d))
9. d(b;d) < d(b;q)
10. b ≠ q
11. u : ∃u:ℝ^n [(cd=cu ∧ q_u_b)]
12. v : ℝ^n
13. cd=cv
14. q_b_v
15. (d(c;b) < d(c;d)) ⇒ (q-b-v ∧ ((d(c;d) < d(c;q)) ⇒ q-u-b))
16. (d(c;b) = d(c;d))
⇒ ((u ≠ v ⇒ ((req-vec(n;u;b) ∧ (r0 < b - c⋅q - b)) ∨ (req-vec(n;v;b) ∧ (b - c⋅q - b < r0))))
   ∧ (req-vec(n;u;v) ⇒ ((b - c⋅q - b = r0) ∧ req-vec(n;u;b))))
17. cd=cv
18. q_b_v
19. b ≠ d
20. u ≠ v
21. u ≠ b
⊢ v ≠ b

---

Latex:

---

Latex:
No  Annotations
\mforall{}n:\mBbbN{}.  \mforall{}c,b,d,q:\mBbbR{}\^{}n.
    (c\_b\_d
    {}\mRightarrow{}  (d(c;d)  <  d(c;q))
    {}\mRightarrow{}  (\mexists{}u:\{u:\mBbbR{}\^{}n|  cd=cu  \mwedge{}  q\_u\_b\} 
              (\mexists{}v:\mBbbR{}\^{}n  [(cd=cv
                              \mwedge{}  q\_b\_v
                              \mwedge{}  (b  \mneq{}  d  {}\mRightarrow{}  (u  \mneq{}  v  \mwedge{}  u  \mneq{}  b  \mwedge{}  v  \mneq{}  b))
                              \mwedge{}  (req-vec(n;b;d)
                                  {}\mRightarrow{}  ((u  \mneq{}  v
                                        {}\mRightarrow{}  ((req-vec(n;u;b)  \mwedge{}  (r0  <  b  -  c\mcdot{}q  -  b))
                                              \mvee{}  (req-vec(n;v;b)  \mwedge{}  (b  -  c\mcdot{}q  -  b  <  r0))))
                                        \mwedge{}  (req-vec(n;u;v)  {}\mRightarrow{}  ((b  -  c\mcdot{}q  -  b  =  r0)  \mwedge{}  req-vec(n;u;b))))))])))


By

---

Latex:
(Auto
  THEN  (FLemma  `rv-be-dist`  [-2]  THENA  Auto)
  THEN  (Assert  (d(c;b)  +  d(b;d))  <  (d(c;b)  +  d(b;q))  BY
                          (InstLemma  `real-vec-triangle-inequality`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}  THEN  Auto))
  THEN  (nRAdd  \mkleeneopen{}-(d(c;b))\mkleeneclose{}  (-1)\mcdot{}  THENA  Auto)
  THEN  (Assert  b  \mneq{}  q  BY
                          (UnfoldTopAb  0  THEN  (Assert  r0  \mleq{}  d(b;d)  BY  Auto)  THEN  Auto))
  THEN  (InstLemma  `rv-line-circle-0-ext`  [\mkleeneopen{}n\mkleeneclose{};\mkleeneopen{}c\mkleeneclose{};\mkleeneopen{}d\mkleeneclose{};\mkleeneopen{}b\mkleeneclose{};\mkleeneopen{}q\mkleeneclose{}]\mcdot{}
              THENA  (Auto  THEN  (RWO    "-3"  0  THEN  Auto)  THEN  nRAdd  \mkleeneopen{}-(d(c;b))\mkleeneclose{}  0\mcdot{}  THEN  Auto)
              )
  THEN  All  (Fold    `rv-be`)
  THEN  D  -1
  THEN  D  -1
  THEN  (D  0  With  \mkleeneopen{}u\mkleeneclose{}    THEN  Auto)
  THEN  D  0  With  \mkleeneopen{}v\mkleeneclose{} 
  THEN  Auto)

---

Home Index