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.
