Thanks Glauco for this outline. First, I re-ask my previous question: is there a particular reason you chose sine and cosine over the exponential function ?
Like FL, I think several lemmas deserve to be in the main part. I will use your sectioning: ORDERING ON REAL NUMBERS - REAL AND COMPLEX NUMBERS BASIC OPERATIONS ~ mul13d ~ subadd4b ~ xrlttri5d : yes to moving all three to the main part (just an opinion, I'm not among the persons who decide). Actually, there are by now algebraic lemmas of this kind in several mathboxes by Thierry Arnoux, David A. Wheeler, me (BJ), and probably others: 21.3.5 Real and Complex Numbers 21.26.11 Algebra helpers 21.29.8.2 Complex numbers (supplements) I'm not proposing to move them to the main part, just mentioning them here in case they prove useful. REAL INTERVALS ~ 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. ~ evthiccabs : I'm surprised that the proof is so long, given evthicc. Have you used MM>minimize * on you theorems? Also, the proof has two very similar parts, I don't know if it is possible to mutualize them. This is actually connected to Issue #1325 on github. LIMITS ellimciota : maybe it is worth to prove the lemma |- ( E! x x e. A -> ( iota x x e. A ) e. A ) ? climinf (and infrglb, etc.) look like important statements; are their equivalents for "non-decreasing bounded-above" in set.mm ? divlimc and limclner : also important, I would move them to the main part TRIGONOMETRY pirp2/bj-pirp/pirp: move Jim's version to the main part, now that it is in three mathboxes. Actually, I would move your whole Trigonometry section to the main part. (And it would be great to have analogs for sine, which can be easily deduced from yours -- but I recognize it is not a pleasant work!). ------------ There's a lot of great work in your mathbox! I'll have to stop here for the moment. Looking at random, I saw halffl, which I would prove using bj-flbi3 (which should then be moved to the main part). 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/9dd29b1f-58ab-4de2-a50e-c0bf0d3f73aa%40googlegroups.com.
