Def  prime(a) == a = 0 & (a ~ 1) & (b,c:. a | bc  a | b  a | c)

is mentioned by

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*  k:{2...}, g:({2..k}), z:{2..k}. Thm*  prime(z) Thm*   Thm*  (g':({2..k}).  Thm*  ({2..k}(g) = {2..k}(g') Thm*  (& g'(z) = 0 Thm*  (& (u:{2..k}. z<u  g'(u) = g(u)))	[can_reduce_composite_factor2]
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*  p:. prime(p)  (b,z:. p | zb  b  0 & p | z)	[prime_divs_exp]
Thm*  p:.  Thm*  prime(p) Thm*   Thm*  (a,b:, e:({a..b}). Thm*  (a<b  p | ( i:{a..b}. e(i))  (i:{a..b}. p | e(i)))	[prime_divs_mul_via_intseg]
Thm*  X:. prime(X)  (a,b:. X | ab  X | a  X | b)	[nat_prime_div_each_factor]
Thm*  X:.  Thm*  prime(X) Thm*   Thm*  (X1:. X1<X  prime(X1)  (a,b:. X1 | ab  X1 | a  X1 | b)) Thm*   Thm*  (W:. 0<W  W<X  (t:. X | tW  X | t))	[nat_prime_div_each_factorLEMMA]
Thm*  f:(Prime), x:. prime(x)  prime_mset_complete(f)(x) = 0	[prime_mset_complete_ismin]
Def  is_prime_factorization(a; b; f) == i:{a..b}. 0<f(i)  prime(i)	[is_prime_factorization]

In prior sections: num thy 1 SimpleMulFacts

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