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

proof

let n be non zero natural number ; :: thesis: ( support (PFactors n) c= Seg 0 implies Radical n divides n )
assume A2: support (PFactors n) c= Seg 0 ; :: thesis: Radical n divides n
{} c= support (PFactors n) by XBOOLE_1:2;
then support (PFactors n) = {} by A2, XBOOLE_0:def 10;
then PFactors n = EmptyBag SetPrimes by BAGORDER:20;
then Radical n = 1 by NAT_3:20;
hence Radical n divides n by NAT_D:6; :: thesis: verum

end;

A3: 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 A4: S₁[k] ; :: thesis: S₁[k + 1]
let n be non zero natural number ; :: thesis: ( support (PFactors n) c= Seg (k + 1) implies Radical n divides n )
assume A5: support (PFactors n) c= Seg (k + 1) ; :: thesis: Radical n divides n
A6: support (pfexp n) = support (PFactors n) by Def6;

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

suppose A7: not support (PFactors n) c= Seg k ; :: thesis: Radical n divides n

A8: now

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

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in support (PFactors n) or x in Seg k )
assume A10: x in support (PFactors n) ; :: thesis: x in Seg k
then A11: x is Prime by A6, NAT_3:34;
reconsider m = x as natural number by A10;
A12: 1 <= m by A11, INT_2:def 5;
m <= k + 1 by A5, A10, FINSEQ_1:3;
then m < k + 1 by A9, A10, XXREAL_0:1;
then m <= k by NAT_1:13;
hence x in Seg k by A12, FINSEQ_1:3; :: thesis: verum

end;

hence contradiction by A7; :: thesis: verum

end;

set p = k + 1;
set e = (k + 1) |-count n;
set s = (k + 1) |^ ((k + 1) |-count n);
A13: k + 1 is Prime by A6, A8, NAT_3:34;
then A14: (pfexp n) . (k + 1) = (k + 1) |-count n by NAT_3:def 8;
A15: k + 1 > 1 by A13, INT_2:def 5;
then (k + 1) |^ ((k + 1) |-count n) divides n by NAT_3:def 7;
then consider t being Nat such that
A16: 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 zero natural number by A16;
A17: support (PFactors t) c= Seg k

proof

let x be set ; :: according to TARSKI:def 3 :: thesis: ( not x in support (PFactors t) or x in Seg k )
assume A18: x in support (PFactors t) ; :: thesis: x in Seg k
then A19: x in support (pfexp t) by Def6;
then A20: x is Prime by NAT_3:34;
reconsider m = x as natural number by A19;
A21: 1 <= m by A20, INT_2:def 5;
support (pfexp t) c= support (pfexp n) by A16, NAT_3:45;
then support (PFactors t) c= support (PFactors n) by A6, Def6;
then m in support (PFactors n) by A18;
then A22: m <= k + 1 by A5, FINSEQ_1:3;
set f = (k + 1) |-count t;

now

assume A23: m = k + 1 ; :: thesis: contradiction
(pfexp t) . (k + 1) = (k + 1) |-count t by A13, NAT_3:def 8;
then (k + 1) |-count t <> 0 by A19, A23, 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
A24: (k + 1) |-count t = 1 + g by NAT_1:10;
reconsider g = g as Element of NAT by ORDINAL1:def 13;
(k + 1) |^ ((k + 1) |-count t) divides t by A15, NAT_3:def 7;
then consider u being Nat such that
A25: t = ((k + 1) |^ ((k + 1) |-count t)) * u by NAT_D:def 3;
n = s * ((((k + 1) |^ g) * (k + 1)) * u) by A16, A24, A25, 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 A15, NAT_3:def 7; :: thesis: verum

end;

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

end;

A26: (k + 1) |-count n <> 0 by A6, A8, A14, POLYNOM1:def 7;
A27: support (ppf s) = support (pfexp s) by NAT_3:def 9;
then A28: support (ppf s) = {(k + 1)} by A13, A26, NAT_3:42;
then A29: support (PFactors s) = {(k + 1)} by A27, Def6;

A30: now

assume support (ppf s) meets support (ppf t) ; :: thesis: contradiction
then consider x being set such that
A31: x in support (ppf s) and
A32: x in support (ppf t) by XBOOLE_0:3;
x in support (pfexp t) by A32, NAT_3:def 9;
then A33: x in support (PFactors t) by Def6;
x = k + 1 by A28, A31, TARSKI:def 1;
then k + 1 <= k by A17, A33, FINSEQ_1:3;
hence contradiction by NAT_1:13; :: thesis: verum

end;

reconsider s1 = s, t1 = t as non zero Element of NAT by ORDINAL1:def 13;
A34: s1,t1 are_relative_prime

proof

assume not s1,t1 are_relative_prime ; :: thesis: contradiction
then A35: s1 gcd t1 <> 1 by INT_2:def 4;
set u = s1 gcd t1;
A36: 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 A35, XXREAL_0:1;
then s1 gcd t1 >= 1 + 1 by NAT_1:13;
then consider r being Element of NAT such that
A37: r is prime and
A38: r divides s1 gcd t1 by INT_2:48;
r divides s1 by A36, A38, NAT_D:4;
then r divides k + 1 by A37, NAT_3:5;
then A39: ( r = 1 or r = k + 1 ) by A13, INT_2:def 5;
s1 gcd t1 divides t1 by NAT_D:def 5;
then k + 1 divides t1 by A37, A38, A39, INT_2:def 5, NAT_D:4;
then k + 1 in support (pfexp t) by A13, NAT_3:37;
then k + 1 in support (PFactors t) by Def6;
then k + 1 <= k by A17, FINSEQ_1:3;
hence contradiction by NAT_1:13; :: thesis: verum

end;

consider f being FinSequence of COMPLEX such that
A40: Product (PFactors s) = Product f and
A41: f = (PFactors s) * (canFS (support (PFactors s))) by NAT_3:def 5;
A42: dom (PFactors s) = SetPrimes by PARTFUN1:def 4;
A43: k + 1 in support (pfexp s) by A27, A28, TARSKI:def 1;
f = (PFactors s) * <*(k + 1)*> by A29, A41, UPROOTS:6
.= <*((PFactors s) . (k + 1))*> by A8, A42, CIRCCMB3:36 ;
then A44: Product (PFactors s) = (PFactors s) . (k + 1) by A40, RVSUM_1:125
.= k + 1 by A43, Def6 ;
support (ppf t) = support (pfexp t) by NAT_3:def 9;
then A45: ( support (ppf s) = support (PFactors s) & support (ppf t) = support (PFactors t) ) by A27, Def6;
A46: ( Radical s divides s & Radical t divides t ) by A4, A17, A26, A44, NAT_3:3;
Radical n = Product ((PFactors s) + (PFactors t)) by A16, A34, Th50
.= (Radical s) * (Radical t) by A30, A45, NAT_3:19 ;
hence Radical n divides n by A16, A46, NAT_3:1; :: thesis: verum

end;

suppose support (PFactors n) c= Seg k ; :: thesis: Radical n divides n

hence Radical n divides n by A4; :: thesis: verum

end;

end;

end;

A47: for k being natural number holds S₁[k] from NAT_1:sch 2(A1, A3);
consider mS being Element of NAT such that
A48: support (ppf n) c= Seg mS by Th14;
support (ppf n) = support (pfexp n) by NAT_3:def 9
.= support (PFactors n) by Def6 ;
hence Radical n divides n by A47, A48; :: thesis: verum