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* i,j,k: . i  j < k  i j < k | [lelt_int_vs_lelt] |
Thm* i,j,k: . i  j < k  | [lelt_int_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 }. n i  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* x y<k
Thm* 
Thm* ( h:({2..k }  ).
Thm* ( {2..k }(g) =  {2..k }(h)
Thm* (& h(x y) = 0
Thm* (& ( u:{2..k }. x y<u  h(u) = g(u))) | [can_reduce_composite_factor] |
Thm* k:{2...}, g:({2..k }  ), x:{2..k }.
Thm* x x<k
Thm* 
Thm*  {2..k }(g) =  {2..k }(split_factor1(g; x))
Thm* & split_factor1(g; x)(x x) = 0
Thm* & ( u:{2..k }. x x<u  split_factor1(g; x)(u) = g(u)) | [split_factor1_char] |
Thm* k:{2...}, g:({2..k }  ), x:{2..k }.
Thm* x x<k  split_factor1(g; x) {2..k }   | [split_factor1_wf] |
Thm* k:{2...}, g:({2..k }  ), x,y:{2..k }.
Thm* x y<k
Thm* 
Thm* x<y
Thm* 
Thm*  {2..k }(g) =  {2..k }(split_factor2(g; x; y))
Thm* & split_factor2(g; x; y)(x y) = 0
Thm* & ( u:{2..k }. x y<u  split_factor2(g; x; y)(u) = g(u)) | [split_factor2_char] |
Thm* k:{2...}, g:({2..k }  ), x,y:{2..k }.
Thm* x y<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 | z b  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 | a b  X | a X | b) | [nat_prime_div_each_factor] |
Thm* X: .
Thm* prime(X)
Thm* 
Thm* ( X1: . X1<X  prime(X1)  ( a,b: . X1 | a b  X1 | a X1 | b))
Thm* 
Thm* ( W: . 0<W  W<X  ( t: . X | t W  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 }  ). b a   {a..b }(f) =  {a..a }(f) | [eval_factorization_nullnorm] |
Thm* a,b: , f:({a..b }  ). b a   {a..b }(f) = 1 | [eval_factorization_intseg_null] |
Thm* a: , b: , f:({a..b }  ), j:{a..b }.
Thm* 2 j  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* a,b: , j:{a..b }.  {a..b }(trivial_factorization(j)) = j | [eval_trivial_factorization] |
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* a,c,b: , f:({a..b }  ).
Thm* a c  c<b   {a..b }(f) =  {a..c }(f) c f(c)  {c+1..b }(f) | [eval_factorization_split_pluck] |
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* a,c,b: , f:({a..b }  ).
Thm* a c  c b   {a..b }(f) =  {a..c }(f)  {c..b }(f) | [eval_factorization_split_mid] |
Thm* a,b: , f:({a..b }  ).  {a..b }(f)  | [eval_factorization_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] |
Thm* a,b: , P:({a..b } Prop), n:{(a+1)..(b+1) }.
Thm* P(n-1)  ( i:{a..b }. n i  P(i))  ( i:{a..b }. n-1 i  P(i)) | [extend_intseg_upperpart_down] |
Def is_prime_factorization(a; b; f) == i:{a..b }. 0<f(i)  prime(i) | [is_prime_factorization] |
Def f is a factorization of k
Def == ( x:Prime . k<x  f(x) = 0) & k =  {2..k+1 }(prime_mset_complete(f)) | [prime_factorization_of] |