Metamath Proof Explorer

Theorem itsclc0xyqsol

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, 25-Feb-2023)

Ref Expression
Hypotheses itscnhlc0yqe.q 
|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
itsclc0yqsol.d 
|- D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
Assertion itsclc0xyqsol 
|- ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) )

Proof

Step Hyp Ref Expression
1 itscnhlc0yqe.q 
 |-  Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
2 itsclc0yqsol.d 
 |-  D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
3 1 2 itscnhlc0xyqsol 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) )
4 3 3exp 
 |-  ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) -> ( ( R e. RR+ /\ 0 <_ D ) -> ( ( X e. RR /\ Y e. RR ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) ) )
5 4 3exp 
 |-  ( ( A e. RR /\ A =/= 0 ) -> ( B e. RR -> ( C e. RR -> ( ( R e. RR+ /\ 0 <_ D ) -> ( ( X e. RR /\ Y e. RR ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) ) ) ) )
6 5 expcom 
 |-  ( A =/= 0 -> ( A e. RR -> ( B e. RR -> ( C e. RR -> ( ( R e. RR+ /\ 0 <_ D ) -> ( ( X e. RR /\ Y e. RR ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) ) ) ) ) )
7 6 3impd 
 |-  ( A =/= 0 -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( R e. RR+ /\ 0 <_ D ) -> ( ( X e. RR /\ Y e. RR ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) ) ) )
8 nne 
 |-  ( -. A =/= 0 <-> A = 0 )
9 1 2 itschlc0xyqsol 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) )
10 9 3exp 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A = 0 /\ B =/= 0 ) ) -> ( ( R e. RR+ /\ 0 <_ D ) -> ( ( X e. RR /\ Y e. RR ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) ) )
11 10 expcom 
 |-  ( ( A = 0 /\ B =/= 0 ) -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( R e. RR+ /\ 0 <_ D ) -> ( ( X e. RR /\ Y e. RR ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) ) ) )
12 8 11 sylanb 
 |-  ( ( -. A =/= 0 /\ B =/= 0 ) -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( R e. RR+ /\ 0 <_ D ) -> ( ( X e. RR /\ Y e. RR ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) ) ) )
13 7 12 jaoi3 
 |-  ( ( A =/= 0 \/ B =/= 0 ) -> ( ( A e. RR /\ B e. RR /\ C e. RR ) -> ( ( R e. RR+ /\ 0 <_ D ) -> ( ( X e. RR /\ Y e. RR ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) ) ) )
14 13 impcom 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) -> ( ( R e. RR+ /\ 0 <_ D ) -> ( ( X e. RR /\ Y e. RR ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) ) )
15 14 3imp 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( R e. RR+ /\ 0 <_ D ) /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( X = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( X = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ Y = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) )