let n be Nat; :: thesis: for f being SetPrimes -defined natural-valued finite-support Function st f <= n & f is increasing holds
Product ((EmptyBag SetPrimes) +* f) divides n !
let f be SetPrimes -defined natural-valued finite-support Function; :: thesis: ( f <= n & f is increasing implies Product ((EmptyBag SetPrimes) +* f) divides n ! )
assume that
A1: f <= n and
A2: f is increasing ; :: thesis: Product ((EmptyBag SetPrimes) +* f) divides n !
set b = (EmptyBag SetPrimes) +* f;
set C = canFS (support ((EmptyBag SetPrimes) +* f));
consider F being FinSequence of COMPLEX such that
A3: Product ((EmptyBag SetPrimes) +* f) = Product F and
A4: F = ((EmptyBag SetPrimes) +* f) * (canFS (support ((EmptyBag SetPrimes) +* f))) by NAT_3:def 5;
reconsider F = F as natural-valued FinSequence by A4;
set S = sort_a F;
A5: Product F = Product (sort_a F) by EULER_2:10, RFINSEQ2:def 6;
A6: F <= n by A1, A4, Th40;
A7: F is positive-yielding by A4, Th41;
A8: rng F = rng (sort_a F) by RFINSEQ2:def 6, CLASSES1:75;
sort_a F is increasing by A2, A4, Th43;
hence Product ((EmptyBag SetPrimes) +* f) divides n ! by A3, A5, A6, A7, A8, Th35, Th38; :: thesis: verum