let n be non zero Nat; :: thesis:
set N = Euler_factorization n;
defpred S₁[ Nat] means for n being non zero Nat st support ((EmptyBag SetPrimes) +* (Euler_factorization n)) c= Seg $1 holds
Product ((EmptyBag SetPrimes) +* (Euler_factorization n)) = Euler n;
A1: S₁[ 0 ]

proof

let n be non zero Nat; :: thesis:
set N = Euler_factorization n;
set G = (EmptyBag SetPrimes) +* (Euler_factorization n);
A2: support ((EmptyBag SetPrimes) +* (Euler_factorization n)) = support (Euler_factorization n) by Th12;
assume A3: support ((EmptyBag SetPrimes) +* (Euler_factorization n)) c= Seg 0 ; :: thesis:
then A4: n = 1 by A2, Th22, NAT_1:53;
support ((EmptyBag SetPrimes) +* (Euler_factorization n)) = {} by A3;
then (EmptyBag SetPrimes) +* (Euler_factorization n) = EmptyBag SetPrimes by PRE_POLY:81;
hence Product ((EmptyBag SetPrimes) +* (Euler_factorization n)) = Euler n by A4, NAT_3:20, EULER_1:17; :: thesis:

end;

A5: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

let k be Nat; :: thesis:
assume A6: S₁[k] ; :: thesis:
let n be non zero Nat; :: thesis:
set N = Euler_factorization n;
set p = k + 1;
set e = (k + 1) |-count n;
set s = (k + 1) |^ ((k + 1) |-count n);
set G = (EmptyBag SetPrimes) +* (Euler_factorization n);
assume A7: support ((EmptyBag SetPrimes) +* (Euler_factorization n)) c= Seg (k + 1) ; :: thesis:

per cases ;

suppose support ((EmptyBag SetPrimes) +* (Euler_factorization n)) c= Seg k ; :: thesis:

hence Product ((EmptyBag SetPrimes) +* (Euler_factorization n)) = Euler n by A6; :: thesis:

end;

suppose A8: not support ((EmptyBag SetPrimes) +* (Euler_factorization n)) c= Seg k ; :: thesis:

A9: support (ppf n) = support (pfexp n) by NAT_3:def 9;
A10: dom (Euler_factorization n) = support (ppf n) by Def1;
A11: support ((EmptyBag SetPrimes) +* (Euler_factorization n)) = support (Euler_factorization n) by Th12;
A12: support (Euler_factorization n) = dom (Euler_factorization n) by Th21;

A13: now :: thesis:

assume A14: not k + 1 in support ((EmptyBag SetPrimes) +* (Euler_factorization n)) ; :: thesis:
support ((EmptyBag SetPrimes) +* (Euler_factorization n)) c= Seg k

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A15: x in support ((EmptyBag SetPrimes) +* (Euler_factorization n)) ; :: thesis:
then reconsider m = x as Nat ;
m <= k + 1 by A7, A15, FINSEQ_1:1;
then m < k + 1 by A14, A15, XXREAL_0:1;
then A16: m <= k by NAT_1:13;
x is Prime by A11, A12, A15, Th17;
then 1 <= m by INT_2:def 4;
hence x in Seg k by A16; :: thesis:

end;

hence contradiction by A8; :: thesis:

end;

then A17: k + 1 is Prime by A11, A12, Th17;
then A18: k + 1 > 1 by INT_2:def 4;
then (k + 1) |^ ((k + 1) |-count n) divides n by NAT_3:def 7;
then consider t being Nat such that
A19: n = ((k + 1) |^ ((k + 1) |-count n)) * t ;
reconsider s = (k + 1) |^ ((k + 1) |-count n), t = t as non zero Nat by A19;
set S = Euler_factorization s;
set T = Euler_factorization t;
A20: dom ((EmptyBag SetPrimes) +* (Euler_factorization s)) = SetPrimes by PARTFUN1:def 2;
(pfexp n) . (k + 1) = (k + 1) |-count n by A17, NAT_3:def 8;
then A21: (k + 1) |-count n <> 0 by A9, A13, A10, A11, A12, PRE_POLY:def 7;
A22: support (ppf t) = support (pfexp t) by NAT_3:def 9;
A23: support ((EmptyBag SetPrimes) +* (Euler_factorization t)) = support (Euler_factorization t) by Th12;
A24: support (Euler_factorization t) = dom (Euler_factorization t) by Th21;
A25: dom (Euler_factorization t) = support (ppf t) by Def1;
A26: support (Euler_factorization t) c= Seg k

proof

set f = (k + 1) |-count t;
let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A27: x in support (Euler_factorization t) ; :: thesis:
then reconsider x = x as Nat by A24, A25;
A28: x in support (pfexp t) by A24, A25, A27, NAT_3:def 9;

A29: now :: thesis:

assume A30: x = k + 1 ; :: thesis:
(pfexp t) . (k + 1) = (k + 1) |-count t by A17, NAT_3:def 8;
then (k + 1) |-count t <> 0 by A28, A30, PRE_POLY:def 7;
then (k + 1) |-count t >= 0 + 1 by NAT_1:13;
then consider g being Nat such that
A31: (k + 1) |-count t = 1 + g by NAT_1:10;
(k + 1) |^ ((k + 1) |-count t) divides t by A18, NAT_3:def 7;
then consider u being Nat such that
A32: t = ((k + 1) |^ ((k + 1) |-count t)) * u ;
n = s * ((((k + 1) |^ g) * (k + 1)) * u) by A19, A31, A32, NEWTON:6
.= (s * (k + 1)) * (((k + 1) |^ g) * u)
.= ((k + 1) |^ (((k + 1) |-count n) + 1)) * (((k + 1) |^ g) * u) by NEWTON:6 ;
then (k + 1) |^ (((k + 1) |-count n) + 1) divides n ;
hence contradiction by A18, NAT_3:def 7; :: thesis:

end;

support (ppf t) c= support (ppf n) by A9, A19, A22, NAT_3:45;
then x in support (Euler_factorization n) by A10, A12, A24, A25, A27;
then x <= k + 1 by A11, A7, FINSEQ_1:1;
then x < k + 1 by A29, XXREAL_0:1;
then A33: x <= k by NAT_1:13;
x is Prime by A28, NAT_3:34;
then 1 <= x by INT_2:def 4;
hence x in Seg k by A33; :: thesis:

end;

A34: s,t are_coprime

proof

set u = s gcd t;
A35: s gcd t divides t by NAT_D:def 5;
A36: 0 + 1 <= s gcd t by NAT_1:13;
assume s gcd t <> 1 ; :: according to INT_2:def 3 :: thesis:
then s gcd t > 1 by A36, XXREAL_0:1;
then s gcd t >= 1 + 1 by NAT_1:13;
then consider r being Element of NAT such that
A37: r is prime and
A38: r divides s gcd t by INT_2:31;
s gcd t divides s by NAT_D:def 5;
then r divides s by A38, NAT_D:4;
then ( r = 1 or r = k + 1 ) by A17, A37, NAT_3:5, INT_2:def 4;
then k + 1 in support (pfexp t) by A37, A38, A35, NAT_D:4, NAT_3:37;
then k + 1 <= k by A26, A24, A25, A22, FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis:

end;

consider f being FinSequence of COMPLEX such that
A39: Product ((EmptyBag SetPrimes) +* (Euler_factorization s)) = Product f and
A40: f = ((EmptyBag SetPrimes) +* (Euler_factorization s)) * (canFS (support ((EmptyBag SetPrimes) +* (Euler_factorization s)))) by NAT_3:def 5;
A41: dom (Euler_factorization s) = support (ppf s) by Def1
.= support (pfexp s) by NAT_3:def 9 ;
A42: support (pfexp s) = {(k + 1)} by A17, A21, NAT_3:42;
then A43: k + 1 in dom (Euler_factorization s) by A41, TARSKI:def 1;
A44: support (Euler_factorization s) c= dom (Euler_factorization s) by PRE_POLY:37;
consider c being non zero Nat such that
A45: ( c = (k + 1) |-count s & (Euler_factorization s) . (k + 1) = ((k + 1) |^ c) - ((k + 1) |^ (c - 1)) ) by A43, Def1;
A46: c -' 1 = c - 1 by XREAL_0:def 2;
{(k + 1)} c= support (Euler_factorization s)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume x in {(k + 1)} ; :: thesis:
then A47: x = k + 1 by TARSKI:def 1;
c - 1 < c - 0 by XREAL_1:15;
then (Euler_factorization s) . (k + 1) <> 0 by A45, A18, PEPIN:66;
hence x in support (Euler_factorization s) by A47, PRE_POLY:def 7; :: thesis:

end;

then support (Euler_factorization s) = {(k + 1)} by A41, A42, A44, XBOOLE_0:def 10;
then A48: support ((EmptyBag SetPrimes) +* (Euler_factorization s)) = {(k + 1)} by Th12;
then f = ((EmptyBag SetPrimes) +* (Euler_factorization s)) * <*(k + 1)*> by A40, FINSEQ_1:94
.= <*(((EmptyBag SetPrimes) +* (Euler_factorization s)) . (k + 1))*> by A13, A20, FINSEQ_2:34 ;
then A49: Product ((EmptyBag SetPrimes) +* (Euler_factorization s)) = (Euler_factorization s) . (k + 1) by A39, A43, FUNCT_4:13
.= Euler s by A17, A45, A46, NAT_1:14, INT_8:8 ;
Product (((EmptyBag SetPrimes) +* (Euler_factorization s)) + ((EmptyBag SetPrimes) +* (Euler_factorization t))) = (Product ((EmptyBag SetPrimes) +* (Euler_factorization s))) * (Product ((EmptyBag SetPrimes) +* (Euler_factorization t))) by A23, A24, A34, A48, A41, A42, Th24, NAT_3:19;
then A50: Product (((EmptyBag SetPrimes) +* (Euler_factorization s)) + ((EmptyBag SetPrimes) +* (Euler_factorization t))) = (Euler s) * (Euler t) by A6, A49, A23, A26;
Euler n = (Euler s) * (Euler t) by A19, A34, EULER_1:21;
hence Product ((EmptyBag SetPrimes) +* (Euler_factorization n)) = Euler n by A50, A19, A34, Th25; :: thesis:

end;

end;

end;

A51: for k being Nat holds S₁[k] from NAT_1:sch 2(A1, A5);
set G = (EmptyBag SetPrimes) +* (Euler_factorization n);
A52: support ((EmptyBag SetPrimes) +* (Euler_factorization n)) = support (Euler_factorization n) by Th12;

per cases ;

suppose A53: support ((EmptyBag SetPrimes) +* (Euler_factorization n)) is empty ; :: thesis:

then A54: n = 1 by A52, Th22, NAT_1:53;
(EmptyBag SetPrimes) +* (Euler_factorization n) = EmptyBag SetPrimes by A53, PRE_POLY:81;
hence Product ((EmptyBag SetPrimes) +* (Euler_factorization n)) = Euler n by A54, NAT_3:20, EULER_1:17; :: thesis:

end;

suppose not support ((EmptyBag SetPrimes) +* (Euler_factorization n)) is empty ; :: thesis:

then reconsider M = support ((EmptyBag SetPrimes) +* (Euler_factorization n)) as non empty finite Subset of NAT by XBOOLE_1:1;
A55: max M is Nat by TARSKI:1;
support ((EmptyBag SetPrimes) +* (Euler_factorization n)) c= Seg (max M)

proof

let x be object ; :: according to TARSKI:def 3 :: thesis:
assume A56: x in support ((EmptyBag SetPrimes) +* (Euler_factorization n)) ; :: thesis:
then reconsider m = x as Nat ;
A57: support ((EmptyBag SetPrimes) +* (Euler_factorization n)) = support (Euler_factorization n) by Th12;
support (Euler_factorization n) c= dom (Euler_factorization n) by PRE_POLY:37;
then x is Prime by A56, A57, Th17;
then A58: 1 <= m by INT_2:def 4;
m <= max M by A56, XXREAL_2:def 8;
hence x in Seg (max M) by A58; :: thesis:

end;

hence Euler n = Product ((EmptyBag SetPrimes) +* (Euler_factorization n)) by A51, A55; :: thesis:

end;

end;