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 < [email protected]> 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 [email protected]. > To view this discussion on the web visit > https://groups.google.com/d/msgid/metamath/73c3f83d-df09-4d1a-8cbd-9805c8912881%40googlegroups.com > <https://groups.google.com/d/msgid/metamath/73c3f83d-df09-4d1a-8cbd-9805c8912881%40googlegroups.com?utm_medium=email&utm_source=footer> > . > -- 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/CAFXXJSsao9934RGhS6H-%3DwBAyiT0tuJE65vmUbiG0%2BFtwv6fNQ%40mail.gmail.com.
