---

Step * 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)))
⊢ ((a * x) + (b * y)) = c
BY
{ (nRMul ⌜M⌝ 0⋅
   THEN RepeatFor 2 (D -1)
   THEN (RWO "-1 -2" 0 THENA Auto)
   THEN (nRNorm 0 THENA Auto)
   THEN RWO "6<" 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)))
\mvdash{}  ((a  *  x)  +  (b  *  y))  =  c


By

---

Latex:
(nRMul  \mkleeneopen{}M\mkleeneclose{}  0\mcdot{}
  THEN  RepeatFor  2  (D  -1)
  THEN  (RWO  "-1  -2"  0  THENA  Auto)
  THEN  (nRNorm  0  THENA  Auto)
  THEN  RWO  "6<"  0
  THEN  Auto)

---

Home Index