Metamath Proof Explorer


Theorem itsclc0xyqsolb

Description: Lemma for itsclc0 . Solutions of the quadratic equations for the coordinates of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 2-May-2023) (Revised by AV, 14-May-2023)

Ref Expression
Hypotheses itsclc0xyqsolr.q Q = A 2 + B 2
itsclc0xyqsolr.d D = R 2 Q C 2
Assertion itsclc0xyqsolb A B C A 0 B 0 R + 0 D X Y X 2 + Y 2 = R 2 A X + B Y = C X = A C + B D Q Y = B C A D Q X = A C B D Q Y = B C + A D Q

Proof

Step Hyp Ref Expression
1 itsclc0xyqsolr.q Q = A 2 + B 2
2 itsclc0xyqsolr.d D = R 2 Q C 2
3 1 2 itsclc0xyqsol A B C A 0 B 0 R + 0 D X Y X 2 + Y 2 = R 2 A X + B Y = C X = A C + B D Q Y = B C A D Q X = A C B D Q Y = B C + A D Q
4 3 3expb A B C A 0 B 0 R + 0 D X Y X 2 + Y 2 = R 2 A X + B Y = C X = A C + B D Q Y = B C A D Q X = A C B D Q Y = B C + A D Q
5 simpl A B C A 0 B 0 A B C
6 simpr A B C A 0 B 0 A 0 B 0
7 simpl R + 0 D X Y R + 0 D
8 1 2 itsclc0xyqsolr A B C A 0 B 0 R + 0 D X = A C + B D Q Y = B C A D Q X = A C B D Q Y = B C + A D Q X 2 + Y 2 = R 2 A X + B Y = C
9 5 6 7 8 syl2an3an A B C A 0 B 0 R + 0 D X Y X = A C + B D Q Y = B C A D Q X = A C B D Q Y = B C + A D Q X 2 + Y 2 = R 2 A X + B Y = C
10 4 9 impbid A B C A 0 B 0 R + 0 D X Y X 2 + Y 2 = R 2 A X + B Y = C X = A C + B D Q Y = B C A D Q X = A C B D Q Y = B C + A D Q