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 = I
itsclinecirc0b.p P = I
itsclinecirc0b.s S = Sphere E
itsclinecirc0b.0 0 ˙ = I × 0
itsclinecirc0b.q Q = A 2 + B 2
itsclinecirc0b.d D = R 2 Q C 2
itsclinecirc0b.l L = Line M E
itsclinecirc0b.a A = X 2 Y 2
itsclinecirc0b.b B = Y 1 X 1
itsclinecirc0b.c C = X 2 Y 1 X 1 Y 2
Assertion itsclinecirc0in X P Y P X Y R + 0 D 0 ˙ S R X L Y = 1 A C + B D Q 2 B C A D Q 1 A C B D Q 2 B C + A D Q

Proof

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