In this blog post, Steve Landsburg presents a truly remarkable proof that the square root of 2 is irrational:
In the comment section of that blog post, I tried to translate the proof into the system of Euclid's Elements. I succeeded, except for one small step.
So my question is, how can we prove that the line containing the red line segment intersects the interior of lower leg of the right triangle? I think it would be fairly easy to prove that the line containing the red segment intersects the line containing the lower leg somewhere. (We just need f show that they're not parallel.) But how can we prove that the intersection point specifically lies somewhere on the lower leg?
Preferably I would like a proof that works within Euclid's Elements, which you can see here.
EDIT: To be clear, the fact that the line intersects the lower leg is shown in the above picture, but I want a rigorous proof that doesn't depend on looking at a picture.
There are three places where it could land. If it lands on that vertical edge, the line could be extended and it would land on a point on circle. It could land on that right angle vertice, which is also a point on circle. And by your "line containing red line" is a tangent. It can touch circle at only one point. The remaining third place is lower leg
Edit: assume the tangent meets the vertical edge, all the points on vertical edge are within the circle. A line from a point on the circle meeting a point within the circle, touches circle at another point ( i don't know again if it should be proved). So the tangent can't intersect with vertical line. The vertical line intersects at only one point on circle, the tangent could intersect this point, but then it would not be tangent. The tangent has to intersect the horizontal line. The length of red line and lower leg( just a name) should be equal(congruency of triangle, I don't know if I can use this), so it has to be lower leg, else the red line will be bigger than hypotenuse of small right angled triangle. I don't know what looking at picture means, hope this helps