Thanks for the response Mario, I see the link between the theorems now. I proved iocmbl as I think I need it but it's fine for it to stay in my math box if no one else is interested :)
Benoit, these sound like interesting suggestions. I have used itexp in areaquad so it is not super simple to change it however it is also not so bad. Now is the time to make changes if it can be strengthened. Replacing NN with NN0 I think should be quite simple. Though I think the case of n = 0 is covered by itgconst <http://us.metamath.org/mpegif/itgconst.html> it will be nice to make itexp a little more general. With putting the theorem in deduction form with "( ph ->" how does making that change work? Would I need to replace almost all theorems in the text so they begin with "( ph ->" or is there some way of just changing the beginning and the end? Sounds like it could be quite a lot of work. Re names I am willing to make the change, I think exp for exponential is a bit confusing in this context. Does anyone else have input? One of the reviewers suggested using the word monomial so maybe itmon is possible, itpow is fine or something else? Using exp does match with itgsinexp <http://us.metamath.org/mpegif/itgsinexp.html>, though that is only in Glauco's math box. I looked for the theorem of the integral of e^x but couldn't find it :( As for a general theorem that sounds nice, I would like to do more calculus stuff, however it will have to wait until I have finished this triangle stuff at least. If anyone else wants to take it on feel free :) -- 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/1673138f-ecf3-4831-8671-edf3c6d03bd6%40googlegroups.com.
