Metamath Proof Explorer


Theorem itsclc0yqsol

Description: Lemma for itsclc0 . Solutions of the quadratic equations for the y-coordinate of the intersection points of a (nondegenerate) line and a circle. (Contributed by AV, 7-Feb-2023)

Ref Expression
Hypotheses itscnhlc0yqe.q Q = A 2 + B 2
itsclc0yqsol.d D = R 2 Q C 2
Assertion itsclc0yqsol A B C A 0 B 0 R + 0 D X Y X 2 + Y 2 = R 2 A X + B Y = C Y = B C A 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 eqid 2 B C = 2 B C
4 eqid C 2 A 2 R 2 = C 2 A 2 R 2
5 1 3 4 itsclc0yqe A B C R + X Y X 2 + Y 2 = R 2 A X + B Y = C Q Y 2 + 2 B C Y + C 2 A 2 R 2 = 0
6 5 3adant1r A B C A 0 B 0 R + X Y X 2 + Y 2 = R 2 A X + B Y = C Q Y 2 + 2 B C Y + C 2 A 2 R 2 = 0
7 6 3adant2r A B C A 0 B 0 R + 0 D X Y X 2 + Y 2 = R 2 A X + B Y = C Q Y 2 + 2 B C Y + C 2 A 2 R 2 = 0
8 3simpa A B C A B
9 8 adantr A B C A 0 B 0 A B
10 1 resum2sqcl A B Q
11 9 10 syl A B C A 0 B 0 Q
12 11 3ad2ant1 A B C A 0 B 0 R + 0 D X Y Q
13 12 recnd A B C A 0 B 0 R + 0 D X Y Q
14 simpr1 A 0 A B C A
15 simpl A 0 A B C A 0
16 simpr2 A 0 A B C B
17 1 resum2sqgt0 A A 0 B 0 < Q
18 14 15 16 17 syl21anc A 0 A B C 0 < Q
19 18 ex A 0 A B C 0 < Q
20 simpr2 B 0 A B C B
21 simpl B 0 A B C B 0
22 simpr1 B 0 A B C A
23 eqid B 2 + A 2 = B 2 + A 2
24 23 resum2sqgt0 B B 0 A 0 < B 2 + A 2
25 20 21 22 24 syl21anc B 0 A B C 0 < B 2 + A 2
26 simp1 A B C A
27 26 recnd A B C A
28 27 sqcld A B C A 2
29 simp2 A B C B
30 29 recnd A B C B
31 30 sqcld A B C B 2
32 28 31 addcomd A B C A 2 + B 2 = B 2 + A 2
33 32 adantl B 0 A B C A 2 + B 2 = B 2 + A 2
34 1 33 syl5eq B 0 A B C Q = B 2 + A 2
35 25 34 breqtrrd B 0 A B C 0 < Q
36 35 ex B 0 A B C 0 < Q
37 19 36 jaoi A 0 B 0 A B C 0 < Q
38 37 impcom A B C A 0 B 0 0 < Q
39 38 gt0ne0d A B C A 0 B 0 Q 0
40 39 3ad2ant1 A B C A 0 B 0 R + 0 D X Y Q 0
41 2cnd A B C A 0 B 0 R + 0 D X Y 2
42 recn B B
43 42 3ad2ant2 A B C B
44 43 adantr A B C A 0 B 0 B
45 44 3ad2ant1 A B C A 0 B 0 R + 0 D X Y B
46 recn C C
47 46 3ad2ant3 A B C C
48 47 adantr A B C A 0 B 0 C
49 48 3ad2ant1 A B C A 0 B 0 R + 0 D X Y C
50 45 49 mulcld A B C A 0 B 0 R + 0 D X Y B C
51 41 50 mulcld A B C A 0 B 0 R + 0 D X Y 2 B C
52 51 negcld A B C A 0 B 0 R + 0 D X Y 2 B C
53 49 sqcld A B C A 0 B 0 R + 0 D X Y C 2
54 recn A A
55 54 3ad2ant1 A B C A
56 55 adantr A B C A 0 B 0 A
57 56 3ad2ant1 A B C A 0 B 0 R + 0 D X Y A
58 57 sqcld A B C A 0 B 0 R + 0 D X Y A 2
59 simpl R + 0 D R +
60 59 rpcnd R + 0 D R
61 60 3ad2ant2 A B C A 0 B 0 R + 0 D X Y R
62 61 sqcld A B C A 0 B 0 R + 0 D X Y R 2
63 58 62 mulcld A B C A 0 B 0 R + 0 D X Y A 2 R 2
64 53 63 subcld A B C A 0 B 0 R + 0 D X Y C 2 A 2 R 2
65 recn Y Y
66 65 adantl X Y Y
67 66 3ad2ant3 A B C A 0 B 0 R + 0 D X Y Y
68 eqidd A B C A 0 B 0 R + 0 D X Y 2 B C 2 4 Q C 2 A 2 R 2 = 2 B C 2 4 Q C 2 A 2 R 2
69 13 40 52 64 67 68 quad A B C A 0 B 0 R + 0 D X Y Q Y 2 + 2 B C Y + C 2 A 2 R 2 = 0 Y = - 2 B C + 2 B C 2 4 Q C 2 A 2 R 2 2 Q Y = - 2 B C - 2 B C 2 4 Q C 2 A 2 R 2 2 Q
70 54 abscld A A
71 70 recnd A A
72 71 3ad2ant1 A B C A
73 72 adantr A B C A 0 B 0 A
74 73 3ad2ant1 A B C A 0 B 0 R + 0 D X Y A
75 59 rpred R + 0 D R
76 75 3ad2ant2 A B C A 0 B 0 R + 0 D X Y R
77 76 resqcld A B C A 0 B 0 R + 0 D X Y R 2
78 77 12 remulcld A B C A 0 B 0 R + 0 D X Y R 2 Q
79 simp1l3 A B C A 0 B 0 R + 0 D X Y C
80 79 resqcld A B C A 0 B 0 R + 0 D X Y C 2
81 78 80 resubcld A B C A 0 B 0 R + 0 D X Y R 2 Q C 2
82 2 81 eqeltrid A B C A 0 B 0 R + 0 D X Y D
83 82 recnd A B C A 0 B 0 R + 0 D X Y D
84 83 sqrtcld A B C A 0 B 0 R + 0 D X Y D
85 41 74 84 mulassd A B C A 0 B 0 R + 0 D X Y 2 A D = 2 A D
86 85 oveq2d A B C A 0 B 0 R + 0 D X Y 2 B C + 2 A D = 2 B C + 2 A D
87 51 negnegd A B C A 0 B 0 R + 0 D X Y 2 B C = 2 B C
88 simpl A B C A 0 B 0 A B C
89 88 3ad2ant1 A B C A 0 B 0 R + 0 D X Y A B C
90 simp2r A B C A 0 B 0 R + 0 D X Y 0 D
91 1 3 4 2 itsclc0yqsollem2 A B C R 0 D 2 B C 2 4 Q C 2 A 2 R 2 = 2 A D
92 89 76 90 91 syl3anc A B C A 0 B 0 R + 0 D X Y 2 B C 2 4 Q C 2 A 2 R 2 = 2 A D
93 87 92 oveq12d A B C A 0 B 0 R + 0 D X Y - 2 B C + 2 B C 2 4 Q C 2 A 2 R 2 = 2 B C + 2 A D
94 74 84 mulcld A B C A 0 B 0 R + 0 D X Y A D
95 41 50 94 adddid A B C A 0 B 0 R + 0 D X Y 2 B C + A D = 2 B C + 2 A D
96 86 93 95 3eqtr4d A B C A 0 B 0 R + 0 D X Y - 2 B C + 2 B C 2 4 Q C 2 A 2 R 2 = 2 B C + A D
97 96 oveq1d A B C A 0 B 0 R + 0 D X Y - 2 B C + 2 B C 2 4 Q C 2 A 2 R 2 2 Q = 2 B C + A D 2 Q
98 50 94 addcld A B C A 0 B 0 R + 0 D X Y B C + A D
99 2ne0 2 0
100 99 a1i A B C A 0 B 0 R + 0 D X Y 2 0
101 98 13 41 40 100 divcan5d A B C A 0 B 0 R + 0 D X Y 2 B C + A D 2 Q = B C + A D Q
102 97 101 eqtrd A B C A 0 B 0 R + 0 D X Y - 2 B C + 2 B C 2 4 Q C 2 A 2 R 2 2 Q = B C + A D Q
103 102 eqeq2d A B C A 0 B 0 R + 0 D X Y Y = - 2 B C + 2 B C 2 4 Q C 2 A 2 R 2 2 Q Y = B C + A D Q
104 85 oveq2d A B C A 0 B 0 R + 0 D X Y 2 B C 2 A D = 2 B C 2 A D
105 87 92 oveq12d A B C A 0 B 0 R + 0 D X Y - 2 B C - 2 B C 2 4 Q C 2 A 2 R 2 = 2 B C 2 A D
106 41 50 94 subdid A B C A 0 B 0 R + 0 D X Y 2 B C A D = 2 B C 2 A D
107 104 105 106 3eqtr4d A B C A 0 B 0 R + 0 D X Y - 2 B C - 2 B C 2 4 Q C 2 A 2 R 2 = 2 B C A D
108 107 oveq1d A B C A 0 B 0 R + 0 D X Y - 2 B C - 2 B C 2 4 Q C 2 A 2 R 2 2 Q = 2 B C A D 2 Q
109 50 94 subcld A B C A 0 B 0 R + 0 D X Y B C A D
110 109 13 41 40 100 divcan5d A B C A 0 B 0 R + 0 D X Y 2 B C A D 2 Q = B C A D Q
111 108 110 eqtrd A B C A 0 B 0 R + 0 D X Y - 2 B C - 2 B C 2 4 Q C 2 A 2 R 2 2 Q = B C A D Q
112 111 eqeq2d A B C A 0 B 0 R + 0 D X Y Y = - 2 B C - 2 B C 2 4 Q C 2 A 2 R 2 2 Q Y = B C A D Q
113 103 112 orbi12d A B C A 0 B 0 R + 0 D X Y Y = - 2 B C + 2 B C 2 4 Q C 2 A 2 R 2 2 Q Y = - 2 B C - 2 B C 2 4 Q C 2 A 2 R 2 2 Q Y = B C + A D Q Y = B C A D Q
114 69 113 bitrd A B C A 0 B 0 R + 0 D X Y Q Y 2 + 2 B C Y + C 2 A 2 R 2 = 0 Y = B C + A D Q Y = B C A D Q
115 absid A 0 A A = A
116 115 ex A 0 A A = A
117 116 3ad2ant1 A B C 0 A A = A
118 117 adantr A B C A 0 B 0 0 A A = A
119 118 3ad2ant1 A B C A 0 B 0 R + 0 D X Y 0 A A = A
120 119 impcom 0 A A B C A 0 B 0 R + 0 D X Y A = A
121 120 oveq1d 0 A A B C A 0 B 0 R + 0 D X Y A D = A D
122 121 oveq2d 0 A A B C A 0 B 0 R + 0 D X Y B C + A D = B C + A D
123 122 oveq1d 0 A A B C A 0 B 0 R + 0 D X Y B C + A D Q = B C + A D Q
124 123 eqeq2d 0 A A B C A 0 B 0 R + 0 D X Y Y = B C + A D Q Y = B C + A D Q
125 121 oveq2d 0 A A B C A 0 B 0 R + 0 D X Y B C A D = B C A D
126 125 oveq1d 0 A A B C A 0 B 0 R + 0 D X Y B C A D Q = B C A D Q
127 126 eqeq2d 0 A A B C A 0 B 0 R + 0 D X Y Y = B C A D Q Y = B C A D Q
128 124 127 orbi12d 0 A A B C A 0 B 0 R + 0 D X Y Y = B C + A D Q Y = B C A D Q Y = B C + A D Q Y = B C A D Q
129 pm1.4 Y = B C + A D Q Y = B C A D Q Y = B C A D Q Y = B C + A D Q
130 128 129 syl6bi 0 A A B C A 0 B 0 R + 0 D X Y Y = B C + A D Q Y = B C A D Q Y = B C A D Q Y = B C + A D Q
131 50 adantl ¬ 0 A A B C A 0 B 0 R + 0 D X Y B C
132 94 adantl ¬ 0 A A B C A 0 B 0 R + 0 D X Y A D
133 131 132 subnegd ¬ 0 A A B C A 0 B 0 R + 0 D X Y B C A D = B C + A D
134 74 adantl ¬ 0 A A B C A 0 B 0 R + 0 D X Y A
135 84 adantl ¬ 0 A A B C A 0 B 0 R + 0 D X Y D
136 134 135 mulneg1d ¬ 0 A A B C A 0 B 0 R + 0 D X Y A D = A D
137 89 simp1d A B C A 0 B 0 R + 0 D X Y A
138 137 adantl ¬ 0 A A B C A 0 B 0 R + 0 D X Y A
139 id A A
140 0red A 0
141 139 140 ltnled A A < 0 ¬ 0 A
142 ltle A 0 A < 0 A 0
143 140 142 mpdan A A < 0 A 0
144 141 143 sylbird A ¬ 0 A A 0
145 144 3ad2ant1 A B C ¬ 0 A A 0
146 145 adantr A B C A 0 B 0 ¬ 0 A A 0
147 146 3ad2ant1 A B C A 0 B 0 R + 0 D X Y ¬ 0 A A 0
148 147 impcom ¬ 0 A A B C A 0 B 0 R + 0 D X Y A 0
149 138 148 absnidd ¬ 0 A A B C A 0 B 0 R + 0 D X Y A = A
150 149 negeqd ¬ 0 A A B C A 0 B 0 R + 0 D X Y A = A
151 57 adantl ¬ 0 A A B C A 0 B 0 R + 0 D X Y A
152 151 negnegd ¬ 0 A A B C A 0 B 0 R + 0 D X Y A = A
153 150 152 eqtrd ¬ 0 A A B C A 0 B 0 R + 0 D X Y A = A
154 153 oveq1d ¬ 0 A A B C A 0 B 0 R + 0 D X Y A D = A D
155 136 154 eqtr3d ¬ 0 A A B C A 0 B 0 R + 0 D X Y A D = A D
156 155 oveq2d ¬ 0 A A B C A 0 B 0 R + 0 D X Y B C A D = B C A D
157 133 156 eqtr3d ¬ 0 A A B C A 0 B 0 R + 0 D X Y B C + A D = B C A D
158 157 oveq1d ¬ 0 A A B C A 0 B 0 R + 0 D X Y B C + A D Q = B C A D Q
159 158 eqeq2d ¬ 0 A A B C A 0 B 0 R + 0 D X Y Y = B C + A D Q Y = B C A D Q
160 131 132 negsubd ¬ 0 A A B C A 0 B 0 R + 0 D X Y B C + A D = B C A D
161 155 oveq2d ¬ 0 A A B C A 0 B 0 R + 0 D X Y B C + A D = B C + A D
162 160 161 eqtr3d ¬ 0 A A B C A 0 B 0 R + 0 D X Y B C A D = B C + A D
163 162 oveq1d ¬ 0 A A B C A 0 B 0 R + 0 D X Y B C A D Q = B C + A D Q
164 163 eqeq2d ¬ 0 A A B C A 0 B 0 R + 0 D X Y Y = B C A D Q Y = B C + A D Q
165 159 164 orbi12d ¬ 0 A A B C A 0 B 0 R + 0 D X Y Y = B C + A D Q Y = B C A D Q Y = B C A D Q Y = B C + A D Q
166 165 biimpd ¬ 0 A A B C A 0 B 0 R + 0 D X Y Y = B C + A D Q Y = B C A D Q Y = B C A D Q Y = B C + A D Q
167 130 166 pm2.61ian A B C A 0 B 0 R + 0 D X Y Y = B C + A D Q Y = B C A D Q Y = B C A D Q Y = B C + A D Q
168 114 167 sylbid A B C A 0 B 0 R + 0 D X Y Q Y 2 + 2 B C Y + C 2 A 2 R 2 = 0 Y = B C A D Q Y = B C + A D Q
169 7 168 syld A B C A 0 B 0 R + 0 D X Y X 2 + Y 2 = R 2 A X + B Y = C Y = B C A D Q Y = B C + A D Q