I maybe wrong, but my feeling is that what Jagra calls A , in Mario's
translation is actually < A , 4 > (or < A, F(A) > , if you prefer).
And Jagra's B , is actually Mario's < B , 4 >
If that's the case, an adaptation could be
{ x | F(x) = 4 } = { ( 1st ` A ) , ( 1st ` B ) }
and the other formulas should be similarly adapted.
To simplify a bit, you could use 4 in place of F(A) and F(B), thus, for
instance, Mario's
(A - B)^2 + (F(A) - F(B))^2 = 6
would become
( ( 1st ` A ) - ( 1st ` B ) )^2 = 6
because (F(A) - F(B))^2 is zero
Il giorno domenica 28 luglio 2024 alle 20:24:41 UTC+2 [email protected] ha
scritto:
> 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/ceb387e8-bd22-41c8-a2e7-ec44028379e2n%40googlegroups.com.
