Theorem: |
integral_mult |
not (?b contains ?bdv) => Integral ?a * ?b D ?bdv = ?a * Integral ?b D ?bdv |
Explanations:
The precondition not (?b contains ?bdv) inhibits wrong applications of the rule as for instance
Integral x* x D x = Integral x D x * Integral x D x ((1))
This is wrong as you easily can verify: integrating the left hand side in (1) gives
Integral x* x D x = Integral x^2 D x = x^3/3 + c ((2))
while integrating the right hand sidein (1) gives
Integral x D x * Integral x D x = x^2/2 * x^2/2 + c = x^4/4 + c ((3))
Thus integrating the both sides in (1) gives two different results (2) and (3) which should not happen (as long as we want to perserve the meaning of '=' and the Integral to be welldefined).