Metamath Proof Explorer


Theorem itsclc0b

Description: The intersection points of a (nondegenerate) line through two points and a circle around the origin. (Contributed by AV, 2-May-2023) (Revised by AV, 14-May-2023)

Ref Expression
Hypotheses itsclc0.i I = 1 2
itsclc0.e E = I
itsclc0.p P = I
itsclc0.s S = Sphere E
itsclc0.0 0 ˙ = I × 0
itsclc0.q Q = A 2 + B 2
itsclc0.d D = R 2 Q C 2
itsclc0.l L = p P | A p 1 + B p 2 = C
Assertion itsclc0b A B C A 0 B 0 R + 0 D X 0 ˙ S R X L X P X 1 = A C + B D Q X 2 = B C A D Q X 1 = A C B D Q X 2 = B C + A D Q

Proof

Step Hyp Ref Expression
1 itsclc0.i I = 1 2
2 itsclc0.e E = I
3 itsclc0.p P = I
4 itsclc0.s S = Sphere E
5 itsclc0.0 0 ˙ = I × 0
6 itsclc0.q Q = A 2 + B 2
7 itsclc0.d D = R 2 Q C 2
8 itsclc0.l L = p P | A p 1 + B p 2 = C
9 rprege0 R + R 0 R
10 elrege0 R 0 +∞ R 0 R
11 9 10 sylibr R + R 0 +∞
12 11 adantr R + 0 D R 0 +∞
13 12 3ad2ant3 A B C A 0 B 0 R + 0 D R 0 +∞
14 eqid p P | p 1 2 + p 2 2 = R 2 = p P | p 1 2 + p 2 2 = R 2
15 1 2 3 4 5 14 2sphere0 R 0 +∞ 0 ˙ S R = p P | p 1 2 + p 2 2 = R 2
16 15 eleq2d R 0 +∞ X 0 ˙ S R X p P | p 1 2 + p 2 2 = R 2
17 13 16 syl A B C A 0 B 0 R + 0 D X 0 ˙ S R X p P | p 1 2 + p 2 2 = R 2
18 fveq1 p = X p 1 = X 1
19 18 oveq2d p = X A p 1 = A X 1
20 fveq1 p = X p 2 = X 2
21 20 oveq2d p = X B p 2 = B X 2
22 19 21 oveq12d p = X A p 1 + B p 2 = A X 1 + B X 2
23 22 eqeq1d p = X A p 1 + B p 2 = C A X 1 + B X 2 = C
24 23 8 elrab2 X L X P A X 1 + B X 2 = C
25 24 a1i A B C A 0 B 0 R + 0 D X L X P A X 1 + B X 2 = C
26 17 25 anbi12d A B C A 0 B 0 R + 0 D X 0 ˙ S R X L X p P | p 1 2 + p 2 2 = R 2 X P A X 1 + B X 2 = C
27 18 oveq1d p = X p 1 2 = X 1 2
28 20 oveq1d p = X p 2 2 = X 2 2
29 27 28 oveq12d p = X p 1 2 + p 2 2 = X 1 2 + X 2 2
30 29 eqeq1d p = X p 1 2 + p 2 2 = R 2 X 1 2 + X 2 2 = R 2
31 30 elrab X p P | p 1 2 + p 2 2 = R 2 X P X 1 2 + X 2 2 = R 2
32 31 anbi1i X p P | p 1 2 + p 2 2 = R 2 X P A X 1 + B X 2 = C X P X 1 2 + X 2 2 = R 2 X P A X 1 + B X 2 = C
33 anandi X P X 1 2 + X 2 2 = R 2 A X 1 + B X 2 = C X P X 1 2 + X 2 2 = R 2 X P A X 1 + B X 2 = C
34 simpl1 A B C A 0 B 0 R + 0 D X P A B C
35 simpl2 A B C A 0 B 0 R + 0 D X P A 0 B 0
36 simpl3l A B C A 0 B 0 R + 0 D X P R +
37 simpl3r A B C A 0 B 0 R + 0 D X P 0 D
38 1 3 rrx2pxel X P X 1
39 1 3 rrx2pyel X P X 2
40 38 39 jca X P X 1 X 2
41 40 adantl A B C A 0 B 0 R + 0 D X P X 1 X 2
42 36 37 41 jca31 A B C A 0 B 0 R + 0 D X P R + 0 D X 1 X 2
43 6 7 itsclc0xyqsolb A B C A 0 B 0 R + 0 D X 1 X 2 X 1 2 + X 2 2 = R 2 A X 1 + B X 2 = C X 1 = A C + B D Q X 2 = B C A D Q X 1 = A C B D Q X 2 = B C + A D Q
44 34 35 42 43 syl21anc A B C A 0 B 0 R + 0 D X P X 1 2 + X 2 2 = R 2 A X 1 + B X 2 = C X 1 = A C + B D Q X 2 = B C A D Q X 1 = A C B D Q X 2 = B C + A D Q
45 44 pm5.32da A B C A 0 B 0 R + 0 D X P X 1 2 + X 2 2 = R 2 A X 1 + B X 2 = C X P X 1 = A C + B D Q X 2 = B C A D Q X 1 = A C B D Q X 2 = B C + A D Q
46 33 45 bitr3id A B C A 0 B 0 R + 0 D X P X 1 2 + X 2 2 = R 2 X P A X 1 + B X 2 = C X P X 1 = A C + B D Q X 2 = B C A D Q X 1 = A C B D Q X 2 = B C + A D Q
47 32 46 syl5bb A B C A 0 B 0 R + 0 D X p P | p 1 2 + p 2 2 = R 2 X P A X 1 + B X 2 = C X P X 1 = A C + B D Q X 2 = B C A D Q X 1 = A C B D Q X 2 = B C + A D Q
48 26 47 bitrd A B C A 0 B 0 R + 0 D X 0 ˙ S R X L X P X 1 = A C + B D Q X 2 = B C A D Q X 1 = A C B D Q X 2 = B C + A D Q