Metamath Proof Explorer

Theorem itsclc0b

Description: The intersection points of a (nondegenerate) line through two points and a circle around the origin. (Contributed by AV, 2-May-2023) (Revised by AV, 14-May-2023)

Ref Expression
Hypotheses itsclc0.i 
|- I = { 1 , 2 }
itsclc0.e 
|- E = ( RR^ ` I )
itsclc0.p 
|- P = ( RR ^m I )
itsclc0.s 
|- S = ( Sphere ` E )
itsclc0.0 
|- .0. = ( I X. { 0 } )
itsclc0.q 
|- Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
itsclc0.d 
|- D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
itsclc0.l 
|- L = { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C }
Assertion itsclc0b 
|- ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( X e. ( .0. S R ) /\ X e. L ) <-> ( X e. P /\ ( ( ( X ` 1 ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( X ` 2 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( ( X ` 1 ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( X ` 2 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 itsclc0.i 
 |-  I = { 1 , 2 }
2 itsclc0.e 
 |-  E = ( RR^ ` I )
3 itsclc0.p 
 |-  P = ( RR ^m I )
4 itsclc0.s 
 |-  S = ( Sphere ` E )
5 itsclc0.0 
 |-  .0. = ( I X. { 0 } )
6 itsclc0.q 
 |-  Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
7 itsclc0.d 
 |-  D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
8 itsclc0.l 
 |-  L = { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C }
9 rprege0 
 |-  ( R e. RR+ -> ( R e. RR /\ 0 <_ R ) )
10 elrege0 
 |-  ( R e. ( 0 [,) +oo ) <-> ( R e. RR /\ 0 <_ R ) )
11 9 10 sylibr 
 |-  ( R e. RR+ -> R e. ( 0 [,) +oo ) )
12 11 adantr 
 |-  ( ( R e. RR+ /\ 0 <_ D ) -> R e. ( 0 [,) +oo ) )
13 12 3ad2ant3 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> R e. ( 0 [,) +oo ) )
14 eqid 
 |-  { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } = { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) }
15 1 2 3 4 5 14 2sphere0 
 |-  ( R e. ( 0 [,) +oo ) -> ( .0. S R ) = { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } )
16 15 eleq2d 
 |-  ( R e. ( 0 [,) +oo ) -> ( X e. ( .0. S R ) <-> X e. { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } ) )
17 13 16 syl 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( X e. ( .0. S R ) <-> X e. { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } ) )
18 fveq1 
 |-  ( p = X -> ( p ` 1 ) = ( X ` 1 ) )
19 18 oveq2d 
 |-  ( p = X -> ( A x. ( p ` 1 ) ) = ( A x. ( X ` 1 ) ) )
20 fveq1 
 |-  ( p = X -> ( p ` 2 ) = ( X ` 2 ) )
21 20 oveq2d 
 |-  ( p = X -> ( B x. ( p ` 2 ) ) = ( B x. ( X ` 2 ) ) )
22 19 21 oveq12d 
 |-  ( p = X -> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = ( ( A x. ( X ` 1 ) ) + ( B x. ( X ` 2 ) ) ) )
23 22 eqeq1d 
 |-  ( p = X -> ( ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C <-> ( ( A x. ( X ` 1 ) ) + ( B x. ( X ` 2 ) ) ) = C ) )
24 23 8 elrab2 
 |-  ( X e. L <-> ( X e. P /\ ( ( A x. ( X ` 1 ) ) + ( B x. ( X ` 2 ) ) ) = C ) )
25 24 a1i 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( X e. L <-> ( X e. P /\ ( ( A x. ( X ` 1 ) ) + ( B x. ( X ` 2 ) ) ) = C ) ) )
26 17 25 anbi12d 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( X e. ( .0. S R ) /\ X e. L ) <-> ( X e. { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } /\ ( X e. P /\ ( ( A x. ( X ` 1 ) ) + ( B x. ( X ` 2 ) ) ) = C ) ) ) )
27 18 oveq1d 
 |-  ( p = X -> ( ( p ` 1 ) ^ 2 ) = ( ( X ` 1 ) ^ 2 ) )
28 20 oveq1d 
 |-  ( p = X -> ( ( p ` 2 ) ^ 2 ) = ( ( X ` 2 ) ^ 2 ) )
29 27 28 oveq12d 
 |-  ( p = X -> ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) )
30 29 eqeq1d 
 |-  ( p = X -> ( ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) <-> ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) = ( R ^ 2 ) ) )
31 30 elrab 
 |-  ( X e. { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } <-> ( X e. P /\ ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) = ( R ^ 2 ) ) )
32 31 anbi1i 
 |-  ( ( X e. { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } /\ ( X e. P /\ ( ( A x. ( X ` 1 ) ) + ( B x. ( X ` 2 ) ) ) = C ) ) <-> ( ( X e. P /\ ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) = ( R ^ 2 ) ) /\ ( X e. P /\ ( ( A x. ( X ` 1 ) ) + ( B x. ( X ` 2 ) ) ) = C ) ) )
33 anandi 
 |-  ( ( X e. P /\ ( ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. ( X ` 1 ) ) + ( B x. ( X ` 2 ) ) ) = C ) ) <-> ( ( X e. P /\ ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) = ( R ^ 2 ) ) /\ ( X e. P /\ ( ( A x. ( X ` 1 ) ) + ( B x. ( X ` 2 ) ) ) = C ) ) )
34 simpl1 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ X e. P ) -> ( A e. RR /\ B e. RR /\ C e. RR ) )
35 simpl2 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ X e. P ) -> ( A =/= 0 \/ B =/= 0 ) )
36 simpl3l 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ X e. P ) -> R e. RR+ )
37 simpl3r 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ X e. P ) -> 0 <_ D )
38 1 3 rrx2pxel 
 |-  ( X e. P -> ( X ` 1 ) e. RR )
39 1 3 rrx2pyel 
 |-  ( X e. P -> ( X ` 2 ) e. RR )
40 38 39 jca 
 |-  ( X e. P -> ( ( X ` 1 ) e. RR /\ ( X ` 2 ) e. RR ) )
41 40 adantl 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ X e. P ) -> ( ( X ` 1 ) e. RR /\ ( X ` 2 ) e. RR ) )
42 36 37 41 jca31 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ X e. P ) -> ( ( R e. RR+ /\ 0 <_ D ) /\ ( ( X ` 1 ) e. RR /\ ( X ` 2 ) e. RR ) ) )
43 6 7 itsclc0xyqsolb 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) ) /\ ( ( R e. RR+ /\ 0 <_ D ) /\ ( ( X ` 1 ) e. RR /\ ( X ` 2 ) e. RR ) ) ) -> ( ( ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. ( X ` 1 ) ) + ( B x. ( X ` 2 ) ) ) = C ) <-> ( ( ( X ` 1 ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( X ` 2 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( ( X ` 1 ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( X ` 2 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) )
44 34 35 42 43 syl21anc 
 |-  ( ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ X e. P ) -> ( ( ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. ( X ` 1 ) ) + ( B x. ( X ` 2 ) ) ) = C ) <-> ( ( ( X ` 1 ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( X ` 2 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( ( X ` 1 ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( X ` 2 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) )
45 44 pm5.32da 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( X e. P /\ ( ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) = ( R ^ 2 ) /\ ( ( A x. ( X ` 1 ) ) + ( B x. ( X ` 2 ) ) ) = C ) ) <-> ( X e. P /\ ( ( ( X ` 1 ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( X ` 2 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( ( X ` 1 ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( X ` 2 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) )
46 33 45 bitr3id 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( X e. P /\ ( ( ( X ` 1 ) ^ 2 ) + ( ( X ` 2 ) ^ 2 ) ) = ( R ^ 2 ) ) /\ ( X e. P /\ ( ( A x. ( X ` 1 ) ) + ( B x. ( X ` 2 ) ) ) = C ) ) <-> ( X e. P /\ ( ( ( X ` 1 ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( X ` 2 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( ( X ` 1 ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( X ` 2 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) )
47 32 46 bitrid 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( X e. { p e. P | ( ( ( p ` 1 ) ^ 2 ) + ( ( p ` 2 ) ^ 2 ) ) = ( R ^ 2 ) } /\ ( X e. P /\ ( ( A x. ( X ` 1 ) ) + ( B x. ( X ` 2 ) ) ) = C ) ) <-> ( X e. P /\ ( ( ( X ` 1 ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( X ` 2 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( ( X ` 1 ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( X ` 2 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) )
48 26 47 bitrd 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( X e. ( .0. S R ) /\ X e. L ) <-> ( X e. P /\ ( ( ( X ` 1 ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( X ` 2 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( ( X ` 1 ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( X ` 2 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) )