n:{1...}.
Thm*
h:({2..(n+1)
}
).
Thm* n =
{2..n+1}(h) & is_prime_factorization(2; (n+1); h)a,b:
, j:{a..b}. {a..b}(trivial_factorization(j)) = jk:{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))