defpred S₁[ Nat] means for n being non zero Nat st support (PFactors n) c= Seg $1 holds
for p being Prime holds p |-count (Radical n) <= 1;
let p be Prime; :: thesis: for n being non zero Nat holds p |-count (Radical n) <= 1
let n be non zero Nat; :: thesis: p |-count (Radical n) <= 1
A1: ex mS being Element of NAT st support (ppf n) c= Seg mS by Th14;
A2: support (ppf n) = support (pfexp n) by NAT_3:def 9
.= support (PFactors n) by Def6 ;
A3: for k being Nat st S₁[k] holds
S₁[k + 1]

proof

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

let p be Prime; :: thesis: p |-count (Radical n) <= 1
reconsider r = k + 1 as non zero Element of NAT ;
set e = r |-count n;
set s = r |^ (r |-count n);

A8: now :: thesis: k + 1 in support (PFactors n)

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

proof

let x be object ; :: 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 reconsider m = x as Nat ;
m <= k + 1 by A5, A10, FINSEQ_1:1;
then m < k + 1 by A9, A10, XXREAL_0:1;
then A11: m <= k by NAT_1:13;
x is Prime by A6, A10, NAT_3:34;
then 1 <= m by INT_2:def 4;
hence x in Seg k by A11, FINSEQ_1:1; :: thesis: verum

end;

hence contradiction by A7; :: thesis: verum

end;

then A12: r is Prime by A6, NAT_3:34;
then A13: r > 1 by INT_2:def 4;
then r |^ (r |-count n) divides n by NAT_3:def 7;
then consider t being Nat such that
A14: n = (r |^ (r |-count n)) * t by NAT_D:def 3;
reconsider s = r |^ (r |-count n), t = t as non zero Nat by A14;
reconsider s1 = s, t1 = t as non zero Element of NAT by ORDINAL1:def 12;
A15: support (ppf s) = support (pfexp s) by NAT_3:def 9;
then A16: support (ppf s) = support (PFactors s) by Def6;
A17: support (PFactors t) c= Seg k

proof

set f = r |-count t;
let x be object ; :: 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 reconsider m = x as Nat ;
A19: x in support (pfexp t) by A18, Def6;

A20: now :: thesis: not m = r

assume A21: m = r ; :: thesis: contradiction
(pfexp t) . r = r |-count t by A12, NAT_3:def 8;
then r |-count t <> 0 by A19, A21, PRE_POLY:def 7;
then r |-count t >= 0 + 1 by NAT_1:13;
then consider g being Nat such that
A22: r |-count t = 1 + g by NAT_1:10;
r |^ (r |-count t) divides t by A13, NAT_3:def 7;
then consider u being Nat such that
A23: t = (r |^ (r |-count t)) * u by NAT_D:def 3;
reconsider g = g as Element of NAT by ORDINAL1:def 12;
n = s * (((r |^ g) * r) * u) by A14, A22, A23, NEWTON:6
.= (s * r) * ((r |^ g) * u)
.= (r |^ ((r |-count n) + 1)) * ((r |^ g) * u) by NEWTON:6 ;
then r |^ ((r |-count n) + 1) divides n by NAT_D:def 3;
hence contradiction by A13, NAT_3:def 7; :: thesis: verum

end;

support (pfexp t) c= support (pfexp n) by A14, NAT_3:45;
then support (PFactors t) c= support (PFactors n) by A6, Def6;
then m in support (PFactors n) by A18;
then m <= k + 1 by A5, FINSEQ_1:1;
then m < r by A20, XXREAL_0:1;
then A24: m <= k by NAT_1:13;
x is Prime by A19, NAT_3:34;
then 1 <= m by INT_2:def 4;
hence x in Seg k by A24, FINSEQ_1:1; :: thesis: verum

end;

(pfexp n) . r = r |-count n by A12, NAT_3:def 8;
then A25: r |-count n <> 0 by A6, A8, PRE_POLY:def 7;
A26: p |-count (Radical s) <= 1

proof

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

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

A28: p > 1 by INT_2:def 4;
Radical s = r by A25, A27, Th54;
hence p |-count (Radical s) <= 1 by A27, A28, NAT_3:22; :: thesis: verum

end;

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

then p,r are_coprime by A12, INT_2:30;
then A29: not p divides r by PYTHTRIP:def 2;
A30: p > 1 by INT_2:def 4;
p |-count s = (r |-count n) * (p |-count r) by NAT_3:32
.= (r |-count n) * 0 by A29, A30, NAT_3:27
.= 0 ;
hence p |-count (Radical s) <= 1 by Th55, NAT_3:30; :: thesis: verum

end;

end;

end;

A31: support (ppf s) = {r} by A12, A25, A15, NAT_3:42;

A32: now :: thesis: not support (ppf s) meets support (ppf t)

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

end;

support (ppf t) = support (pfexp t) by NAT_3:def 9;
then A36: support (ppf t) = support (PFactors t) by Def6;
A37: ( p |-count (Radical s) = 0 or p |-count (Radical t) = 0 )

proof

assume that
A38: p |-count (Radical s) <> 0 and
A39: p |-count (Radical t) <> 0 ; :: thesis: contradiction
p |-count t > 0 by A39, Th55, NAT_3:30;
then (PFactors t) . p <> 0 by Th49;
then A40: p in support (PFactors t) by PRE_POLY:def 7;
p |-count s > 0 by A38, Th55, NAT_3:30;
then (PFactors s) . p <> 0 by Th49;
then p in support (PFactors s) by PRE_POLY:def 7;
hence contradiction by A32, A16, A36, A40, XBOOLE_0:3; :: thesis: verum

end;

s1,t1 are_coprime

proof

set u = s1 gcd t1;
A41: s1 gcd t1 divides t1 by NAT_D:def 5;
s1 gcd t1 <> 0 by INT_2:5;
then A42: 0 + 1 <= s1 gcd t1 by NAT_1:13;
assume not s1,t1 are_coprime ; :: thesis: contradiction
then s1 gcd t1 <> 1 by INT_2:def 3;
then s1 gcd t1 > 1 by A42, XXREAL_0:1;
then s1 gcd t1 >= 1 + 1 by NAT_1:13;
then consider w being Element of NAT such that
A43: w is prime and
A44: w divides s1 gcd t1 by INT_2:31;
s1 gcd t1 divides s1 by NAT_D:def 5;
then w divides s1 by A44, NAT_D:4;
then w divides r by A43, NAT_3:5;
then ( w = 1 or w = r ) by A12, INT_2:def 4;
then r divides t1 by A43, A44, A41, INT_2:def 4, NAT_D:4;
then r in support (pfexp t) by A12, NAT_3:37;
then r in support (PFactors t) by Def6;
then k + 1 <= k by A17, FINSEQ_1:1;
hence contradiction by NAT_1:13; :: thesis: verum

end;

then Radical n = Product ((PFactors s) + (PFactors t)) by A14, Th50
.= (Radical s) * (Radical t) by A32, A16, A36, NAT_3:19 ;
then p |-count (Radical n) = (p |-count (Radical t)) + (p |-count (Radical s)) by NAT_3:28;
hence p |-count (Radical n) <= 1 by A4, A17, A37, A26; :: 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 A4; :: thesis: verum

end;

end;

end;

A45: S₁[ 0 ]

proof

let n be non zero Nat; :: thesis: ( support (PFactors n) c= Seg 0 implies for p being Prime holds p |-count (Radical n) <= 1 )
assume A46: support (PFactors n) c= Seg 0 ; :: thesis: for p being Prime holds p |-count (Radical n) <= 1
let p be Prime; :: thesis: p |-count (Radical n) <= 1
{} c= support (PFactors n) ;
then support (PFactors n) = {} by A46;
then A47: PFactors n = EmptyBag SetPrimes by PRE_POLY:81;
not p divides Radical n

proof

assume p divides Radical n ; :: thesis: contradiction
then A48: p divides 1 by A47, NAT_3:20;
1 divides p by NAT_D:6;
then p = 1 by A48, NAT_D:5;
hence contradiction by INT_2:def 4; :: thesis: verum

end;

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

end;

for k being Nat holds S₁[k] from NAT_1:sch 2(A45, A3);
hence p |-count (Radical n) <= 1 by A1, A2; :: thesis: verum