Metamath Proof Explorer

Theorem itsclc0yqe

Description: Lemma for itsclc0 . Quadratic equation for the y-coordinate of the intersection points of an arbitrary line and a circle. This theorem holds even for degenerate lines ( A = B = 0 ). (Contributed by AV, 25-Feb-2023)

Ref Expression
Hypotheses itscnhlc0yqe.q 
|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
itscnhlc0yqe.t 
|- T = -u ( 2 x. ( B x. C ) )
itscnhlc0yqe.u 
|- U = ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) )
Assertion itsclc0yqe 
|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) )

Proof

Step Hyp Ref Expression
1 itscnhlc0yqe.q 
 |-  Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
2 itscnhlc0yqe.t 
 |-  T = -u ( 2 x. ( B x. C ) )
3 itscnhlc0yqe.u 
 |-  U = ( ( C ^ 2 ) - ( ( A ^ 2 ) x. ( R ^ 2 ) ) )
4 simp11 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> A e. RR )
5 4 anim1i 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) /\ A = 0 ) -> ( A e. RR /\ A = 0 ) )
6 5 ancoms 
 |-  ( ( A = 0 /\ ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) ) -> ( A e. RR /\ A = 0 ) )
7 simpr12 
 |-  ( ( A = 0 /\ ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) ) -> B e. RR )
8 simpr13 
 |-  ( ( A = 0 /\ ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) ) -> C e. RR )
9 simpr2 
 |-  ( ( A = 0 /\ ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) ) -> R e. RR+ )
10 simpr3 
 |-  ( ( A = 0 /\ ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) ) -> ( X e. RR /\ Y e. RR ) )
11 1 2 3 itschlc0yqe 
 |-  ( ( ( ( A e. RR /\ A = 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) )
12 6 7 8 9 10 11 syl311anc 
 |-  ( ( A = 0 /\ ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) )
13 12 ex 
 |-  ( A = 0 -> ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) ) )
14 4 anim1i 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) /\ A =/= 0 ) -> ( A e. RR /\ A =/= 0 ) )
15 14 ancoms 
 |-  ( ( A =/= 0 /\ ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) ) -> ( A e. RR /\ A =/= 0 ) )
16 simpr12 
 |-  ( ( A =/= 0 /\ ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) ) -> B e. RR )
17 simpr13 
 |-  ( ( A =/= 0 /\ ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) ) -> C e. RR )
18 simpr2 
 |-  ( ( A =/= 0 /\ ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) ) -> R e. RR+ )
19 simpr3 
 |-  ( ( A =/= 0 /\ ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) ) -> ( X e. RR /\ Y e. RR ) )
20 1 2 3 itscnhlc0yqe 
 |-  ( ( ( ( A e. RR /\ A =/= 0 ) /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) )
21 15 16 17 18 19 20 syl311anc 
 |-  ( ( A =/= 0 /\ ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) )
22 21 ex 
 |-  ( A =/= 0 -> ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) ) )
23 13 22 pm2.61ine 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR+ /\ ( X e. RR /\ Y e. RR ) ) -> ( ( ( ( X ^ 2 ) + ( Y ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. X ) + ( B x. Y ) ) = C ) -> ( ( Q x. ( Y ^ 2 ) ) + ( ( T x. Y ) + U ) ) = 0 ) )