(15steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: only one factored by 1 a
1. f : Prime
  n,n':. f is a factorization of n  f is a factorization of n'  n = n'
By: n,n':.
nn'  f is a factorization of n  f is a factorization of n'  n = n'
Asserted

Generated subgoals:

1 2. n : 
3. n' : 
4. nn'
5. f is a factorization of n
6. f is a factorization of n'
  n = n'
PREMISE
2 2. n,n':.
2. nn'  f is a factorization of n  f is a factorization of n'  n = n'
3. n : 
4. n' : 
5. f is a factorization of n
6. f is a factorization of n'
  n = n'
1 step

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

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