(11steps total) PrintForm Definitions Lemmas FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Every positive integer can be factored into primes.

At: prime factorization exists2


  n:{1...}. f:(Prime). f is a factorization of n

By: SimilarTo
Thm*  n:{1...}. 
Thm*  h:({2..(n+1)}). 
Thm*  n = {2..n+1}(h) & is_prime_factorization(2; (n+1); h)


Generated subgoal:

1 1. n : {1...}
2. h:({2..(n+1)}). n = {2..n+1}(h) & is_prime_factorization(2; (n+1); h)
  f:(Prime). f is a factorization of n

10 steps

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

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