---

Step * 2 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
⊢ (x^2 + y^2) = r^2
BY
{ ((Assert r0 < M^2 BY (RWO "rnexp2" 0 THEN EAuto 1 THEN Auto)) THEN nRMul ⌜M^2⌝ 0⋅) }

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

---

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
\mvdash{}  (x\^{}2  +  y\^{}2)  =  r\^{}2


By

---

Latex:
((Assert  r0  <  M\^{}2  BY  (RWO  "rnexp2"  0  THEN  EAuto  1  THEN  Auto))  THEN  nRMul  \mkleeneopen{}M\^{}2\mkleeneclose{}  0\mcdot{})

---

Home Index