let n be non zero Nat; Euler n divides n !
set F0 = Euler_factorization n;
set F1 = Euler_factorization_1 n;
set F2 = Euler_factorization_2 n;
set b0 = (EmptyBag SetPrimes) +* (Euler_factorization n);
set b1 = (EmptyBag SetPrimes) +* (Euler_factorization_1 n);
set b2 = (EmptyBag SetPrimes) +* (Euler_factorization_2 n);
A1:
Euler n = Product ((EmptyBag SetPrimes) +* (Euler_factorization n))
by Th26;
A2:
Product ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) divides n
by Th33;
A3:
Product ((EmptyBag SetPrimes) +* (Euler_factorization_2 n)) divides (n - 1) !
by Th45, Th44;
A4:
support ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) = support (Euler_factorization_1 n)
by Th12;
A5:
support (Euler_factorization_1 n) = dom (Euler_factorization_1 n)
by Th28;
A6:
support ((EmptyBag SetPrimes) +* (Euler_factorization_2 n)) = support (Euler_factorization_2 n)
by Th12;
A7:
support (Euler_factorization_2 n) = dom (Euler_factorization_2 n)
by Th30;
A8:
dom (Euler_factorization_1 n) = support (ppf n)
by Def2;
A9:
dom (Euler_factorization_2 n) = support (ppf n)
by Def3;
(EmptyBag SetPrimes) +* (Euler_factorization n) = ((EmptyBag SetPrimes) +* (Euler_factorization_1 n)) (#) ((EmptyBag SetPrimes) +* (Euler_factorization_2 n))
by Th31;
then A10:
Product ((EmptyBag SetPrimes) +* (Euler_factorization n)) = (Product ((EmptyBag SetPrimes) +* (Euler_factorization_1 n))) * (Product ((EmptyBag SetPrimes) +* (Euler_factorization_2 n)))
by A4, A5, A6, A7, A8, A9, Th16;
((n - 1) + 1) ! = ((n - 1) !) * ((n - 1) + 1)
by NEWTON:15;
hence
Euler n divides n !
by A1, A2, A3, A10, NEWTON02:2; verum