---

Step * 2 1 2 2 1 1 4 2 1 1 1 of Lemma ip-line-circle-1


1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. p : Point(rv)
5. q : Point(rv)
6. a # b
7. p # q
8. pp : Point(rv)
9. p - a = pp ∈ Point(rv)
10. qq : Point(rv)
11. q - a = qq ∈ Point(rv)
12. ||pp|| ≤ ||a - b||
13. ||a - b|| ≤ ||qq||
14. pp # qq
15. r0 < ||qq - pp||
16. r0 < ||qq - pp||^2
17. r0 ≤ (((r(2) * pp ⋅ qq - pp) * r(2) * pp ⋅ qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - ||a - b||^2))
18. t : ℝ
19. quadratic1(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2) = t ∈ ℝ
20. s : ℝ
21. quadratic2(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2) = s ∈ ℝ
22. ∀X:Point(rv). pp + X ≡ p + X - a
23. ||p + t*q - p - a|| = ||a - b||
24. ||p + s*q - p - a|| = ||a - b||
25. t ∈ [r0, r1]
26. s ≤ r0
27. (||a - p|| < ||a - b||) ⇒ (s < r0)
28. qq - pp ≡ q - p
29. ab=ap + s*q - p
30. q ≡ p + s*q - p ⇒ p ≡ p + s*q - p
31. q # p + s*q - p
32. ∀t:ℝ. ((t ≤ r0) ⇒ ((-(t)/r1 - t) ∈ [r0, r1]))
33. (-(s)/r1 - s) ∈ [r0, r1]
34. r0 < (r1 - s)
⊢ ∃t:ℝ. ((t ∈ [r0, r1]) ∧ p ≡ t*q + r1 - t*p + s*q - p)
BY
{ (D 0 With ⌜(-(s)/r1 - s)⌝  THEN Auto) }

1
1. rv : InnerProductSpace
2. a : Point(rv)
3. b : Point(rv)
4. p : Point(rv)
5. q : Point(rv)
6. a # b
7. p # q
8. pp : Point(rv)
9. p - a = pp ∈ Point(rv)
10. qq : Point(rv)
11. q - a = qq ∈ Point(rv)
12. ||pp|| ≤ ||a - b||
13. ||a - b|| ≤ ||qq||
14. pp # qq
15. r0 < ||qq - pp||
16. r0 < ||qq - pp||^2
17. r0 ≤ (((r(2) * pp ⋅ qq - pp) * r(2) * pp ⋅ qq - pp) - r(4) * ||qq - pp||^2 * (||pp||^2 - ||a - b||^2))
18. t : ℝ
19. quadratic1(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2) = t ∈ ℝ
20. s : ℝ
21. quadratic2(||qq - pp||^2;r(2) * pp ⋅ qq - pp;||pp||^2 - ||a - b||^2) = s ∈ ℝ
22. ∀X:Point(rv). pp + X ≡ p + X - a
23. ||p + t*q - p - a|| = ||a - b||
24. ||p + s*q - p - a|| = ||a - b||
25. t ∈ [r0, r1]
26. s ≤ r0
27. (||a - p|| < ||a - b||) ⇒ (s < r0)
28. qq - pp ≡ q - p
29. ab=ap + s*q - p
30. q ≡ p + s*q - p ⇒ p ≡ p + s*q - p
31. q # p + s*q - p
32. ∀t:ℝ. ((t ≤ r0) ⇒ ((-(t)/r1 - t) ∈ [r0, r1]))
33. (-(s)/r1 - s) ∈ [r0, r1]
34. r0 < (r1 - s)
35. (-(s)/r1 - s) ∈ [r0, r1]
⊢ p ≡ (-(s)/r1 - s)*q + r1 - (-(s)/r1 - s)*p + s*q - p

---

Latex:

---

Latex:

1.  rv  :  InnerProductSpace
2.  a  :  Point(rv)
3.  b  :  Point(rv)
4.  p  :  Point(rv)
5.  q  :  Point(rv)
6.  a  \#  b
7.  p  \#  q
8.  pp  :  Point(rv)
9.  p  -  a  =  pp
10.  qq  :  Point(rv)
11.  q  -  a  =  qq
12.  ||pp||  \mleq{}  ||a  -  b||
13.  ||a  -  b||  \mleq{}  ||qq||
14.  pp  \#  qq
15.  r0  <  ||qq  -  pp||
16.  r0  <  ||qq  -  pp||\^{}2
17.  r0  \mleq{}  (((r(2)  *  pp  \mcdot{}  qq  -  pp)  *  r(2)  *  pp  \mcdot{}  qq  -  pp)  -  r(4)
*  ||qq  -  pp||\^{}2
*  (||pp||\^{}2  -  ||a  -  b||\^{}2))
18.  t  :  \mBbbR{}
19.  quadratic1(||qq  -  pp||\^{}2;r(2)  *  pp  \mcdot{}  qq  -  pp;||pp||\^{}2  -  ||a  -  b||\^{}2)  =  t
20.  s  :  \mBbbR{}
21.  quadratic2(||qq  -  pp||\^{}2;r(2)  *  pp  \mcdot{}  qq  -  pp;||pp||\^{}2  -  ||a  -  b||\^{}2)  =  s
22.  \mforall{}X:Point(rv).  pp  +  X  \mequiv{}  p  +  X  -  a
23.  ||p  +  t*q  -  p  -  a||  =  ||a  -  b||
24.  ||p  +  s*q  -  p  -  a||  =  ||a  -  b||
25.  t  \mmember{}  [r0,  r1]
26.  s  \mleq{}  r0
27.  (||a  -  p||  <  ||a  -  b||)  {}\mRightarrow{}  (s  <  r0)
28.  qq  -  pp  \mequiv{}  q  -  p
29.  ab=ap  +  s*q  -  p
30.  q  \mequiv{}  p  +  s*q  -  p  {}\mRightarrow{}  p  \mequiv{}  p  +  s*q  -  p
31.  q  \#  p  +  s*q  -  p
32.  \mforall{}t:\mBbbR{}.  ((t  \mleq{}  r0)  {}\mRightarrow{}  ((-(t)/r1  -  t)  \mmember{}  [r0,  r1]))
33.  (-(s)/r1  -  s)  \mmember{}  [r0,  r1]
34.  r0  <  (r1  -  s)
\mvdash{}  \mexists{}t:\mBbbR{}.  ((t  \mmember{}  [r0,  r1])  \mwedge{}  p  \mequiv{}  t*q  +  r1  -  t*p  +  s*q  -  p)


By

---

Latex:
(D  0  With  \mkleeneopen{}(-(s)/r1  -  s)\mkleeneclose{}    THEN  Auto)

---

Home Index