Metamath Proof Explorer

Theorem itsclinecirc0b

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. (Contributed by AV, 2-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 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 ) ) ) ) ) )

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 eqid 
 |-  ( ( Y ` 2 ) - ( X ` 2 ) ) = ( ( Y ` 2 ) - ( X ` 2 ) )
13 1 2 3 8 10 12 11 rrx2linest 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X L Y ) = { p e. P | ( B x. ( p ` 2 ) ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + C ) } )
14 13 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( X L Y ) = { p e. P | ( B x. ( p ` 2 ) ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + C ) } )
15 eqcom 
 |-  ( ( B x. ( p ` 2 ) ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + C ) <-> ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + C ) = ( B x. ( p ` 2 ) ) )
16 1 3 rrx2pxel 
 |-  ( Y e. P -> ( Y ` 1 ) e. RR )
17 16 adantl 
 |-  ( ( X e. P /\ Y e. P ) -> ( Y ` 1 ) e. RR )
18 1 3 rrx2pxel 
 |-  ( X e. P -> ( X ` 1 ) e. RR )
19 18 adantr 
 |-  ( ( X e. P /\ Y e. P ) -> ( X ` 1 ) e. RR )
20 17 19 resubcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( Y ` 1 ) - ( X ` 1 ) ) e. RR )
21 10 20 eqeltrid 
 |-  ( ( X e. P /\ Y e. P ) -> B e. RR )
22 21 3adant3 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> B e. RR )
23 22 ad2antrr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> B e. RR )
24 1 3 rrx2pyel 
 |-  ( p e. P -> ( p ` 2 ) e. RR )
25 24 adantl 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( p ` 2 ) e. RR )
26 23 25 remulcld 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( B x. ( p ` 2 ) ) e. RR )
27 26 recnd 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( B x. ( p ` 2 ) ) e. CC )
28 1 3 rrx2pyel 
 |-  ( Y e. P -> ( Y ` 2 ) e. RR )
29 28 adantl 
 |-  ( ( X e. P /\ Y e. P ) -> ( Y ` 2 ) e. RR )
30 1 3 rrx2pyel 
 |-  ( X e. P -> ( X ` 2 ) e. RR )
31 30 adantr 
 |-  ( ( X e. P /\ Y e. P ) -> ( X ` 2 ) e. RR )
32 29 31 resubcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) e. RR )
33 32 3adant3 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) e. RR )
34 33 ad2antrr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) e. RR )
35 1 3 rrx2pxel 
 |-  ( p e. P -> ( p ` 1 ) e. RR )
36 35 adantl 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( p ` 1 ) e. RR )
37 34 36 remulcld 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) e. RR )
38 37 recnd 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) e. CC )
39 31 17 remulcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( X ` 2 ) x. ( Y ` 1 ) ) e. RR )
40 19 29 remulcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( X ` 1 ) x. ( Y ` 2 ) ) e. RR )
41 39 40 resubcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( ( X ` 2 ) x. ( Y ` 1 ) ) - ( ( X ` 1 ) x. ( Y ` 2 ) ) ) e. RR )
42 11 41 eqeltrid 
 |-  ( ( X e. P /\ Y e. P ) -> C e. RR )
43 42 recnd 
 |-  ( ( X e. P /\ Y e. P ) -> C e. CC )
44 43 3adant3 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> C e. CC )
45 44 ad2antrr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> C e. CC )
46 27 38 45 subaddd 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( ( ( B x. ( p ` 2 ) ) - ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) ) = C <-> ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + C ) = ( B x. ( p ` 2 ) ) ) )
47 15 46 bitr4id 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( ( B x. ( p ` 2 ) ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + C ) <-> ( ( B x. ( p ` 2 ) ) - ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) ) = C ) )
48 31 29 resubcld 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( X ` 2 ) - ( Y ` 2 ) ) e. RR )
49 9 48 eqeltrid 
 |-  ( ( X e. P /\ Y e. P ) -> A e. RR )
50 49 3adant3 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> A e. RR )
51 50 ad2antrr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> A e. RR )
52 51 36 remulcld 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( A x. ( p ` 1 ) ) e. RR )
53 52 recnd 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( A x. ( p ` 1 ) ) e. CC )
54 53 27 addcomd 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = ( ( B x. ( p ` 2 ) ) + ( A x. ( p ` 1 ) ) ) )
55 29 3adant3 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( Y ` 2 ) e. RR )
56 55 ad2antrr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( Y ` 2 ) e. RR )
57 56 recnd 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( Y ` 2 ) e. CC )
58 31 3adant3 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( X ` 2 ) e. RR )
59 58 ad2antrr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( X ` 2 ) e. RR )
60 59 recnd 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( X ` 2 ) e. CC )
61 57 60 negsubdi2d 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> -u ( ( Y ` 2 ) - ( X ` 2 ) ) = ( ( X ` 2 ) - ( Y ` 2 ) ) )
62 9 61 eqtr4id 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> A = -u ( ( Y ` 2 ) - ( X ` 2 ) ) )
63 62 oveq1d 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( A x. ( p ` 1 ) ) = ( -u ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) )
64 32 recnd 
 |-  ( ( X e. P /\ Y e. P ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) e. CC )
65 64 3adant3 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) e. CC )
66 65 ad2antrr 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( ( Y ` 2 ) - ( X ` 2 ) ) e. CC )
67 36 recnd 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( p ` 1 ) e. CC )
68 66 67 mulneg1d 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( -u ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) = -u ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) )
69 63 68 eqtr2d 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> -u ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) = ( A x. ( p ` 1 ) ) )
70 69 oveq2d 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( ( B x. ( p ` 2 ) ) + -u ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) ) = ( ( B x. ( p ` 2 ) ) + ( A x. ( p ` 1 ) ) ) )
71 27 38 negsubd 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( ( B x. ( p ` 2 ) ) + -u ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) ) = ( ( B x. ( p ` 2 ) ) - ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) ) )
72 54 70 71 3eqtr2rd 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( ( B x. ( p ` 2 ) ) - ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) ) = ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) )
73 72 eqeq1d 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( ( ( B x. ( p ` 2 ) ) - ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) ) = C <-> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C ) )
74 47 73 bitrd 
 |-  ( ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) /\ p e. P ) -> ( ( B x. ( p ` 2 ) ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + C ) <-> ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C ) )
75 74 rabbidva 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> { p e. P | ( B x. ( p ` 2 ) ) = ( ( ( ( Y ` 2 ) - ( X ` 2 ) ) x. ( p ` 1 ) ) + C ) } = { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } )
76 14 75 eqtrd 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( X L Y ) = { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } )
77 76 eleq2d 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( Z e. ( X L Y ) <-> Z e. { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } ) )
78 77 anbi2d 
 |-  ( ( ( 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. ( .0. S R ) /\ Z e. { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } ) ) )
79 50 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> A e. RR )
80 22 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> B e. RR )
81 42 3adant3 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> C e. RR )
82 81 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> C e. RR )
83 1 3 10 9 rrx2pnedifcoorneorr 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( B =/= 0 \/ A =/= 0 ) )
84 83 orcomd 
 |-  ( ( X e. P /\ Y e. P /\ X =/= Y ) -> ( A =/= 0 \/ B =/= 0 ) )
85 84 adantr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( A =/= 0 \/ B =/= 0 ) )
86 simpr 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( R e. RR+ /\ 0 <_ D ) )
87 eqid 
 |-  { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } = { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C }
88 1 2 3 4 5 6 7 87 itsclc0b 
 |-  ( ( ( A e. RR /\ B e. RR /\ C e. RR ) /\ ( A =/= 0 \/ B =/= 0 ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( Z e. ( .0. S R ) /\ Z e. { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } ) <-> ( 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 ) ) ) ) ) )
89 79 80 82 85 86 88 syl311anc 
 |-  ( ( ( X e. P /\ Y e. P /\ X =/= Y ) /\ ( R e. RR+ /\ 0 <_ D ) ) -> ( ( Z e. ( .0. S R ) /\ Z e. { p e. P | ( ( A x. ( p ` 1 ) ) + ( B x. ( p ` 2 ) ) ) = C } ) <-> ( 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 ) ) ) ) ) )
90 78 89 bitrd 
 |-  ( ( ( 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 ) ) ) ) ) )