---

Step * 2 1 of Lemma line-circle-intersection-lemma


1. a : ℝ
2. b : ℝ
3. c : ℝ
4. r : ℝ
5. M : ℝ
6. (a^2 + b^2) = M ∈ ℝ
7. k : ℝ
8. ((M * r^2) - c^2) = k ∈ ℝ
9. r0 < M
10. r0 ≤ k
11. x : ℝ
12. y : ℝ
13. ((x = ((a * c) + (b * rsqrt(k))/M)) ∧ (y = ((b * c) - a * rsqrt(k)/M)))
∨ ((x = ((a * c) - b * rsqrt(k)/M)) ∧ (y = ((b * c) + (a * rsqrt(k))/M)))
14. ((a * x) + (b * y)) = c
15. r0 < M^2
⊢ ((M^2 * x^2) + (M^2 * y^2)) = (M^2 * r^2)
BY
{ (RepeatFor 2 (D -3)
   THEN (RWO "-3 -4" 0 THENA Auto)
   THEN (RWO "rnexp-rdiv<" 0 THENA Auto)
   THEN (nRNorm 0 THENA Auto)
   THEN ((RWO "rnexp2" 0 THENM nRNorm 0) THENA Auto)
   THEN (RWW  "rmul-assoc rsqrt_squared" 0 THENA Auto)
   THEN (RWW "6< 8<" 0 THENA Auto)
   THEN RWO  "rnexp2" 0
   THEN Auto) }

---

Latex:

---

Latex:

1.  a  :  \mBbbR{}
2.  b  :  \mBbbR{}
3.  c  :  \mBbbR{}
4.  r  :  \mBbbR{}
5.  M  :  \mBbbR{}
6.  (a\^{}2  +  b\^{}2)  =  M
7.  k  :  \mBbbR{}
8.  ((M  *  r\^{}2)  -  c\^{}2)  =  k
9.  r0  <  M
10.  r0  \mleq{}  k
11.  x  :  \mBbbR{}
12.  y  :  \mBbbR{}
13.  ((x  =  ((a  *  c)  +  (b  *  rsqrt(k))/M))  \mwedge{}  (y  =  ((b  *  c)  -  a  *  rsqrt(k)/M)))
\mvee{}  ((x  =  ((a  *  c)  -  b  *  rsqrt(k)/M))  \mwedge{}  (y  =  ((b  *  c)  +  (a  *  rsqrt(k))/M)))
14.  ((a  *  x)  +  (b  *  y))  =  c
15.  r0  <  M\^{}2
\mvdash{}  ((M\^{}2  *  x\^{}2)  +  (M\^{}2  *  y\^{}2))  =  (M\^{}2  *  r\^{}2)


By

---

Latex:
(RepeatFor  2  (D  -3)
  THEN  (RWO  "-3  -4"  0  THENA  Auto)
  THEN  (RWO  "rnexp-rdiv<"  0  THENA  Auto)
  THEN  (nRNorm  0  THENA  Auto)
  THEN  ((RWO  "rnexp2"  0  THENM  nRNorm  0)  THENA  Auto)
  THEN  (RWW    "rmul-assoc  rsqrt\_squared"  0  THENA  Auto)
  THEN  (RWW  "6<  8<"  0  THENA  Auto)
  THEN  RWO    "rnexp2"  0
  THEN  Auto)

---

Home Index