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

is mentioned by

Thm*  n:{1...}. !f:(Prime). f is a factorization of n[fta_mset]
Thm*  n:, f,g:(Prime).
Thm*  f is a factorization of n  g is a factorization of n  f = g		[prime_factorization_mset_unique]
Thm*  n:{1...}. f:(Prime). f is a factorization of n[prime_factorization_exists2]
Thm*  a,b:, f:({a..b}), x:{a..b}. complete_intseg_mset(a; b; f)(x) = f(x)[complete_intseg_mset_isext]
Thm*  a,b:, f:({a..b}), x:.
Thm*  a  x < b  complete_intseg_mset(a; b; f)(x) = 0		[complete_intseg_mset_ismin]
Thm*  a,b:, f:({a..b}). complete_intseg_mset(a; b; f)  [complete_intseg_mset_wf]
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:, 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*  a,b:, f:({a..b}), j:{a..b}. 0<f(j)  j | {a..b}(f)[factor_divides_evalfactorization]
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]
Thm*  a,b:, f:({a..b}). is_prime_factorization(a; b; f)  Prop[is_prime_factorization_wf]
Thm*  a:, b:, f:({a..b}), j:{a..b}.
Thm*  2j  0<f(j)  {a..b}(reduce_factorization(f; j))<{a..b}(f)		[eval_reduce_factorization_less]
Thm*  a,b:, f:({a..b}), z:{a..b}.
Thm*  0<f(z)  {a..b}(f) = z{a..b}(reduce_factorization(f; z))		[eval_factorization_pluck]
Thm*  a,b:, f,g:({a..b}).
Thm*  {a..b}(f){a..b}(g) = {a..b}(i.f(i)+g(i))		[eval_factorization_prod]
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*  f:(Prime), n,n':.
Thm*  f is a factorization of n  f is a factorization of n'  n = n'		[only_one_factored_by]
Thm*  a:{2...}, b:, f:({a..b}). {a..b}(f) = 1  (i:{a..b}. f(i) = 0)[eval_factorization_one]
Thm*  f:(Prime), n:. f is a factorization of n  0<n[only_positives_prime_fed]
Thm*  a:, b:, f:({a..b}). {a..b}(f)  [eval_factorization_nat_plus]
Thm*  a,b:, f:({a..b}), j:{a..b}.
Thm*  0<f(j)  (i:{a..b}. reduce_factorization(f; j)(i)f(i))		[reduce_factorization_bound]
Thm*  a,b:, f,g:({a..b}), j:{a..b}.
Thm*  0<f(j)
Thm*  
Thm*  0<g(j)  reduce_factorization(f; j) = reduce_factorization(g; j)  f = g		[reduce_factorization_cancel]
Thm*  a,b:, f:({a..b}), j:{a..b}.
Thm*  0<f(j)  reduce_factorization(f; j)  {a..b}		[reduce_factorization_wf]
Thm*  x,y:. x  y  trivial_factorization(x)(y) = 0  [trivial_factorization_comp2]
Thm*  x,y:. x = y  trivial_factorization(x)(y) = 1  [trivial_factorization_comp1]
Thm*  a,b:, z:{a..b}. trivial_factorization(z)  {a..b}[trivial_factorization_wf]
Thm*  n:, f,g:(Prime).
Thm*  f is a factorization of n
Thm*  
Thm*  g is a factorization of n
Thm*  
Thm*  (x:{2..(n+1)}. prime_mset_complete(f)(x) = prime_mset_complete(g)(x))
Thm*  
Thm*  f = g		[prime_factorization_limit]
Thm*  f:(Prime), k:. f is a factorization of k  Prop[prime_factorization_of_wf]
Thm*  f:(Prime), x:. prime(x)  prime_mset_complete(f)(x) = 0[prime_mset_complete_ismin]
Thm*  f:(Prime), x:Prime. prime_mset_complete(f)(x) = f(x)[prime_mset_complete_isext]
Thm*  f:(Prime). prime_mset_complete(f)  [prime_mset_complete_wf]

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

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

FTA Sections DiscrMathExt Doc