---

Step * of Lemma line-circle-intersection-lemma

No Annotations
∀a,b,c,r:ℝ.
  ((r0 < (a^2 + b^2))
  ⇒ (r0 ≤ (((a^2 + b^2) * r^2) - c^2))
  ⇒ (∀x,y:ℝ.
        ((((x = ((a * c) + (b * rsqrt(((a^2 + b^2) * r^2) - c^2))/a^2 + b^2))
        ∧ (y = ((b * c) - a * rsqrt(((a^2 + b^2) * r^2) - c^2)/a^2 + b^2)))
        ∨ ((x = ((a * c) - b * rsqrt(((a^2 + b^2) * r^2) - c^2)/a^2 + b^2))
          ∧ (y = ((b * c) + (a * rsqrt(((a^2 + b^2) * r^2) - c^2))/a^2 + b^2))))
        ⇒ ((((a * x) + (b * y)) = c) ∧ ((x^2 + y^2) = r^2)))))
BY
{ ((RepeatFor 4 (Intro) THEN (GenConcl ⌜(a^2 + b^2) = M ∈ ℝ⌝⋅ THENA Auto))
   THEN (GenConcl ⌜((M * r^2) - c^2) = k ∈ ℝ⌝⋅ THENA Auto)
   THEN Intros
   THEN BetterSplitAndConcl) }

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)))
⊢ ((a * x) + (b * y)) = c

2
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

---

Latex:

---

Latex:
No  Annotations
\mforall{}a,b,c,r:\mBbbR{}.
    ((r0  <  (a\^{}2  +  b\^{}2))
    {}\mRightarrow{}  (r0  \mleq{}  (((a\^{}2  +  b\^{}2)  *  r\^{}2)  -  c\^{}2))
    {}\mRightarrow{}  (\mforall{}x,y:\mBbbR{}.
                ((((x  =  ((a  *  c)  +  (b  *  rsqrt(((a\^{}2  +  b\^{}2)  *  r\^{}2)  -  c\^{}2))/a\^{}2  +  b\^{}2))
                \mwedge{}  (y  =  ((b  *  c)  -  a  *  rsqrt(((a\^{}2  +  b\^{}2)  *  r\^{}2)  -  c\^{}2)/a\^{}2  +  b\^{}2)))
                \mvee{}  ((x  =  ((a  *  c)  -  b  *  rsqrt(((a\^{}2  +  b\^{}2)  *  r\^{}2)  -  c\^{}2)/a\^{}2  +  b\^{}2))
                    \mwedge{}  (y  =  ((b  *  c)  +  (a  *  rsqrt(((a\^{}2  +  b\^{}2)  *  r\^{}2)  -  c\^{}2))/a\^{}2  +  b\^{}2))))
                {}\mRightarrow{}  ((((a  *  x)  +  (b  *  y))  =  c)  \mwedge{}  ((x\^{}2  +  y\^{}2)  =  r\^{}2)))))


By

---

Latex:
((RepeatFor  4  (Intro)  THEN  (GenConcl  \mkleeneopen{}(a\^{}2  +  b\^{}2)  =  M\mkleeneclose{}\mcdot{}  THENA  Auto))
  THEN  (GenConcl  \mkleeneopen{}((M  *  r\^{}2)  -  c\^{}2)  =  k\mkleeneclose{}\mcdot{}  THENA  Auto)
  THEN  Intros
  THEN  BetterSplitAndConcl)

---

Home Index