Hi Jon, I have a few suggestions concerning your theorem "itexp", if it doesn't take you too much time: * In set.mm, NN does not denote the natural numbers: it excludes zero (there was a recent flame war about this on this discussion group, let's not reopen it!). The set.mm symbol for natural numbers is NN0, so you could prove your theorem with NN0 in place of NN (of course, your theorem using NN is perfectly correct, but it is awkwardly restricted, ever so slightly). * Since your theorem could be useful, it might be worth to put it in deduction form (i.e. prepend "( ph -> " to the hypotheses and the conclusion). * I would label it "itpow" rather than "itexp" since it integrates power functions, and not exponential functions. * It would be nice to have the similar theorem for general polynomials, with something like sum_ k e. ( 0 ... N ) ( ( P ` k ) x. ( x ^ k ) ) on the LHS. Up to you to see if it's worth your time.
Benoit -- 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/8a55d2ae-79db-48a0-b3dd-2f1a9645c4b8%40googlegroups.com.
