FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  P & Q == PQ

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*   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; kh))
[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*  k:{2...}, g:({2..k}), x,y:{2..k}.
Thm*  xy<k
Thm*  
Thm*  (h:({2..k}). 
Thm*  ({2..k}(g) = {2..k}(h)
Thm*  (h(xy) = 0
Thm*  (& (u:{2..k}. xy<u  h(u) = g(u)))
[can_reduce_composite_factor]
Thm*  k:{2...}, g:({2..k}), x:{2..k}.
Thm*  xx<k
Thm*  
Thm*  {2..k}(g) = {2..k}(split_factor1(gx))
Thm*  & split_factor1(gx)(xx) = 0
Thm*  & (u:{2..k}. xx<u  split_factor1(gx)(u) = g(u))
[split_factor1_char]
Thm*  k:{2...}, g:({2..k}), x,y:{2..k}.
Thm*  xy<k
Thm*  
Thm*  x<y
Thm*  
Thm*  {2..k}(g) = {2..k}(split_factor2(gxy))
Thm*  & split_factor2(gxy)(xy) = 0
Thm*  & (u:{2..k}. xy<u  split_factor2(gxy)(u) = g(u))
[split_factor2_char]
Thm*  p:. prime(p (b,z:p | zb  b  0 & p | z)[prime_divs_exp]
Def  f is a factorization of k
Def  == (x:Primek<x  f(x) = 0) & k = {2..k+1}(prime_mset_complete(f))
[prime_factorization_of]

In prior sections: core int 1 bool 1 LogicSupplement int 2 num thy 1 SimpleMulFacts IteratedBinops rel 1

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

FTA Sections DiscrMathExt Doc