(15steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
At: prime factorization unique a 1

1. a : {2...}
2. b : 
3. k:, g,h:({a..b}).
3. is_prime_factorization(a; b; g)
3. 
3. is_prime_factorization(a; b; h)
3. 
3. {a..b}(g) = k  {a..b}(g) = {a..b}(h)  g = h
4. g : {a..b}
5. h : {a..b}
6. is_prime_factorization(a; b; g)
7. is_prime_factorization(a; b; h)
8. {a..b}(g) = {a..b}(h)
  g = h


By: BackThru: Hyp:3 Using:[{a..b}(g)] ...


Generated subgoal:

1   {a..b}(g)  
1 step

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

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