> > the proofs that I followed stated the coefficients in terms of sine and > cosine. Some of them, then, proved some intermediate results using the > complex exponential form (it simplified some integral calculation), some > other sources instead kept using sine and cosine everywhere. When I had a > choice between two alternative such proofs, I followed the sine/cosine > approach. >
Thanks. Sticking to a proof you followed in a book is a good reason. I would have thought using exp all along would shorten things a bit, but this is a detail. > > ~ eliood , ~ eliocd , ~ elicod , ~ eliccd : it looks to me that they > could be strengthened by assuming only that A, B, C are extended reals. > For instance, in the proof of eliood, use elioo1 instead of elioo2, and > similarly in the proof of eliccd, use elicc1 instead of elicc2. > > elioo1 and elioo2 are "different" theorems, and I'm sure there are pros and > cons in both. But I see that elioo2 has (roughly) ten times the number of > references than elioo1 does and I guess that's an indication that elioo2 > turns out to be handy more often than elioo1. It maybe I chose eliood in > such form, because I noticed it was required more often in that form. Of > course, it may be useful to also introduce an elioo1d alternative that > takes the elioo1 "approach". > I'm not saying that either of elioo1/2 is more general than the other, and it is not the case indeed. What I'm saying is that you can strengthen your theorem eliood (relax the hypothesis C e. RR to C e. RR*) by using elioo1 in its proof instead of elioo2. And similarly with eliccd. > unfortunately I miss some of the features of metamath.exe , because I use mmj2 only (but I'm really intrigued by Thierry's plugin for Eclipse, I hope I will soon have time to take a closer look at it). > If I'm not mistaken, Normann periodically runs a "minimize" on the all set.mm, and that will help. Yes, but I think "periodically" used to be once a year, but a bit less now, and I'm not sure it looks at the mathboxes. Anyway, minimizing is not a requirement. I think that the objective of "minimize" is precisely what you're asking for: you do not have to remember all the labels, and only use the basic jca, sylibr, etc. And once the proof is done, "minimize" will optimize them, using sylanbrc, etc. Benoît -- 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/7af06596-e74a-4ab3-a915-d05149c72cc6%40googlegroups.com.
