pige3 - why...?

[Thomas Brendan Leahy]

I can't help but notice pige3 is shown in a very convoluted way, when it (in fact a slightly stronger statement) can be seen to follow quickly from sincos6thpi (which is indirectly used in the proof), sinltx, and a bit of arithmetic.  It seems like this is meant to preserve the geometric character of the approach, using Lipschitz continuity as a sort of analytic version of Euclid's first postulate, but I'm not sure that actually accomplishes that any better; after all, if you were to ask the layperson what a sine was, they'd give you a geometric answer, and there are a lot of situations in geometry (starting with corners) where this approach wouldn't work.

[Mario Carneiro]

Well, that's a nice proof! I struggled with good proofs of this theorem for a long while before I found the derivative proof, but I'm not wedded to it, and I agree that your proof approach is much more simple and direct. I'm not sure how I missed it. You should contribute it!

Mario

On Sun, Dec 8, 2019 at 11:54 PM Thomas Brendan Leahy <tbrend...@gmail.com> wrote:

I can't help but notice pige3 is shown in a very convoluted way, when it (in fact a slightly stronger statement) can be seen to follow quickly from sincos6thpi (which is indirectly used in the proof), sinltx, and a bit of arithmetic.  It seems like this is meant to preserve the geometric character of the approach, using Lipschitz continuity as a sort of analytic version of Euclid's first postulate, but I'm not sure that actually accomplishes that any better; after all, if you were to ask the layperson what a sine was, they'd give you a geometric answer, and there are a lot of situations in geometry (starting with corners) where this approach wouldn't work.

--
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 metamath+u...@googlegroups.com.
To view this discussion on the web visit https://groups.google.com/d/msgid/metamath/73c3f83d-df09-4d1a-8cbd-9805c8912881%40googlegroups.com.