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

proof

let n be non zero natural number ; :: thesis: ( support (PFactors n) c= Seg 0 implies for p being Prime holds p |-count (Radical n) <= 1 )
assume A2: support (PFactors n) c= Seg 0 ; :: thesis: for p being Prime holds p |-count (Radical n) <= 1
{} c= support (PFactors n) by XBOOLE_1:2;
then support (PFactors n) = {} by A2, XBOOLE_0:def 10;
then A3: PFactors n = EmptyBag SetPrimes by BAGORDER:20;
let p be Prime; :: thesis: p |-count (Radical n) <= 1
not p divides Radical n

proof

assume p divides Radical n ; :: thesis: contradiction
then ( p divides 1 & 1 divides p ) by A3, NAT_3:20, NAT_D:6;
then p = 1 by NAT_D:5;
hence contradiction by INT_2:def 5; :: thesis: verum

end;

hence p |-count (Radical n) <= 1 by Th6; :: thesis: verum

end;

A4: 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 A5: S₁[k] ; :: thesis: S₁[k + 1]
let n be non zero natural number ; :: thesis: ( support (PFactors n) c= Seg (k + 1) implies for p being Prime holds p |-count (Radical n) <= 1 )
assume A6: support (PFactors n) c= Seg (k + 1) ; :: thesis: for p being Prime holds p |-count (Radical n) <= 1
A7: 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 A8: not support (PFactors n) c= Seg k ; :: thesis: for p being Prime holds p |-count (Radical n) <= 1

A9: now

assume A10: 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 A11: x in support (PFactors n) ; :: thesis: x in Seg k
then A12: x is Prime by A7, NAT_3:34;
reconsider m = x as natural number by A11;
A13: 1 <= m by A12, INT_2:def 5;
m <= k + 1 by A6, A11, FINSEQ_1:3;
then m < k + 1 by A10, A11, XXREAL_0:1;
then m <= k by NAT_1:13;
hence x in Seg k by A13, FINSEQ_1:3; :: thesis: verum

end;

hence contradiction by A8; :: thesis: verum

end;

reconsider r = k + 1 as non zero Element of NAT ;
set e = r |-count n;
set s = r |^ (r |-count n);
A14: r is Prime by A7, A9, NAT_3:34;
then A15: (pfexp n) . r = r |-count n by NAT_3:def 8;
A16: r > 1 by A14, INT_2:def 5;
then r |^ (r |-count n) divides n by NAT_3:def 7;
then consider t being Nat such that
A17: n = (r |^ (r |-count n)) * t by NAT_D:def 3;
reconsider s = r |^ (r |-count n), t = t as non zero natural number by A17;
let p be Prime; :: thesis: p |-count (Radical n) <= 1
A18: 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 A19: x in support (PFactors t) ; :: thesis: x in Seg k
then A20: x in support (pfexp t) by Def6;
then A21: x is Prime by NAT_3:34;
reconsider m = x as natural number by A20;
A22: 1 <= m by A21, INT_2:def 5;
support (pfexp t) c= support (pfexp n) by A17, NAT_3:45;
then support (PFactors t) c= support (PFactors n) by A7, Def6;
then m in support (PFactors n) by A19;
then A23: m <= k + 1 by A6, FINSEQ_1:3;
set f = r |-count t;

now

assume A24: m = r ; :: thesis: contradiction
(pfexp t) . r = r |-count t by A14, NAT_3:def 8;
then r |-count t <> 0 by A20, A24, POLYNOM1:def 7;
then r |-count t > 0 ;
then r |-count t >= 0 + 1 by NAT_1:13;
then consider g being Nat such that
A25: r |-count t = 1 + g by NAT_1:10;
reconsider g = g as Element of NAT by ORDINAL1:def 13;
r |^ (r |-count t) divides t by A16, NAT_3:def 7;
then consider u being Nat such that
A26: t = (r |^ (r |-count t)) * u by NAT_D:def 3;
n = s * (((r |^ g) * r) * u) by A17, A25, A26, NEWTON:11
.= (s * r) * ((r |^ g) * u)
.= (r |^ ((r |-count n) + 1)) * ((r |^ g) * u) by NEWTON:11 ;
then r |^ ((r |-count n) + 1) divides n by NAT_D:def 3;
hence contradiction by A16, NAT_3:def 7; :: thesis: verum

end;

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

end;

A27: r |-count n <> 0 by A7, A9, A15, POLYNOM1:def 7;
A28: support (ppf s) = support (pfexp s) by NAT_3:def 9;
then A29: support (ppf s) = {r} by A14, A27, NAT_3:42;

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 = r by A29, A31, TARSKI:def 1;
then r <= k by A18, 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 w being Element of NAT such that
A37: w is prime and
A38: w divides s1 gcd t1 by INT_2:48;
w divides s1 by A36, A38, NAT_D:4;
then w divides r by A37, NAT_3:5;
then A39: ( w = 1 or w = r ) by A14, INT_2:def 5;
s1 gcd t1 divides t1 by NAT_D:def 5;
then r divides t1 by A37, A38, A39, INT_2:def 5, NAT_D:4;
then r in support (pfexp t) by A14, NAT_3:37;
then r in support (PFactors t) by Def6;
then k + 1 <= k by A18, FINSEQ_1:3;
hence contradiction by NAT_1:13; :: thesis: verum

end;

support (ppf t) = support (pfexp t) by NAT_3:def 9;
then A40: ( support (ppf s) = support (PFactors s) & support (ppf t) = support (PFactors t) ) by A28, Def6;
A41: Radical n = Product ((PFactors s) + (PFactors t)) by A17, A34, Th50
.= (Radical s) * (Radical t) by A30, A40, NAT_3:19 ;
A42: ( p |-count (Radical s) <= p |-count s & p |-count (Radical t) <= p |-count t ) by Th55, NAT_3:30;
A43: ( p |-count (Radical s) = 0 or p |-count (Radical t) = 0 )

proof

assume ( p |-count (Radical s) <> 0 & p |-count (Radical t) <> 0 ) ; :: thesis: contradiction
then ( p |-count s > 0 & p |-count t > 0 ) by A42;
then ( (PFactors s) . p <> 0 & (PFactors t) . p <> 0 ) by Th49;
then ( p in support (PFactors s) & p in support (PFactors t) ) by POLYNOM1:def 7;
hence contradiction by A30, A40, XBOOLE_0:3; :: thesis: verum

end;

A44: p |-count (Radical s) <= 1

proof

per cases ( p = r or p <> r ) ;

suppose A45: p = r ; :: thesis: p |-count (Radical s) <= 1

then A46: Radical s = r by A27, Th54;
p > 1 by INT_2:def 5;
hence p |-count (Radical s) <= 1 by A45, A46, NAT_3:22; :: thesis: verum

end;

suppose p <> r ; :: thesis: p |-count (Radical s) <= 1

then p,r are_relative_prime by A14, INT_2:47;
then A47: not p divides r by PYTHTRIP:def 2;
A48: p > 1 by INT_2:def 5;
p |-count s = (r |-count n) * (p |-count r) by NAT_3:32
.= (r |-count n) * 0 by A47, A48, NAT_3:27
.= 0 ;
hence p |-count (Radical s) <= 1 by Th55, NAT_3:30; :: thesis: verum

end;

end;

end;

p |-count (Radical n) = (p |-count (Radical t)) + (p |-count (Radical s)) by A41, NAT_3:28;
hence p |-count (Radical n) <= 1 by A5, A18, A43, A44; :: thesis: verum

end;

suppose support (PFactors n) c= Seg k ; :: thesis: for p being Prime holds p |-count (Radical n) <= 1

hence for p being Prime holds p |-count (Radical n) <= 1 by A5; :: thesis: verum

end;

end;

end;

A49: for k being natural number holds S₁[k] from NAT_1:sch 2(A1, A4);
consider mS being Element of NAT such that
A50: 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 p |-count (Radical n) <= 1 by A49, A50; :: thesis: verum