Metamath Proof Explorer


Theorem itschlc0xyqsol

Description: Lemma for itsclc0 . Solutions of the quadratic equations for the coordinates of the intersection points of a horizontal line and a circle. (Contributed by AV, 8-Feb-2023)

Ref Expression
Hypotheses itscnhlc0yqe.q Q = A 2 + B 2
itsclc0yqsol.d D = R 2 Q C 2
Assertion itschlc0xyqsol A B C A = 0 B 0 R + 0 D X Y X 2 + Y 2 = R 2 A X + B Y = C X = A C + B D Q Y = B C A D Q X = A C B D Q Y = B C + A D Q

Proof

Step Hyp Ref Expression
1 itscnhlc0yqe.q Q = A 2 + B 2
2 itsclc0yqsol.d D = R 2 Q C 2
3 1 2 itschlc0xyqsol1 A B C A = 0 B 0 R + 0 D X Y X 2 + Y 2 = R 2 A X + B Y = C Y = C B X = D B X = D B
4 orcom X = D B X = D B X = D B X = D B
5 oveq1 A = 0 A C = 0 C
6 5 ad2antrl A B C A = 0 B 0 A C = 0 C
7 6 adantr A B C A = 0 B 0 R + 0 D A C = 0 C
8 simpll3 A B C A = 0 B 0 R + 0 D C
9 8 recnd A B C A = 0 B 0 R + 0 D C
10 9 mul02d A B C A = 0 B 0 R + 0 D 0 C = 0
11 7 10 eqtrd A B C A = 0 B 0 R + 0 D A C = 0
12 11 oveq1d A B C A = 0 B 0 R + 0 D A C + B D = 0 + B D
13 simpll2 A B C A = 0 B 0 R + 0 D B
14 13 recnd A B C A = 0 B 0 R + 0 D B
15 rpre R + R
16 15 adantr R + 0 D R
17 16 recnd R + 0 D R
18 17 adantl A B C A = 0 B 0 R + 0 D R
19 18 sqcld A B C A = 0 B 0 R + 0 D R 2
20 1 resum2sqcl A B Q
21 20 recnd A B Q
22 21 3adant3 A B C Q
23 22 adantr A B C A = 0 B 0 Q
24 23 adantr A B C A = 0 B 0 R + 0 D Q
25 19 24 mulcld A B C A = 0 B 0 R + 0 D R 2 Q
26 9 sqcld A B C A = 0 B 0 R + 0 D C 2
27 25 26 subcld A B C A = 0 B 0 R + 0 D R 2 Q C 2
28 2 27 eqeltrid A B C A = 0 B 0 R + 0 D D
29 28 sqrtcld A B C A = 0 B 0 R + 0 D D
30 14 29 mulcld A B C A = 0 B 0 R + 0 D B D
31 30 addid2d A B C A = 0 B 0 R + 0 D 0 + B D = B D
32 12 31 eqtrd A B C A = 0 B 0 R + 0 D A C + B D = B D
33 32 oveq1d A B C A = 0 B 0 R + 0 D A C + B D Q = B D Q
34 sq0i A = 0 A 2 = 0
35 34 ad2antrl A B C A = 0 B 0 A 2 = 0
36 35 oveq1d A B C A = 0 B 0 A 2 + B 2 = 0 + B 2
37 simp2 A B C B
38 37 recnd A B C B
39 38 sqcld A B C B 2
40 39 addid2d A B C 0 + B 2 = B 2
41 38 sqvald A B C B 2 = B B
42 40 41 eqtrd A B C 0 + B 2 = B B
43 42 adantr A B C A = 0 B 0 0 + B 2 = B B
44 36 43 eqtrd A B C A = 0 B 0 A 2 + B 2 = B B
45 1 44 syl5eq A B C A = 0 B 0 Q = B B
46 45 adantr A B C A = 0 B 0 R + 0 D Q = B B
47 46 oveq2d A B C A = 0 B 0 R + 0 D B D Q = B D B B
48 simplrr A B C A = 0 B 0 R + 0 D B 0
49 29 14 14 48 48 divcan5d A B C A = 0 B 0 R + 0 D B D B B = D B
50 47 49 eqtrd A B C A = 0 B 0 R + 0 D B D Q = D B
51 33 50 eqtrd A B C A = 0 B 0 R + 0 D A C + B D Q = D B
52 51 3adant3 A B C A = 0 B 0 R + 0 D X Y A C + B D Q = D B
53 52 adantr A B C A = 0 B 0 R + 0 D X Y Y = C B A C + B D Q = D B
54 53 eqcomd A B C A = 0 B 0 R + 0 D X Y Y = C B D B = A C + B D Q
55 54 eqeq2d A B C A = 0 B 0 R + 0 D X Y Y = C B X = D B X = A C + B D Q
56 55 biimpd A B C A = 0 B 0 R + 0 D X Y Y = C B X = D B X = A C + B D Q
57 oveq1 A = 0 A D = 0 D
58 57 ad2antrl A B C A = 0 B 0 A D = 0 D
59 58 adantr A B C A = 0 B 0 R + 0 D A D = 0 D
60 29 mul02d A B C A = 0 B 0 R + 0 D 0 D = 0
61 59 60 eqtrd A B C A = 0 B 0 R + 0 D A D = 0
62 61 oveq2d A B C A = 0 B 0 R + 0 D B C A D = B C 0
63 14 9 mulcld A B C A = 0 B 0 R + 0 D B C
64 63 subid1d A B C A = 0 B 0 R + 0 D B C 0 = B C
65 62 64 eqtrd A B C A = 0 B 0 R + 0 D B C A D = B C
66 65 46 oveq12d A B C A = 0 B 0 R + 0 D B C A D Q = B C B B
67 66 3adant3 A B C A = 0 B 0 R + 0 D X Y B C A D Q = B C B B
68 9 3adant3 A B C A = 0 B 0 R + 0 D X Y C
69 14 3adant3 A B C A = 0 B 0 R + 0 D X Y B
70 simp1rr A B C A = 0 B 0 R + 0 D X Y B 0
71 68 69 69 70 70 divcan5d A B C A = 0 B 0 R + 0 D X Y B C B B = C B
72 67 71 eqtr2d A B C A = 0 B 0 R + 0 D X Y C B = B C A D Q
73 72 eqeq2d A B C A = 0 B 0 R + 0 D X Y Y = C B Y = B C A D Q
74 73 biimpa A B C A = 0 B 0 R + 0 D X Y Y = C B Y = B C A D Q
75 56 74 jctird A B C A = 0 B 0 R + 0 D X Y Y = C B X = D B X = A C + B D Q Y = B C A D Q
76 14 29 mulneg2d A B C A = 0 B 0 R + 0 D B D = B D
77 76 eqcomd A B C A = 0 B 0 R + 0 D B D = B D
78 77 46 oveq12d A B C A = 0 B 0 R + 0 D B D Q = B D B B
79 29 negcld A B C A = 0 B 0 R + 0 D D
80 79 14 14 48 48 divcan5d A B C A = 0 B 0 R + 0 D B D B B = D B
81 78 80 eqtrd A B C A = 0 B 0 R + 0 D B D Q = D B
82 11 oveq1d A B C A = 0 B 0 R + 0 D A C B D = 0 B D
83 df-neg B D = 0 B D
84 82 83 eqtr4di A B C A = 0 B 0 R + 0 D A C B D = B D
85 84 oveq1d A B C A = 0 B 0 R + 0 D A C B D Q = B D Q
86 29 14 48 divnegd A B C A = 0 B 0 R + 0 D D B = D B
87 81 85 86 3eqtr4d A B C A = 0 B 0 R + 0 D A C B D Q = D B
88 87 3adant3 A B C A = 0 B 0 R + 0 D X Y A C B D Q = D B
89 88 adantr A B C A = 0 B 0 R + 0 D X Y Y = C B A C B D Q = D B
90 89 eqcomd A B C A = 0 B 0 R + 0 D X Y Y = C B D B = A C B D Q
91 90 eqeq2d A B C A = 0 B 0 R + 0 D X Y Y = C B X = D B X = A C B D Q
92 91 biimpd A B C A = 0 B 0 R + 0 D X Y Y = C B X = D B X = A C B D Q
93 58 3ad2ant1 A B C A = 0 B 0 R + 0 D X Y A D = 0 D
94 17 3ad2ant2 A B C A = 0 B 0 R + 0 D X Y R
95 94 sqcld A B C A = 0 B 0 R + 0 D X Y R 2
96 23 3ad2ant1 A B C A = 0 B 0 R + 0 D X Y Q
97 95 96 mulcld A B C A = 0 B 0 R + 0 D X Y R 2 Q
98 simp1l3 A B C A = 0 B 0 R + 0 D X Y C
99 98 recnd A B C A = 0 B 0 R + 0 D X Y C
100 99 sqcld A B C A = 0 B 0 R + 0 D X Y C 2
101 97 100 subcld A B C A = 0 B 0 R + 0 D X Y R 2 Q C 2
102 2 101 eqeltrid A B C A = 0 B 0 R + 0 D X Y D
103 102 sqrtcld A B C A = 0 B 0 R + 0 D X Y D
104 103 mul02d A B C A = 0 B 0 R + 0 D X Y 0 D = 0
105 93 104 eqtrd A B C A = 0 B 0 R + 0 D X Y A D = 0
106 105 oveq2d A B C A = 0 B 0 R + 0 D X Y B C + A D = B C + 0
107 simp1l2 A B C A = 0 B 0 R + 0 D X Y B
108 107 recnd A B C A = 0 B 0 R + 0 D X Y B
109 108 99 mulcld A B C A = 0 B 0 R + 0 D X Y B C
110 109 addid1d A B C A = 0 B 0 R + 0 D X Y B C + 0 = B C
111 106 110 eqtrd A B C A = 0 B 0 R + 0 D X Y B C + A D = B C
112 45 3ad2ant1 A B C A = 0 B 0 R + 0 D X Y Q = B B
113 111 112 oveq12d A B C A = 0 B 0 R + 0 D X Y B C + A D Q = B C B B
114 99 108 108 70 70 divcan5d A B C A = 0 B 0 R + 0 D X Y B C B B = C B
115 113 114 eqtr2d A B C A = 0 B 0 R + 0 D X Y C B = B C + A D Q
116 115 eqeq2d A B C A = 0 B 0 R + 0 D X Y Y = C B Y = B C + A D Q
117 116 biimpa A B C A = 0 B 0 R + 0 D X Y Y = C B Y = B C + A D Q
118 92 117 jctird A B C A = 0 B 0 R + 0 D X Y Y = C B X = D B X = A C B D Q Y = B C + A D Q
119 75 118 orim12d A B C A = 0 B 0 R + 0 D X Y Y = C B X = D B X = D B X = A C + B D Q Y = B C A D Q X = A C B D Q Y = B C + A D Q
120 4 119 syl5bi A B C A = 0 B 0 R + 0 D X Y Y = C B X = D B X = D B X = A C + B D Q Y = B C A D Q X = A C B D Q Y = B C + A D Q
121 120 expimpd A B C A = 0 B 0 R + 0 D X Y Y = C B X = D B X = D B X = A C + B D Q Y = B C A D Q X = A C B D Q Y = B C + A D Q
122 3 121 syld A B C A = 0 B 0 R + 0 D X Y X 2 + Y 2 = R 2 A X + B Y = C X = A C + B D Q Y = B C A D Q X = A C B D Q Y = B C + A D Q