(16steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Redistributing the power of a composite square in a factorization down to the square root produces another factorization of the same number, zeroing the power of the composite and leaving the powers of larger factors untouched.

At: split factor1 char

  k:{2...}, g:({2..k}), x:{2..k}.
  xx<k
  
  {2..k}(g) = {2..k}(split_factor1(g; x))
  & split_factor1(g; x)(xx) = 0
  & (u:{2..k}. xx<u  split_factor1(g; x)(u) = g(u))
By: {After letting h = split_factor1(g; x)  {2..k} and elaborating the three
{cases from its definition, the only work is showing that it factors the same
{number as g
{}
SideProof

Generated subgoal:

1 1. k : {2...}
2. g : {2..k}
3. x : {2..k}
4. xx<k
5. x<xx
6. h : {2..k}
7. h = split_factor1(g; x)
8. h(xx) = 0  
9. h(x) = g(x)+g(xx)+g(xx)  
10. u:{2..k}. u = x  u = xx  h(u) = g(u)
  {2..k}(g) = {2..k}(h)
10 steps

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

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