3 ms·

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 a

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.

Chinjut 10y ago
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.
- monochromatic 10y ago
  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.

Chinjut 10y ago

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.

monochromatic 10y ago
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.