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=12
itsclinecirc0b.e E=msup
itsclinecirc0b.p P=I
itsclinecirc0b.s S=SphereE
itsclinecirc0b.0 0˙=I×0
itsclinecirc0b.q Q=A2+B2
itsclinecirc0b.d D=R2QC2
itsclinecirc0b.l L=LineME
itsclinecirc0b.a A=X2Y2
itsclinecirc0b.b B=Y1X1
itsclinecirc0b.c C=X2Y1X1Y2
Assertion itsclinecirc0in XPYPXYR+0D0˙SRXLY=1AC+BDQ2BCADQ1ACBDQ2BC+ADQ

Proof

Step Hyp Ref Expression
1 itsclinecirc0b.i I=12
2 itsclinecirc0b.e E=msup
3 itsclinecirc0b.p P=I
4 itsclinecirc0b.s S=SphereE
5 itsclinecirc0b.0 0˙=I×0
6 itsclinecirc0b.q Q=A2+B2
7 itsclinecirc0b.d D=R2QC2
8 itsclinecirc0b.l L=LineME
9 itsclinecirc0b.a A=X2Y2
10 itsclinecirc0b.b B=Y1X1
11 itsclinecirc0b.c C=X2Y1X1Y2
12 elin z0˙SRXLYz0˙SRzXLY
13 1 2 3 4 5 6 7 8 9 10 11 itsclinecirc0b XPYPXYR+0Dz0˙SRzXLYzPz1=AC+BDQz2=BCADQz1=ACBDQz2=BC+ADQ
14 12 13 syl5bb XPYPXYR+0Dz0˙SRXLYzPz1=AC+BDQz2=BCADQz1=ACBDQz2=BC+ADQ
15 1 3 rrx2pyel XPX2
16 15 adantr XPYPX2
17 1 3 rrx2pyel YPY2
18 17 adantl XPYPY2
19 16 18 resubcld XPYPX2Y2
20 9 19 eqeltrid XPYPA
21 20 3adant3 XPYPXYA
22 21 adantr XPYPXYR+0DA
23 1 3 rrx2pxel YPY1
24 23 adantl XPYPY1
25 1 3 rrx2pxel XPX1
26 25 adantr XPYPX1
27 24 26 resubcld XPYPY1X1
28 10 27 eqeltrid XPYPB
29 28 3adant3 XPYPXYB
30 29 adantr XPYPXYR+0DB
31 16 24 remulcld XPYPX2Y1
32 26 18 remulcld XPYPX1Y2
33 31 32 resubcld XPYPX2Y1X1Y2
34 11 33 eqeltrid XPYPC
35 34 3adant3 XPYPXYC
36 35 adantr XPYPXYR+0DC
37 22 30 36 3jca XPYPXYR+0DABC
38 21 29 35 3jca XPYPXYABC
39 rpre R+R
40 39 adantr R+0DR
41 6 7 itsclc0lem3 ABCRD
42 38 40 41 syl2an XPYPXYR+0DD
43 simprr XPYPXYR+0D0D
44 42 43 jca XPYPXYR+0DD0D
45 20 28 jca XPYPAB
46 6 resum2sqcl ABQ
47 45 46 syl XPYPQ
48 47 3adant3 XPYPXYQ
49 1 3 10 9 rrx2pnedifcoorneorr XPYPXYB0A0
50 49 orcomd XPYPXYA0B0
51 6 resum2sqorgt0 ABA0B00<Q
52 21 29 50 51 syl3anc XPYPXY0<Q
53 52 gt0ne0d XPYPXYQ0
54 48 53 jca XPYPXYQQ0
55 54 adantr XPYPXYR+0DQQ0
56 itsclc0lem1 ABCD0DQQ0AC+BDQ
57 37 44 55 56 syl3anc XPYPXYR+0DAC+BDQ
58 30 22 36 3jca XPYPXYR+0DBAC
59 48 adantr XPYPXYR+0DQ
60 53 adantr XPYPXYR+0DQ0
61 59 60 jca XPYPXYR+0DQQ0
62 itsclc0lem2 BACD0DQQ0BCADQ
63 58 44 61 62 syl3anc XPYPXYR+0DBCADQ
64 itsclc0lem2 ABCD0DQQ0ACBDQ
65 37 44 61 64 syl3anc XPYPXYR+0DACBDQ
66 itsclc0lem1 BACD0DQQ0BC+ADQ
67 58 44 61 66 syl3anc XPYPXYR+0DBC+ADQ
68 1 3 prelrrx2b AC+BDQBCADQACBDQBC+ADQzPz1=AC+BDQz2=BCADQz1=ACBDQz2=BC+ADQz1AC+BDQ2BCADQ1ACBDQ2BC+ADQ
69 57 63 65 67 68 syl22anc XPYPXYR+0DzPz1=AC+BDQz2=BCADQz1=ACBDQz2=BC+ADQz1AC+BDQ2BCADQ1ACBDQ2BC+ADQ
70 14 69 bitrd XPYPXYR+0Dz0˙SRXLYz1AC+BDQ2BCADQ1ACBDQ2BC+ADQ
71 70 eqrdv XPYPXYR+0D0˙SRXLY=1AC+BDQ2BCADQ1ACBDQ2BC+ADQ