FTA Sections DiscrMathExt Doc
IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html
Def  {i...} == {j:| ij }

is mentioned by

Thm*  n:{1...}. !f:(Prime). f is a factorization of n[fta_mset]
Thm*  n:{1...}. f:(Prime). f is a factorization of n[prime_factorization_exists2]
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*  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(g; x))
Thm*  & split_factor1(g; x)(xx) = 0
Thm*  & (u:{2..k}. xx<u  split_factor1(g; x)(u) = g(u))		[split_factor1_char]
Thm*  k:{2...}, g:({2..k}), x:{2..k}.
Thm*  xx<k  split_factor1(g; x)  {2..k}		[split_factor1_wf]
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(g; x; y))
Thm*  & split_factor2(g; x; y)(xy) = 0
Thm*  & (u:{2..k}. xy<u  split_factor2(g; x; y)(u) = g(u))		[split_factor2_char]
Thm*  k:{2...}, g:({2..k}), x,y:{2..k}.
Thm*  xy<k  split_factor2(g; x; y)  {2..k}		[split_factor2_wf]
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:{2...}, b:, f:({a..b}).
Thm*  {a..b}(f) = 1  (i:{a..b}. f(i) = 0)		[eval_factorization_not_one]
Thm*  a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  f = (x.0)[eval_factorization_one_c]
Thm*  a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  (i:{a..b}. 0<f(i))[eval_factorization_one_b]
Thm*  a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  (i:{a..b}. f(i) = 0)[eval_factorization_one]

In prior sections: int 1 int 2 SimpleMulFacts IteratedBinops

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

FTA Sections DiscrMathExt Doc