I don't know what does or doesn't get into what, but the argument for the shortest path from A to B being the direct straight-line path is conceptually simple, like so: let f(t) be a curve which passes from A to B. We can split f(t) into coordinate functions x(t), y(t), …, and we can choose a coordinate system such that A and B differ only on their x coordinate, with B having the larger x coordinate.

The total length of the curve described by f is the integral of |df/dt| dt, which is to say, the integral of sqrt((dx/dt)^2 + (dy/dt)^2 + ...) dt. This integrand is at least as large as dx/dt dt. But the integral of this latter integrand is the difference of B's and A's x coordinates, which is to say, the length of the direct straight-line path from A to B.

Thus, every path from A to B is at least as long as the direct straight-line path. [In fact, paying more careful attention, we have by this same argument the slightly stronger result that every other path is strictly longer than the straight-line path]

Now, without some context, this is not a good proof because you don't say your assumptions/axioms up front. Did you already prove that sqrt(x2+y2)>=x? Did you already prove that this particual integral exists? That you are allowed to choose a coordinate system so that A and B are both on the x axis?

If you take all of the above for granted (or "obvious"), you may as well say that the straight line being shortest is obvious.

Every proof is like this [except in the particular context of 100% formalized proof systems agreed upon in all details beforehand, but that is a niche context, not the default for mathematical discussion or thought].

I spelt out the parts of the argument that might be unfamiliar. I'm sure anyone here can readily convince themselves that sqrt(x^2 + y^2) >= x [x^2 is increasing for positive inputs, thus so is its inverse function, so sqrt(x^2 + y^2) >= sqrt(x^2) = |x| >= x], and that you can choose a coordinate system so that A and B are both on the x axis [take A to be the origin; take the vector from A to B to give the positive x axis, and other axes accordingly perpendicular to this one], and so on.

The integral business can be phrased however one likes, formally or informally, to account for the idea of a rectifiable curve as one whose length is given by treating it as built of many component straight-line pieces. The conceptual argument is the same, regardless of any particular choice of technical framework.

And if you furthermore aren't sure that, say, x^2 is increasing on positive inputs, we can explore that as well. If you furthermore aren't sold on modus ponens, we can explore that as well. Everything is infinitely explorable (and malleable!). But I noted only what here seemed directly relevant to the curiosity at hand.

I think it was exactly the right level of rigor for a HN comment. Gets the important idea across, doesn't get bogged down in the details that would be easy enough to fill in.

I'm not totally sure; I think it depends on what exactly you classify as calculus of variations, and what assumptions you're willing to make along the way. For what it's worth, I don't think I know how to prove the most general case possible. But given that I encountered this in physics rather than in math, I was satisfied with proving the physical analog, which would be the claim that the path of light in Euclidean space is always linear. Assuming we're talking about light allowed me to make 3 useful assumptions: (1) that the speed of the particle doing the traveling is constant, which comes in quite handy in the proof [1], (2) that there is only 1 independent variable (i.e., time) rather than 3 space coordinates, and (3) that our functions are all sufficiently smooth and such. The nice thing about this proof is it doesn't need the Euler-Lagrange equation that everybody uses... it doesn't need calculus of variations at all. Every step is an elementary calculus step. But the downside is the thought process that actually leads to the derivation is the one you'd only really get after studying a bit of calculus of variations, so you wouldn't come up with it without having that foundation (even though it's not required). (Yes, you can try to remove time from this proof and still keep it rigorous, but then it'd require a stronger background than just freshman calculus in order to be understood.)

[1] The reason I was satisfied with this is that it's obvious that the speed of the particle is irrelevant to the length of the path so long as the medium is uniform, so once I proved it for light of constant speed, I was done. It's not necessarily satisfying for a mathematician though.

This is a pictorial description of the proof in the sibling comment. It does not use calculus of variations, just the definition of the path length of a (differentiable parametrized) curve. If you want to call your parametrization a "light-ray" thats fine, but muddies the waters for me.

Just spell out what we mean by path, length of a path, and use calculus of a single variable. No need to introduce 'time', 'constant speed' or the like.

BTW, a truly variational proof is in the wikipedia article [0].

[0] https://en.wikipedia.org/wiki/Calculus_of_variations#Example

> This is a pictorial description of the proof in the sibling comment.

Well, for starters, it was also posted an hour before that one...

But it's not the same. The sibling comment performs a change of basis. I don't.