Metamath Proof Explorer


Theorem 2itscp

Description: A condition for a quadratic equation with real coefficients (for the intersection points of a line with a circle) to have (exactly) two different real solutions. (Contributed by AV, 5-Mar-2023) (Revised by AV, 16-May-2023)

Ref Expression
Hypotheses 2itscp.a φ A
2itscp.b φ B
2itscp.x φ X
2itscp.y φ Y
2itscp.d D = X A
2itscp.e E = B Y
2itscp.c C = D B + E A
2itscp.r φ R
2itscp.l φ A 2 + B 2 < R 2
2itscp.n φ B Y A X
2itscp.q Q = E 2 + D 2
2itscp.s S = R 2 Q C 2
Assertion 2itscp φ 0 < S

Proof

Step Hyp Ref Expression
1 2itscp.a φ A
2 2itscp.b φ B
3 2itscp.x φ X
4 2itscp.y φ Y
5 2itscp.d D = X A
6 2itscp.e E = B Y
7 2itscp.c C = D B + E A
8 2itscp.r φ R
9 2itscp.l φ A 2 + B 2 < R 2
10 2itscp.n φ B Y A X
11 2itscp.q Q = E 2 + D 2
12 2itscp.s S = R 2 Q C 2
13 2 recnd φ B
14 13 adantr φ B Y B
15 4 recnd φ Y
16 15 adantr φ B Y Y
17 simpr φ B Y B Y
18 14 16 17 subne0d φ B Y B Y 0
19 18 ex φ B Y B Y 0
20 3 recnd φ X
21 20 adantr φ A X X
22 1 recnd φ A
23 22 adantr φ A X A
24 simpr φ A X A X
25 24 necomd φ A X X A
26 21 23 25 subne0d φ A X X A 0
27 26 ex φ A X X A 0
28 6 neeq1i E 0 B Y 0
29 5 neeq1i D 0 X A 0
30 28 29 anbi12i E 0 D 0 B Y 0 X A 0
31 2re 2
32 31 a1i φ 2
33 3 1 resubcld φ X A
34 5 33 eqeltrid φ D
35 34 1 remulcld φ D A
36 2 4 resubcld φ B Y
37 6 36 eqeltrid φ E
38 37 2 remulcld φ E B
39 35 38 remulcld φ D A E B
40 32 39 remulcld φ 2 D A E B
41 40 adantr φ E 0 D 0 2 D A E B
42 37 resqcld φ E 2
43 2 resqcld φ B 2
44 42 43 remulcld φ E 2 B 2
45 34 resqcld φ D 2
46 1 resqcld φ A 2
47 45 46 remulcld φ D 2 A 2
48 44 47 readdcld φ E 2 B 2 + D 2 A 2
49 48 adantr φ E 0 D 0 E 2 B 2 + D 2 A 2
50 8 resqcld φ R 2
51 50 46 resubcld φ R 2 A 2
52 42 51 remulcld φ E 2 R 2 A 2
53 50 43 resubcld φ R 2 B 2
54 45 53 remulcld φ D 2 R 2 B 2
55 52 54 readdcld φ E 2 R 2 A 2 + D 2 R 2 B 2
56 55 adantr φ E 0 D 0 E 2 R 2 A 2 + D 2 R 2 B 2
57 35 38 resubcld φ D A E B
58 57 sqge0d φ 0 D A E B 2
59 1 2 3 4 5 6 2itscplem1 φ E 2 B 2 + D 2 A 2 - 2 D A E B = D A E B 2
60 58 59 breqtrrd φ 0 E 2 B 2 + D 2 A 2 - 2 D A E B
61 48 40 subge0d φ 0 E 2 B 2 + D 2 A 2 - 2 D A E B 2 D A E B E 2 B 2 + D 2 A 2
62 60 61 mpbid φ 2 D A E B E 2 B 2 + D 2 A 2
63 62 adantr φ E 0 D 0 2 D A E B E 2 B 2 + D 2 A 2
64 44 adantr φ E 0 D 0 E 2 B 2
65 47 adantr φ E 0 D 0 D 2 A 2
66 52 adantr φ E 0 D 0 E 2 R 2 A 2
67 54 adantr φ E 0 D 0 D 2 R 2 B 2
68 43 adantr φ E 0 D 0 B 2
69 51 adantr φ E 0 D 0 R 2 A 2
70 simpl E 0 D 0 E 0
71 sqn0rp E E 0 E 2 +
72 37 70 71 syl2an φ E 0 D 0 E 2 +
73 46 43 50 ltaddsub2d φ A 2 + B 2 < R 2 B 2 < R 2 A 2
74 9 73 mpbid φ B 2 < R 2 A 2
75 74 adantr φ E 0 D 0 B 2 < R 2 A 2
76 68 69 72 75 ltmul2dd φ E 0 D 0 E 2 B 2 < E 2 R 2 A 2
77 46 adantr φ E 0 D 0 A 2
78 53 adantr φ E 0 D 0 R 2 B 2
79 simpr E 0 D 0 D 0
80 sqn0rp D D 0 D 2 +
81 34 79 80 syl2an φ E 0 D 0 D 2 +
82 46 43 50 ltaddsubd φ A 2 + B 2 < R 2 A 2 < R 2 B 2
83 9 82 mpbid φ A 2 < R 2 B 2
84 83 adantr φ E 0 D 0 A 2 < R 2 B 2
85 77 78 81 84 ltmul2dd φ E 0 D 0 D 2 A 2 < D 2 R 2 B 2
86 64 65 66 67 76 85 lt2addd φ E 0 D 0 E 2 B 2 + D 2 A 2 < E 2 R 2 A 2 + D 2 R 2 B 2
87 41 49 56 63 86 lelttrd φ E 0 D 0 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
88 87 ex φ E 0 D 0 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
89 30 88 syl5bir φ B Y 0 X A 0 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
90 19 27 89 syl2and φ B Y A X 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
91 90 imp φ B Y A X 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
92 nne ¬ A X A = X
93 eqcom A = X X = A
94 20 22 subeq0ad φ X A = 0 X = A
95 94 biimprd φ X = A X A = 0
96 93 95 syl5bi φ A = X X A = 0
97 92 96 syl5bi φ ¬ A X X A = 0
98 5 eqeq1i D = 0 X A = 0
99 28 98 anbi12i E 0 D = 0 B Y 0 X A = 0
100 0red φ E 0 D = 0 0
101 44 adantr φ E 0 D = 0 E 2 B 2
102 52 adantr φ E 0 D = 0 E 2 R 2 A 2
103 37 sqge0d φ 0 E 2
104 2 sqge0d φ 0 B 2
105 42 43 103 104 mulge0d φ 0 E 2 B 2
106 105 adantr φ E 0 D = 0 0 E 2 B 2
107 43 adantr φ E 0 D = 0 B 2
108 51 adantr φ E 0 D = 0 R 2 A 2
109 simprl φ E 0 D = 0 E 0
110 37 109 71 syl2an2r φ E 0 D = 0 E 2 +
111 74 adantr φ E 0 D = 0 B 2 < R 2 A 2
112 107 108 110 111 ltmul2dd φ E 0 D = 0 E 2 B 2 < E 2 R 2 A 2
113 100 101 102 106 112 lelttrd φ E 0 D = 0 0 < E 2 R 2 A 2
114 oveq1 D = 0 D A = 0 A
115 114 adantl E 0 D = 0 D A = 0 A
116 22 mul02d φ 0 A = 0
117 115 116 sylan9eqr φ E 0 D = 0 D A = 0
118 117 oveq1d φ E 0 D = 0 D A E B = 0 E B
119 38 recnd φ E B
120 119 mul02d φ 0 E B = 0
121 120 adantr φ E 0 D = 0 0 E B = 0
122 118 121 eqtrd φ E 0 D = 0 D A E B = 0
123 122 oveq2d φ E 0 D = 0 2 D A E B = 2 0
124 2t0e0 2 0 = 0
125 123 124 eqtrdi φ E 0 D = 0 2 D A E B = 0
126 sq0i D = 0 D 2 = 0
127 126 adantl E 0 D = 0 D 2 = 0
128 127 adantl φ E 0 D = 0 D 2 = 0
129 128 oveq1d φ E 0 D = 0 D 2 R 2 B 2 = 0 R 2 B 2
130 53 recnd φ R 2 B 2
131 130 mul02d φ 0 R 2 B 2 = 0
132 131 adantr φ E 0 D = 0 0 R 2 B 2 = 0
133 129 132 eqtrd φ E 0 D = 0 D 2 R 2 B 2 = 0
134 133 oveq2d φ E 0 D = 0 E 2 R 2 A 2 + D 2 R 2 B 2 = E 2 R 2 A 2 + 0
135 52 recnd φ E 2 R 2 A 2
136 135 addid1d φ E 2 R 2 A 2 + 0 = E 2 R 2 A 2
137 136 adantr φ E 0 D = 0 E 2 R 2 A 2 + 0 = E 2 R 2 A 2
138 134 137 eqtrd φ E 0 D = 0 E 2 R 2 A 2 + D 2 R 2 B 2 = E 2 R 2 A 2
139 113 125 138 3brtr4d φ E 0 D = 0 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
140 139 ex φ E 0 D = 0 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
141 99 140 syl5bir φ B Y 0 X A = 0 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
142 19 97 141 syl2and φ B Y ¬ A X 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
143 142 imp φ B Y ¬ A X 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
144 nne ¬ B Y B = Y
145 13 15 subeq0ad φ B Y = 0 B = Y
146 145 biimprd φ B = Y B Y = 0
147 144 146 syl5bi φ ¬ B Y B Y = 0
148 6 eqeq1i E = 0 B Y = 0
149 148 29 anbi12i E = 0 D 0 B Y = 0 X A 0
150 0red φ E = 0 D 0 0
151 47 adantr φ E = 0 D 0 D 2 A 2
152 54 adantr φ E = 0 D 0 D 2 R 2 B 2
153 34 sqge0d φ 0 D 2
154 1 sqge0d φ 0 A 2
155 45 46 153 154 mulge0d φ 0 D 2 A 2
156 155 adantr φ E = 0 D 0 0 D 2 A 2
157 46 adantr φ E = 0 D 0 A 2
158 53 adantr φ E = 0 D 0 R 2 B 2
159 simprr φ E = 0 D 0 D 0
160 34 159 80 syl2an2r φ E = 0 D 0 D 2 +
161 43 recnd φ B 2
162 46 recnd φ A 2
163 161 162 addcomd φ B 2 + A 2 = A 2 + B 2
164 163 9 eqbrtrd φ B 2 + A 2 < R 2
165 43 46 50 ltaddsub2d φ B 2 + A 2 < R 2 A 2 < R 2 B 2
166 164 165 mpbid φ A 2 < R 2 B 2
167 166 adantr φ E = 0 D 0 A 2 < R 2 B 2
168 157 158 160 167 ltmul2dd φ E = 0 D 0 D 2 A 2 < D 2 R 2 B 2
169 150 151 152 156 168 lelttrd φ E = 0 D 0 0 < D 2 R 2 B 2
170 oveq1 E = 0 E B = 0 B
171 170 adantr E = 0 D 0 E B = 0 B
172 13 mul02d φ 0 B = 0
173 171 172 sylan9eqr φ E = 0 D 0 E B = 0
174 173 oveq2d φ E = 0 D 0 D A E B = D A 0
175 34 adantr φ E = 0 D 0 D
176 175 recnd φ E = 0 D 0 D
177 22 adantr φ E = 0 D 0 A
178 176 177 mulcld φ E = 0 D 0 D A
179 178 mul01d φ E = 0 D 0 D A 0 = 0
180 174 179 eqtrd φ E = 0 D 0 D A E B = 0
181 180 oveq2d φ E = 0 D 0 2 D A E B = 2 0
182 181 124 eqtrdi φ E = 0 D 0 2 D A E B = 0
183 sq0i E = 0 E 2 = 0
184 183 adantr E = 0 D 0 E 2 = 0
185 184 adantl φ E = 0 D 0 E 2 = 0
186 185 oveq1d φ E = 0 D 0 E 2 R 2 A 2 = 0 R 2 A 2
187 51 recnd φ R 2 A 2
188 187 mul02d φ 0 R 2 A 2 = 0
189 188 adantr φ E = 0 D 0 0 R 2 A 2 = 0
190 186 189 eqtrd φ E = 0 D 0 E 2 R 2 A 2 = 0
191 190 oveq1d φ E = 0 D 0 E 2 R 2 A 2 + D 2 R 2 B 2 = 0 + D 2 R 2 B 2
192 54 recnd φ D 2 R 2 B 2
193 192 addid2d φ 0 + D 2 R 2 B 2 = D 2 R 2 B 2
194 193 adantr φ E = 0 D 0 0 + D 2 R 2 B 2 = D 2 R 2 B 2
195 191 194 eqtrd φ E = 0 D 0 E 2 R 2 A 2 + D 2 R 2 B 2 = D 2 R 2 B 2
196 169 182 195 3brtr4d φ E = 0 D 0 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
197 196 ex φ E = 0 D 0 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
198 149 197 syl5bir φ B Y = 0 X A 0 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
199 147 27 198 syl2and φ ¬ B Y A X 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
200 199 imp φ ¬ B Y A X 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
201 ioran ¬ B Y A X ¬ B Y ¬ A X
202 10 pm2.24d φ ¬ B Y A X 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
203 201 202 syl5bir φ ¬ B Y ¬ A X 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
204 203 imp φ ¬ B Y ¬ A X 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
205 91 143 200 204 4casesdan φ 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2
206 40 55 posdifd φ 2 D A E B < E 2 R 2 A 2 + D 2 R 2 B 2 0 < E 2 R 2 A 2 + D 2 R 2 B 2 - 2 D A E B
207 205 206 mpbid φ 0 < E 2 R 2 A 2 + D 2 R 2 B 2 - 2 D A E B
208 1 2 3 4 5 6 7 8 11 12 2itscplem3 φ S = E 2 R 2 A 2 + D 2 R 2 B 2 - 2 D A E B
209 207 208 breqtrrd φ 0 < S