I would do something like this (which is not exactly metamath syntax but
not too hard to write precisely):
0 < k,
0 < l,
F = (x e. RR |-> k*x^2 - 2*k*x + l),
{ x | F(x) = 4 } = {A, B},
(A - B)^2 + (F(A) - F(B))^2 = 6
|- (A^2 + F(A)^2) + (B^2 + F(B)^2) = ?
although to actually prove it you have to first fill in the ? with the
answer.
On Sun, Jul 28, 2024 at 8:07 PM jagra <[email protected]> wrote:
> Understand this is not a common, and probably not even wanted, topic on
> this group.
>
> Trying to translate to metamath a simple problem from AIMO train dataset,
> just out of curiosity.
>
> The problem statement is:
>
> Let $k, l > 0$ be parameters. The parabola $y = kx^2 - 2kx + l$ intersects
> the line $y = 4$ at two points $A$ and $B$. These points are distance 6
> apart. What is the sum of the squares of the distances from $A$ and $B$ to
> the origin?
>
> Trying to come up a direct construction of the conditions and statement to
> prove and blocking, from my ignorance most certainly, on some embarassing
> road blocks.
>
>
> 1. Define function y=4
> 2. Define parabola function in terms of k and l
> 3. Connect 1 & 2 with points A and B
> 4. Define distance between A and B
> 5. Define the goal in terms of A and B
>
> Really understand this is probably a basic question and I'm offsetting my
> due dilligence, so, no problem if no one takes the time to answer this :)
>
> Best regards,
> Jorge Agra
>
> --
> You received this message because you are subscribed to the Google Groups
> "Metamath" group.
> To unsubscribe from this group and stop receiving emails from it, send an
> email to [email protected].
> To view this discussion on the web visit
> https://groups.google.com/d/msgid/metamath/6f644425-c9fd-4516-b8f3-76b104c2be4fn%40googlegroups.com
> <https://groups.google.com/d/msgid/metamath/6f644425-c9fd-4516-b8f3-76b104c2be4fn%40googlegroups.com?utm_medium=email&utm_source=footer>
> .
>
--
You received this message because you are subscribed to the Google Groups
"Metamath" group.
To unsubscribe from this group and stop receiving emails from it, send an email
to [email protected].
To view this discussion on the web visit
https://groups.google.com/d/msgid/metamath/CAFXXJSvErAB952rJfK4Qef9T6sO%2B4DiA%2B6b3JEZCiq-_J9uyHA%40mail.gmail.com.
