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))a,b:
, P:({a..b}Prop), n:{(a+1)..(b+1)}.
Thm* P(n-1)
(i:{a..b}. ni P(i)) (i:{a..b}. n-1i P(i))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)))