Metamath Proof Explorer


Theorem itscnhlc0xyqsol

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

Ref Expression
Hypotheses itscnhlc0yqe.q Q=A2+B2
itsclc0yqsol.d D=R2QC2
Assertion itscnhlc0xyqsol AA0BCR+0DXYX2+Y2=R2AX+BY=CX=AC+BDQY=BCADQX=ACBDQY=BC+ADQ

Proof

Step Hyp Ref Expression
1 itscnhlc0yqe.q Q=A2+B2
2 itsclc0yqsol.d D=R2QC2
3 simpl AA0A
4 3 3anim1i AA0BCABC
5 simpr AA0A0
6 5 3ad2ant1 AA0BCA0
7 6 orcd AA0BCA0B0
8 4 7 jca AA0BCABCA0B0
9 8 3anim1i AA0BCR+0DXYABCA0B0R+0DXY
10 1 2 itsclc0yqsol ABCA0B0R+0DXYX2+Y2=R2AX+BY=CY=BCADQY=BC+ADQ
11 9 10 syl AA0BCR+0DXYX2+Y2=R2AX+BY=CY=BCADQY=BC+ADQ
12 11 imp AA0BCR+0DXYX2+Y2=R2AX+BY=CY=BCADQY=BC+ADQ
13 oveq2 Y=BCADQBY=BBCADQ
14 13 oveq2d Y=BCADQAX+BY=AX+BBCADQ
15 14 eqeq1d Y=BCADQAX+BY=CAX+BBCADQ=C
16 simp12 AA0BCR+0DXYB
17 16 recnd AA0BCR+0DXYB
18 simp13 AA0BCR+0DXYC
19 18 recnd AA0BCR+0DXYC
20 17 19 mulcld AA0BCR+0DXYBC
21 simp11l AA0BCR+0DXYA
22 21 recnd AA0BCR+0DXYA
23 rpre R+R
24 23 adantr R+0DR
25 24 adantl AA0BCR+0DR
26 25 resqcld AA0BCR+0DR2
27 simp1l AA0BCA
28 simp2 AA0BCB
29 1 resum2sqcl ABQ
30 27 28 29 syl2anc AA0BCQ
31 30 adantr AA0BCR+0DQ
32 26 31 remulcld AA0BCR+0DR2Q
33 simpl3 AA0BCR+0DC
34 33 resqcld AA0BCR+0DC2
35 32 34 resubcld AA0BCR+0DR2QC2
36 2 35 eqeltrid AA0BCR+0DD
37 36 3adant3 AA0BCR+0DXYD
38 37 recnd AA0BCR+0DXYD
39 38 sqrtcld AA0BCR+0DXYD
40 22 39 mulcld AA0BCR+0DXYAD
41 20 40 subcld AA0BCR+0DXYBCAD
42 30 3ad2ant1 AA0BCR+0DXYQ
43 42 recnd AA0BCR+0DXYQ
44 1 resum2sqgt0 AA0B0<Q
45 44 3adant3 AA0BC0<Q
46 45 gt0ne0d AA0BCQ0
47 46 3ad2ant1 AA0BCR+0DXYQ0
48 17 41 43 47 divassd AA0BCR+0DXYBBCADQ=BBCADQ
49 48 eqcomd AA0BCR+0DXYBBCADQ=BBCADQ
50 49 oveq2d AA0BCR+0DXYAX+BBCADQ=AX+BBCADQ
51 19 43 47 divcan3d AA0BCR+0DXYQCQ=C
52 51 eqcomd AA0BCR+0DXYC=QCQ
53 50 52 eqeq12d AA0BCR+0DXYAX+BBCADQ=CAX+BBCADQ=QCQ
54 43 19 mulcld AA0BCR+0DXYQC
55 17 41 mulcld AA0BCR+0DXYBBCAD
56 54 55 43 47 divsubdird AA0BCR+0DXYQCBBCADQ=QCQBBCADQ
57 56 eqcomd AA0BCR+0DXYQCQBBCADQ=QCBBCADQ
58 57 eqeq1d AA0BCR+0DXYQCQBBCADQ=AXQCBBCADQ=AX
59 54 43 47 divcld AA0BCR+0DXYQCQ
60 55 43 47 divcld AA0BCR+0DXYBBCADQ
61 simp3l AA0BCR+0DXYX
62 61 recnd AA0BCR+0DXYX
63 22 62 mulcld AA0BCR+0DXYAX
64 59 60 63 subadd2d AA0BCR+0DXYQCQBBCADQ=AXAX+BBCADQ=QCQ
65 eqcom QCBBCADQA=XX=QCBBCADQA
66 65 a1i AA0BCR+0DXYQCBBCADQA=XX=QCBBCADQA
67 54 55 subcld AA0BCR+0DXYQCBBCAD
68 67 43 47 divcld AA0BCR+0DXYQCBBCADQ
69 simp11r AA0BCR+0DXYA0
70 68 62 22 69 divmul2d AA0BCR+0DXYQCBBCADQA=XQCBBCADQ=AX
71 67 43 22 47 69 divdiv1d AA0BCR+0DXYQCBBCADQA=QCBBCADQA
72 71 eqeq2d AA0BCR+0DXYX=QCBBCADQAX=QCBBCADQA
73 66 70 72 3bitr3d AA0BCR+0DXYQCBBCADQ=AXX=QCBBCADQA
74 58 64 73 3bitr3d AA0BCR+0DXYAX+BBCADQ=QCQX=QCBBCADQA
75 53 74 bitrd AA0BCR+0DXYAX+BBCADQ=CX=QCBBCADQA
76 15 75 sylan9bbr AA0BCR+0DXYY=BCADQAX+BY=CX=QCBBCADQA
77 1 oveq1i QC=A2+B2C
78 27 recnd AA0BCA
79 78 sqcld AA0BCA2
80 28 recnd AA0BCB
81 80 sqcld AA0BCB2
82 simp3 AA0BCC
83 82 recnd AA0BCC
84 79 81 83 adddird AA0BCA2+B2C=A2C+B2C
85 77 84 eqtrid AA0BCQC=A2C+B2C
86 85 adantr AA0BCR+0DQC=A2C+B2C
87 80 adantr AA0BCR+0DB
88 33 recnd AA0BCR+0DC
89 87 88 mulcld AA0BCR+0DBC
90 78 adantr AA0BCR+0DA
91 36 recnd AA0BCR+0DD
92 91 sqrtcld AA0BCR+0DD
93 90 92 mulcld AA0BCR+0DAD
94 87 89 93 subdid AA0BCR+0DBBCAD=BBCBAD
95 80 80 83 mulassd AA0BCBBC=BBC
96 recn BB
97 96 sqvald BB2=BB
98 97 3ad2ant2 AA0BCB2=BB
99 98 eqcomd AA0BCBB=B2
100 99 oveq1d AA0BCBBC=B2C
101 95 100 eqtr3d AA0BCBBC=B2C
102 101 adantr AA0BCR+0DBBC=B2C
103 87 90 92 mul12d AA0BCR+0DBAD=ABD
104 102 103 oveq12d AA0BCR+0DBBCBAD=B2CABD
105 94 104 eqtrd AA0BCR+0DBBCAD=B2CABD
106 86 105 oveq12d AA0BCR+0DQCBBCAD=A2C+B2C-B2CABD
107 90 sqcld AA0BCR+0DA2
108 107 88 mulcld AA0BCR+0DA2C
109 87 sqcld AA0BCR+0DB2
110 109 88 mulcld AA0BCR+0DB2C
111 108 110 addcomd AA0BCR+0DA2C+B2C=B2C+A2C
112 111 oveq1d AA0BCR+0DA2C+B2C-B2CABD=B2C+A2C-B2CABD
113 87 92 mulcld AA0BCR+0DBD
114 90 113 mulcld AA0BCR+0DABD
115 110 108 114 pnncand AA0BCR+0DB2C+A2C-B2CABD=A2C+ABD
116 106 112 115 3eqtrd AA0BCR+0DQCBBCAD=A2C+ABD
117 116 oveq1d AA0BCR+0DQCBBCADQA=A2C+ABDQA
118 78 sqvald AA0BCA2=AA
119 118 oveq1d AA0BCA2C=AAC
120 78 78 83 mulassd AA0BCAAC=AAC
121 119 120 eqtrd AA0BCA2C=AAC
122 121 adantr AA0BCR+0DA2C=AAC
123 122 oveq1d AA0BCR+0DA2C+ABD=AAC+ABD
124 31 recnd AA0BCR+0DQ
125 124 90 mulcomd AA0BCR+0DQA=AQ
126 123 125 oveq12d AA0BCR+0DA2C+ABDQA=AAC+ABDAQ
127 90 88 mulcld AA0BCR+0DAC
128 90 127 113 adddid AA0BCR+0DAAC+BD=AAC+ABD
129 128 eqcomd AA0BCR+0DAAC+ABD=AAC+BD
130 129 oveq1d AA0BCR+0DAAC+ABDAQ=AAC+BDAQ
131 127 113 addcld AA0BCR+0DAC+BD
132 46 adantr AA0BCR+0DQ0
133 simpl1r AA0BCR+0DA0
134 131 124 90 132 133 divcan5d AA0BCR+0DAAC+BDAQ=AC+BDQ
135 130 134 eqtrd AA0BCR+0DAAC+ABDAQ=AC+BDQ
136 117 126 135 3eqtrd AA0BCR+0DQCBBCADQA=AC+BDQ
137 136 eqeq2d AA0BCR+0DX=QCBBCADQAX=AC+BDQ
138 137 biimpd AA0BCR+0DX=QCBBCADQAX=AC+BDQ
139 138 3adant3 AA0BCR+0DXYX=QCBBCADQAX=AC+BDQ
140 139 adantr AA0BCR+0DXYY=BCADQX=QCBBCADQAX=AC+BDQ
141 76 140 sylbid AA0BCR+0DXYY=BCADQAX+BY=CX=AC+BDQ
142 141 ex AA0BCR+0DXYY=BCADQAX+BY=CX=AC+BDQ
143 142 com23 AA0BCR+0DXYAX+BY=CY=BCADQX=AC+BDQ
144 143 adantld AA0BCR+0DXYX2+Y2=R2AX+BY=CY=BCADQX=AC+BDQ
145 144 imp AA0BCR+0DXYX2+Y2=R2AX+BY=CY=BCADQX=AC+BDQ
146 145 ancrd AA0BCR+0DXYX2+Y2=R2AX+BY=CY=BCADQX=AC+BDQY=BCADQ
147 oveq2 Y=BC+ADQBY=BBC+ADQ
148 147 oveq2d Y=BC+ADQAX+BY=AX+BBC+ADQ
149 148 eqeq1d Y=BC+ADQAX+BY=CAX+BBC+ADQ=C
150 20 40 addcld AA0BCR+0DXYBC+AD
151 17 150 43 47 divassd AA0BCR+0DXYBBC+ADQ=BBC+ADQ
152 151 eqcomd AA0BCR+0DXYBBC+ADQ=BBC+ADQ
153 152 oveq2d AA0BCR+0DXYAX+BBC+ADQ=AX+BBC+ADQ
154 153 52 eqeq12d AA0BCR+0DXYAX+BBC+ADQ=CAX+BBC+ADQ=QCQ
155 17 150 mulcld AA0BCR+0DXYBBC+AD
156 54 155 43 47 divsubdird AA0BCR+0DXYQCBBC+ADQ=QCQBBC+ADQ
157 156 eqcomd AA0BCR+0DXYQCQBBC+ADQ=QCBBC+ADQ
158 157 eqeq1d AA0BCR+0DXYQCQBBC+ADQ=AXQCBBC+ADQ=AX
159 155 43 47 divcld AA0BCR+0DXYBBC+ADQ
160 59 159 63 subadd2d AA0BCR+0DXYQCQBBC+ADQ=AXAX+BBC+ADQ=QCQ
161 eqcom QCBBC+ADQA=XX=QCBBC+ADQA
162 161 a1i AA0BCR+0DXYQCBBC+ADQA=XX=QCBBC+ADQA
163 54 155 subcld AA0BCR+0DXYQCBBC+AD
164 163 43 47 divcld AA0BCR+0DXYQCBBC+ADQ
165 164 62 22 69 divmul2d AA0BCR+0DXYQCBBC+ADQA=XQCBBC+ADQ=AX
166 163 43 22 47 69 divdiv1d AA0BCR+0DXYQCBBC+ADQA=QCBBC+ADQA
167 166 eqeq2d AA0BCR+0DXYX=QCBBC+ADQAX=QCBBC+ADQA
168 162 165 167 3bitr3d AA0BCR+0DXYQCBBC+ADQ=AXX=QCBBC+ADQA
169 158 160 168 3bitr3d AA0BCR+0DXYAX+BBC+ADQ=QCQX=QCBBC+ADQA
170 154 169 bitrd AA0BCR+0DXYAX+BBC+ADQ=CX=QCBBC+ADQA
171 149 170 sylan9bbr AA0BCR+0DXYY=BC+ADQAX+BY=CX=QCBBC+ADQA
172 87 89 93 adddid AA0BCR+0DBBC+AD=BBC+BAD
173 102 103 oveq12d AA0BCR+0DBBC+BAD=B2C+ABD
174 172 173 eqtrd AA0BCR+0DBBC+AD=B2C+ABD
175 86 174 oveq12d AA0BCR+0DQCBBC+AD=A2C+B2C-B2C+ABD
176 111 oveq1d AA0BCR+0DA2C+B2C-B2C+ABD=B2C+A2C-B2C+ABD
177 110 108 114 pnpcand AA0BCR+0DB2C+A2C-B2C+ABD=A2CABD
178 175 176 177 3eqtrd AA0BCR+0DQCBBC+AD=A2CABD
179 178 oveq1d AA0BCR+0DQCBBC+ADQA=A2CABDQA
180 122 oveq1d AA0BCR+0DA2CABD=AACABD
181 180 125 oveq12d AA0BCR+0DA2CABDQA=AACABDAQ
182 90 127 113 subdid AA0BCR+0DAACBD=AACABD
183 182 eqcomd AA0BCR+0DAACABD=AACBD
184 183 oveq1d AA0BCR+0DAACABDAQ=AACBDAQ
185 127 113 subcld AA0BCR+0DACBD
186 185 124 90 132 133 divcan5d AA0BCR+0DAACBDAQ=ACBDQ
187 184 186 eqtrd AA0BCR+0DAACABDAQ=ACBDQ
188 179 181 187 3eqtrd AA0BCR+0DQCBBC+ADQA=ACBDQ
189 188 eqeq2d AA0BCR+0DX=QCBBC+ADQAX=ACBDQ
190 189 biimpd AA0BCR+0DX=QCBBC+ADQAX=ACBDQ
191 190 3adant3 AA0BCR+0DXYX=QCBBC+ADQAX=ACBDQ
192 191 adantr AA0BCR+0DXYY=BC+ADQX=QCBBC+ADQAX=ACBDQ
193 171 192 sylbid AA0BCR+0DXYY=BC+ADQAX+BY=CX=ACBDQ
194 193 ex AA0BCR+0DXYY=BC+ADQAX+BY=CX=ACBDQ
195 194 com23 AA0BCR+0DXYAX+BY=CY=BC+ADQX=ACBDQ
196 195 adantld AA0BCR+0DXYX2+Y2=R2AX+BY=CY=BC+ADQX=ACBDQ
197 196 imp AA0BCR+0DXYX2+Y2=R2AX+BY=CY=BC+ADQX=ACBDQ
198 197 ancrd AA0BCR+0DXYX2+Y2=R2AX+BY=CY=BC+ADQX=ACBDQY=BC+ADQ
199 146 198 orim12d AA0BCR+0DXYX2+Y2=R2AX+BY=CY=BCADQY=BC+ADQX=AC+BDQY=BCADQX=ACBDQY=BC+ADQ
200 12 199 mpd AA0BCR+0DXYX2+Y2=R2AX+BY=CX=AC+BDQY=BCADQX=ACBDQY=BC+ADQ
201 200 ex AA0BCR+0DXYX2+Y2=R2AX+BY=CX=AC+BDQY=BCADQX=ACBDQY=BC+ADQ