Metamath Proof Explorer

Theorem itsclinecirc0in

Description: The intersection points of a line through two different points and a circle around the origin, using the definition of a line in a two dimensional Euclidean space, expressed as intersection. (Contributed by AV, 7-May-2023) (Revised by AV, 14-May-2023)

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

Proof

Step Hyp Ref Expression
1 itsclinecirc0b.i 
 |-  I = { 1 , 2 }
2 itsclinecirc0b.e 
 |-  E = ( RR^ ` I )
3 itsclinecirc0b.p 
 |-  P = ( RR ^m I )
4 itsclinecirc0b.s 
 |-  S = ( Sphere ` E )
5 itsclinecirc0b.0 
 |-  .0. = ( I X. { 0 } )
6 itsclinecirc0b.q 
 |-  Q = ( ( A ^ 2 ) + ( B ^ 2 ) )
7 itsclinecirc0b.d 
 |-  D = ( ( ( R ^ 2 ) x. Q ) - ( C ^ 2 ) )
8 itsclinecirc0b.l 
 |-  L = ( LineM ` E )
9 itsclinecirc0b.a 
 |-  A = ( ( X ` 2 ) - ( Y ` 2 ) )
10 itsclinecirc0b.b 
 |-  B = ( ( Y ` 1 ) - ( X ` 1 ) )
11 itsclinecirc0b.c 
 |-  C = ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) )
12 elin 
 |-  ( z e. ( ( .0. S R ) i^i ( X L Y ) ) <-> ( z e. ( .0. S R ) /\ z e. ( X L Y ) ) )
13 1 2 3 4 5 6 7 8 9 10 11 itsclinecirc0b 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( z e. ( .0. S R ) /\ z e. ( X L Y ) ) <-> ( z e. P /\ ( ( ( z ` 1 ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( z ` 2 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( ( z ` 1 ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( z ` 2 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) )
14 12 13 syl5bb 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( z e. ( ( .0. S R ) i^i ( X L Y ) ) <-> ( z e. P /\ ( ( ( z ` 1 ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( z ` 2 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( ( z ` 1 ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( z ` 2 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) )
15 1 3 rrx2pyel 
 |-  ( X e. P -> ( X ` 2 ) e. RR )
16 15 adantr 
 |-  ( ( X e. P /\ Y e. P ) -> ( X ` 2 ) e. RR )
17 1 3 rrx2pyel 
 |-  ( Y e. P -> ( Y ` 2 ) e. RR )
18 17 adantl 
 |-  ( ( X e. P /\ Y e. P ) -> ( Y ` 2 ) e. RR )
19 16 18 resubcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( X ` 2 ) - ( Y ` 2 ) ) e. RR )
20 9 19 eqeltrid 
 |-  ( ( X e. P /\ Y e. P ) -> A e. RR )
21 20 3adant3 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> A e. RR )
22 21 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> A e. RR )
23 1 3 rrx2pxel 
 |-  ( Y e. P -> ( Y ` 1 ) e. RR )
24 23 adantl 
 |-  ( ( X e. P /\ Y e. P ) -> ( Y ` 1 ) e. RR )
25 1 3 rrx2pxel 
 |-  ( X e. P -> ( X ` 1 ) e. RR )
26 25 adantr 
 |-  ( ( X e. P /\ Y e. P ) -> ( X ` 1 ) e. RR )
27 24 26 resubcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( Y ` 1 ) - ( X ` 1 ) ) e. RR )
28 10 27 eqeltrid 
 |-  ( ( X e. P /\ Y e. P ) -> B e. RR )
29 28 3adant3 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> B e. RR )
30 29 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> B e. RR )
31 16 24 remulcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( X ` 2 ) x. ( Y ` 1 ) ) e. RR )
32 26 18 remulcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( X ` 1 ) x. ( Y ` 2 ) ) e. RR )
33 31 32 resubcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) e. RR )
34 11 33 eqeltrid 
 |-  ( ( X e. P /\ Y e. P ) -> C e. RR )
35 34 3adant3 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> C e. RR )
36 35 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> C e. RR )
37 22 30 36 3jca 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A e. RR /\ B e. RR /\ C e. RR ) )
38 21 29 35 3jca 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( A e. RR /\ B e. RR /\ C e. RR ) )
39 rpre 
 |-  ( R e. RR+ -> R e. RR )
40 39 adantr 
 |-  ( ( R e. RR+ /\ 0 <_ D ) -> R e. RR )
41 6 7 itsclc0lem3 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ R e. RR ) -> D e. RR )
42 38 40 41 syl2an 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> D e. RR )
43 simprr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> 0 <_ D )
44 42 43 jca 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( D e. RR /\ 0 <_ D ) )
45 20 28 jca 
 |-  ( ( X e. P /\ Y e. P ) -> ( A e. RR /\ B e. RR ) )
46 6 resum2sqcl 
 |-  ( ( A e. RR /\ B e. RR ) -> Q e. RR )
47 45 46 syl 
 |-  ( ( X e. P /\ Y e. P ) -> Q e. RR )
48 47 3adant3 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> Q e. RR )
49 1 3 10 9 rrx2pnedifcoorneorr 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( B =/= 0 \/ A =/= 0 ) )
50 49 orcomd 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( A =/= 0 \/ B =/= 0 ) )
51 6 resum2sqorgt0 
 |-  ( ( A e. RR /\ B e. RR /\ ( A =/= 0 \/ B =/= 0 ) ) -> 0 < Q )
52 21 29 50 51 syl3anc 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> 0 < Q )
53 52 gt0ne0d 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> Q =/= 0 )
54 48 53 jca 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( Q e. RR /\ Q =/= 0 ) )
55 54 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( Q e. RR /\ Q =/= 0 ) )
56 itsclc0lem1 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( D e. RR /\ 0 <_ D ) /\ ( Q e. RR /\ Q =/= 0 ) ) -> ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) e. RR )
57 37 44 55 56 syl3anc 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) e. RR )
58 30 22 36 3jca 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( B e. RR /\ A e. RR /\ C e. RR ) )
59 48 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> Q e. RR )
60 53 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> Q =/= 0 )
61 59 60 jca 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( Q e. RR /\ Q =/= 0 ) )
62 itsclc0lem2 
 |-  ( ( ( B e. RR /\ A e. RR /\ C e. RR ) /\ ( D e. RR /\ 0 <_ D ) /\ ( Q e. RR /\ Q =/= 0 ) ) -> ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) e. RR )
63 58 44 61 62 syl3anc 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) e. RR )
64 itsclc0lem2 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( D e. RR /\ 0 <_ D ) /\ ( Q e. RR /\ Q =/= 0 ) ) -> ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) e. RR )
65 37 44 61 64 syl3anc 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) e. RR )
66 itsclc0lem1 
 |-  ( ( ( B e. RR /\ A e. RR /\ C e. RR ) /\ ( D e. RR /\ 0 <_ D ) /\ ( Q e. RR /\ Q =/= 0 ) ) -> ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) e. RR )
67 58 44 61 66 syl3anc 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) e. RR )
68 1 3 prelrrx2b 
 |-  ( ( ( ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) e. RR /\ ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) e. RR ) /\ ( ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) e. RR /\ ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) e. RR ) ) -> ( ( z e. P /\ ( ( ( z ` 1 ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( z ` 2 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( ( z ` 1 ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( z ` 2 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) <-> z e. { { <. 1 , ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) >. , <. 2 , ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) >. } , { <. 1 , ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) >. , <. 2 , ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) >. } } ) )
69 57 63 65 67 68 syl22anc 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( z e. P /\ ( ( ( z ` 1 ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( z ` 2 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( ( z ` 1 ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( z ` 2 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) <-> z e. { { <. 1 , ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) >. , <. 2 , ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) >. } , { <. 1 , ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) >. , <. 2 , ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) >. } } ) )
70 14 69 bitrd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( z e. ( ( .0. S R ) i^i ( X L Y ) ) <-> z e. { { <. 1 , ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) >. , <. 2 , ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) >. } , { <. 1 , ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) >. , <. 2 , ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) >. } } ) )
71 70 eqrdv 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( .0. S R ) i^i ( X L Y ) ) = { { <. 1 , ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) >. , <. 2 , ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) >. } , { <. 1 , ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) >. , <. 2 , ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) >. } } )