1. n : {1...}
2. g : {2..(n+1)}
3. n = {2..n+1}(g)
  h:({2..(n+1)}). n = {2..n+1}(h) & is_prime_factorization(2; (n+1); h)

By:	Inst:  Thm*  k:{2...}, n:, g:({2..k}). Thm*  2  n < k+1 Thm*   Thm*  (i:{2..k}. ni  0<g(i)  prime(i)) Thm*   Thm*  (h:({2..k}).  Thm*  ({2..k}(g) = {2..k}(h) & is_prime_factorization(2; k; h)) Using:[n+1 | n+1 | g]

1

4. h:({2..(n+1)}).  4. {2..n+1}(g) = {2..n+1}(h) & is_prime_factorization(2; (n+1); h)   h:({2..(n+1)}). n = {2..n+1}(h) & is_prime_factorization(2; (n+1); h)

1 step

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