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 = ( 0 ..^ 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 ` 1 ) - ( Y ` 1 ) )
itsclinecirc0b.b 
|- B = ( ( Y ` 0 ) - ( X ` 0 ) )
itsclinecirc0b.c 
|- C = ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) )
Assertion itsclinecirc0in 
|- ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( .0. S R ) i^i ( X L Y ) ) = { <" ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) "> , <" ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) "> } )

Proof

Step Hyp Ref Expression
1 itsclinecirc0b.i 
 |-  I = ( 0 ..^ 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 ` 1 ) - ( Y ` 1 ) )
10 itsclinecirc0b.b 
 |-  B = ( ( Y ` 0 ) - ( X ` 0 ) )
11 itsclinecirc0b.c 
 |-  C = ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) )
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 ` 0 ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( z ` 1 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( ( z ` 0 ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( z ` 1 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) )
14 12 13 bitrid 
 |-  ( ( ( 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 ` 0 ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( z ` 1 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( ( z ` 0 ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( z ` 1 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) ) )
15 1 3 rrx2pyel 
 |-  ( X e. P -> ( X ` 1 ) e. RR )
16 15 adantr 
 |-  ( ( X e. P /\ Y e. P ) -> ( X ` 1 ) e. RR )
17 1 3 rrx2pyel 
 |-  ( Y e. P -> ( Y ` 1 ) e. RR )
18 17 adantl 
 |-  ( ( X e. P /\ Y e. P ) -> ( Y ` 1 ) e. RR )
19 16 18 resubcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( X ` 1 ) - ( Y ` 1 ) ) 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 ` 0 ) e. RR )
24 23 adantl 
 |-  ( ( X e. P /\ Y e. P ) -> ( Y ` 0 ) e. RR )
25 1 3 rrx2pxel 
 |-  ( X e. P -> ( X ` 0 ) e. RR )
26 25 adantr 
 |-  ( ( X e. P /\ Y e. P ) -> ( X ` 0 ) e. RR )
27 24 26 resubcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( Y ` 0 ) - ( X ` 0 ) ) 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 ` 1 ) x. ( Y ` 0 ) ) e. RR )
32 26 18 remulcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( X ` 0 ) x. ( Y ` 1 ) ) e. RR )
33 31 32 resubcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( X ` 1 ) x. ( Y ` 0 ) ) - ( ( X ` 0 ) x. ( Y ` 1 ) ) ) 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 6 resum2sqcl 
 |-  ( ( A e. RR /\ B e. RR ) -> Q e. RR )
46 20 28 45 syl2anc 
 |-  ( ( X e. P /\ Y e. P ) -> Q e. RR )
47 46 3adant3 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> Q e. RR )
48 1 3 10 9 rrx2pnedifcoorneorr 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( B =/= 0 \/ A =/= 0 ) )
49 48 orcomd 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( A =/= 0 \/ B =/= 0 ) )
50 6 resum2sqorgt0 
 |-  ( ( A e. RR /\ B e. RR /\ ( A =/= 0 \/ B =/= 0 ) ) -> 0 < Q )
51 21 29 49 50 syl3anc 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> 0 < Q )
52 51 gt0ne0d 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> Q =/= 0 )
53 47 52 jca 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( Q e. RR /\ Q =/= 0 ) )
54 53 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( Q e. RR /\ Q =/= 0 ) )
55 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 )
56 37 44 54 55 syl3anc 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) e. RR )
57 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 ) )
58 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 )
59 57 44 54 58 syl3anc 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) e. RR )
60 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 )
61 37 44 54 60 syl3anc 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) e. RR )
62 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 )
63 57 44 54 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 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 ` 0 ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( z ` 1 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( ( z ` 0 ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( z ` 1 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) <-> z e. { <" ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) "> , <" ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) "> } ) )
65 56 59 61 63 64 syl22anc 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( z e. P /\ ( ( ( z ` 0 ) = ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( z ` 1 ) = ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) ) \/ ( ( z ` 0 ) = ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) /\ ( z ` 1 ) = ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) ) ) ) <-> z e. { <" ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) "> , <" ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) "> } ) )
66 14 65 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. { <" ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) "> , <" ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) "> } ) )
67 66 eqrdv 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( .0. S R ) i^i ( X L Y ) ) = { <" ( ( ( A x. C ) + ( B x. ( sqrt ` D ) ) ) / Q ) ( ( ( B x. C ) - ( A x. ( sqrt ` D ) ) ) / Q ) "> , <" ( ( ( A x. C ) - ( B x. ( sqrt ` D ) ) ) / Q ) ( ( ( B x. C ) + ( A x. ( sqrt ` D ) ) ) / Q ) "> } )