Def  is_prime_factorization(a; b; f) == i:{a..b}. 0<f(i)  prime(i)

is mentioned by

Thm*  n:{1...}.  Thm*  h:({2..(n+1)}).  Thm*  n = {2..n+1}(h) & is_prime_factorization(2; (n+1); h)	[prime_factorization_exists]
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))	[prime_factorization_existsLEMMA]
Thm*  a:{2...}, b:, g,h:({a..b}). Thm*  is_prime_factorization(a; b; g) Thm*   Thm*  is_prime_factorization(a; b; h)  {a..b}(g) = {a..b}(h)  g = h	[prime_factorization_unique]
Thm*  a:, b:, f:({a..b}), p:. Thm*  is_prime_factorization(a; b; f) Thm*   Thm*  prime(p) Thm*   Thm*  p | {a..b}(f)  {a..b}(f) = p{a..b}(reduce_factorization(f; p))	[remove_prime_factor]
Thm*  a:, b:, f:({a..b}), p:. Thm*  is_prime_factorization(a; b; f) Thm*   Thm*  prime(p)  p | {a..b}(f)  p  {a..b} & 0<f(p)	[prime_factorization_includes_prime_divisors]
Thm*  a,b:, f:({a..b}), j:{a..b}. Thm*  0<f(j) Thm*   Thm*  is_prime_factorization(a; b; f) Thm*   Thm*  is_prime_factorization(a; b; reduce_factorization(f; j))	[reduce_fac_pres_isprimefac]
Thm*  a,b:, f:({a..b}). SqStable(is_prime_factorization(a; b; f))	[sq_stable__is_prime_factorization]
Thm*  f:(Prime), b:. is_prime_factorization(2; b; prime_mset_complete(f))	[prime_mset_c_is_prime_f]

Try larger context: DiscrMathExt IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html