let n be non empty natural number ; :: thesis: Product (ppf n) = n
defpred S₁[ natural number ] means for n being non empty natural number st support (ppf n) c= Seg $1 holds
Product (ppf n) = n;
A1: S₁[ 0 ]

proof

let n be non empty natural number ; :: thesis: ( support (ppf n) c= Seg 0 implies Product (ppf n) = n )
assume A2: support (ppf n) c= Seg 0 ; :: thesis: Product (ppf n) = n
{} c= support (ppf n) by XBOOLE_1:2;
then A3: support (ppf n) = {} by A2, XBOOLE_0:def 10;
then A4: ppf n = EmptyBag SetPrimes by BAGORDER:20;

now

reconsider k = n as Nat ;
assume n <> 1 ; :: thesis: contradiction
then k > 1 by UPROOTS:1;
then k >= 1 + 1 by NAT_1:13;
then consider p being Element of NAT such that
A5: p is prime and
A6: p divides k by INT_2:48;
not support (pfexp n) is empty by A5, A6, Th37;
hence contradiction by A3, Def9; :: thesis: verum

end;

hence Product (ppf n) = n by A4, Th20; :: thesis: verum

end;

A7: for k being natural number st S₁[k] holds
S₁[k + 1]

proof

let k be natural number ; :: thesis: ( S₁[k] implies S₁[k + 1] )
assume A8: S₁[k] ; :: thesis: S₁[k + 1]
let n be non empty natural number ; :: thesis: ( support (ppf n) c= Seg (k + 1) implies Product (ppf n) = n )
assume A9: support (ppf n) c= Seg (k + 1) ; :: thesis: Product (ppf n) = n
A10: support (ppf n) = support (pfexp n) by Def9;

per cases ( not support (ppf n) c= Seg k or support (ppf n) c= Seg k ) ;

suppose A11: not support (ppf n) c= Seg k ; :: thesis: Product (ppf n) = n

A12: now

assume A13: not k + 1 in support (ppf n) ; :: thesis: contradiction
support (ppf n) c= Seg k

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in support (ppf n) or x in Seg k )
assume A14: x in support (ppf n) ; :: thesis: x in Seg k
then A15: x is Prime by A10, Th34;
reconsider m = x as natural number by A14;
A16: 1 <= m by A15, INT_2:def 5;
m <= k + 1 by A9, A14, FINSEQ_1:3;
then m < k + 1 by A13, A14, XXREAL_0:1;
then m <= k by NAT_1:13;
hence x in Seg k by A16, FINSEQ_1:3; :: thesis: verum

end;

hence contradiction by A11; :: thesis: verum

end;

set p = k + 1;
set e = (k + 1) |-count n;
set s = (k + 1) |^ ((k + 1) |-count n);
A17: k + 1 is Prime by A10, A12, Th34;
then A18: (pfexp n) . (k + 1) = (k + 1) |-count n by Def8;
A19: k + 1 > 1 by A17, INT_2:def 5;
then (k + 1) |^ ((k + 1) |-count n) divides n by Def7;
then consider t being Nat such that
A20: n = ((k + 1) |^ ((k + 1) |-count n)) * t by NAT_D:def 3;
reconsider s = (k + 1) |^ ((k + 1) |-count n), t = t as non empty natural number by A20;
A21: support (ppf t) = support (pfexp t) by Def9;
A22: support (ppf t) c= Seg k

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in support (ppf t) or x in Seg k )
assume A23: x in support (ppf t) ; :: thesis: x in Seg k
then A24: x in support (pfexp t) by Def9;
then A25: x is Prime by Th34;
reconsider m = x as natural number by A24;
A26: 1 <= m by A25, INT_2:def 5;
support (ppf t) c= support (ppf n) by A10, A20, A21, Th45;
then m in support (ppf n) by A23;
then A27: m <= k + 1 by A9, FINSEQ_1:3;
set f = (k + 1) |-count t;

now

assume A28: m = k + 1 ; :: thesis: contradiction
(pfexp t) . (k + 1) = (k + 1) |-count t by A17, Def8;
then (k + 1) |-count t <> 0 by A24, A28, POLYNOM1:def 7;
then (k + 1) |-count t > 0 ;
then (k + 1) |-count t >= 0 + 1 by NAT_1:13;
then consider g being Nat such that
A29: (k + 1) |-count t = 1 + g by NAT_1:10;
(k + 1) |^ ((k + 1) |-count t) divides t by A19, Def7;
then consider u being Nat such that
A30: t = ((k + 1) |^ ((k + 1) |-count t)) * u by NAT_D:def 3;
n = s * ((((k + 1) |^ g) * (k + 1)) * u) by A20, A29, A30, NEWTON:11
.= (s * (k + 1)) * (((k + 1) |^ g) * u)
.= ((k + 1) |^ (((k + 1) |-count n) + 1)) * (((k + 1) |^ g) * u) by NEWTON:11 ;
then (k + 1) |^ (((k + 1) |-count n) + 1) divides n by NAT_D:def 3;
hence contradiction by A19, Def7; :: thesis: verum

end;

then m < k + 1 by A27, XXREAL_0:1;
then m <= k by NAT_1:13;
hence x in Seg k by A26, FINSEQ_1:3; :: thesis: verum

end;

A31: (k + 1) |-count n <> 0 by A10, A12, A18, POLYNOM1:def 7;
support (ppf s) = support (pfexp s) by Def9;
then A32: support (ppf s) = {(k + 1)} by A17, A31, Th42;

now

assume (support (ppf s)) /\ (support (ppf t)) <> {} ; :: thesis: contradiction
then consider x being set such that
A33: x in (support (ppf s)) /\ (support (ppf t)) by XBOOLE_0:def 1;
A34: x in support (ppf s) by A33, XBOOLE_0:def 4;
A35: x in support (ppf t) by A33, XBOOLE_0:def 4;
x = k + 1 by A32, A34, TARSKI:def 1;
then k + 1 <= k by A22, A35, FINSEQ_1:3;
hence contradiction by NAT_1:13; :: thesis: verum

end;

then A36: support (ppf s) misses support (ppf t) by XBOOLE_0:def 7;
reconsider s1 = s, t1 = t as non empty Nat ;
s1,t1 are_relative_prime

proof

assume A37: s1 gcd t1 <> 1 ; :: according to INT_2:def 4 :: thesis: contradiction
set u = s1 gcd t1;
A38: s1 gcd t1 divides s1 by NAT_D:def 5;
s1 gcd t1 <> 0 by INT_2:5;
then 0 < s1 gcd t1 ;
then 0 + 1 <= s1 gcd t1 by NAT_1:13;
then s1 gcd t1 > 1 by A37, XXREAL_0:1;
then s1 gcd t1 >= 1 + 1 by NAT_1:13;
then consider r being Element of NAT such that
A39: r is prime and
A40: r divides s1 gcd t1 by INT_2:48;
r divides s1 by A38, A40, NAT_D:4;
then r divides k + 1 by A39, Th5;
then A41: ( r = 1 or r = k + 1 ) by A17, INT_2:def 5;
s1 gcd t1 divides t1 by NAT_D:def 5;
then k + 1 divides t1 by A39, A40, A41, INT_2:def 5, NAT_D:4;
then k + 1 in support (pfexp t) by A17, Th37;
then k + 1 <= k by A21, A22, FINSEQ_1:3;
hence contradiction by NAT_1:13; :: thesis: verum

end;

then A42: ppf n = (ppf s) + (ppf t) by A20, Th58;
consider f being FinSequence of COMPLEX such that
A43: Product (ppf s) = Product f and
A44: f = (ppf s) * (canFS (support (ppf s))) by Def5;
A45: dom (ppf s) = SetPrimes by PARTFUN1:def 4;
f = (ppf s) * <*(k + 1)*> by A32, A44, UPROOTS:6
.= <*((ppf s) . (k + 1))*> by A12, A45, CIRCCMB3:36 ;
then A46: Product (ppf s) = (ppf s) . (k + 1) by A43, RVSUM_1:125
.= s by A17, A31, Th59 ;
Product (ppf t) = t by A8, A22;
hence Product (ppf n) = n by A20, A36, A42, A46, Th19; :: thesis: verum

end;

suppose support (ppf n) c= Seg k ; :: thesis: Product (ppf n) = n

hence Product (ppf n) = n by A8; :: thesis: verum

end;

end;

end;

A47: for k being natural number holds S₁[k] from NAT_1:sch 2(A1, A7);
A48: support (ppf n) = support (pfexp n) by Def9;

per cases ( support (ppf n) is empty or not support (ppf n) is empty ) ;

suppose support (ppf n) is empty ; :: thesis: Product (ppf n) = n

hence Product (ppf n) = n by A1; :: thesis: verum

end;

suppose not support (ppf n) is empty ; :: thesis: Product (ppf n) = n

then reconsider S = support (ppf n) as non empty finite Subset of NAT by XBOOLE_1:1;
support (ppf n) c= Seg (max S)

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in support (ppf n) or x in Seg (max S) )
assume A49: x in support (ppf n) ; :: thesis: x in Seg (max S)
then A50: x is Prime by A48, Th34;
reconsider m = x as natural number by A49;
A51: 1 <= m by A50, INT_2:def 5;
m <= max S by A49, XXREAL_2:def 8;
hence x in Seg (max S) by A51, FINSEQ_1:3; :: thesis: verum

end;

hence Product (ppf n) = n by A47; :: thesis: verum

end;

end;