(3steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
The pairwise sum of factorizations of a couple of numbers factorizes their product.

At: eval factorization prod

  a,b:, f,g:({a..b}). {a..b}(f){a..b}(g) = {a..b}(i.f(i)+g(i))
By: Auto
THEN
Def of {<int>..<int>}(<exponents>)
THEN
Rewrite by
Thm*  a,b:, f,g:({a..b}).
Thm*  ( i:{a..b}. f(i))( i:{a..b}. g(i)) = ( i:{a..b}. f(i)g(i))
THEN
Reduce Concl

Generated subgoal:

1 1. a : 
2. b : 
3. f : {a..b}
4. g : {a..b}
  ( i:{a..b}. if(i)ig(i)) = ( i:{a..b}. i(f(i)+g(i)))
2 steps

About:
intnatural_numberaddmultiplylambdaapplyfunctionequalall
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html

(3steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc