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.
