let k be non zero Nat; :: thesis: ( k is square-free implies Radical k = k )

assume A1: k is square-free ; :: thesis: Radical k = k

for i being object st i in SetPrimes holds

(PFactors k) . i = (ppf k) . i

hence Radical k = k by NAT_3:61; :: thesis: verum

assume A1: k is square-free ; :: thesis: Radical k = k

for i being object st i in SetPrimes holds

(PFactors k) . i = (ppf k) . i

proof

then
PFactors k = ppf k
by PBOOLE:3;
let i be object ; :: thesis: ( i in SetPrimes implies (PFactors k) . i = (ppf k) . i )

assume i in SetPrimes ; :: thesis: (PFactors k) . i = (ppf k) . i

then reconsider p = i as prime Element of NAT by NEWTON:def 6;

end;assume i in SetPrimes ; :: thesis: (PFactors k) . i = (ppf k) . i

then reconsider p = i as prime Element of NAT by NEWTON:def 6;

per cases
( p in support (pfexp k) or not p in support (pfexp k) )
;

end;

suppose A2:
p in support (pfexp k)
; :: thesis: (PFactors k) . i = (ppf k) . i

A3:
p <> 1
by INT_2:def 4;

p |-count k <> 0

p |-count k <= 1 by A1, Th24;

then p |-count k = 1 by A4, XXREAL_0:1;

then (ppf k) . p = p |^ 1 by A2, NAT_3:def 9

.= p ;

hence (PFactors k) . i = (ppf k) . i by A2, Def6; :: thesis: verum

end;p |-count k <> 0

proof

then A4:
p |-count k >= 1
by NAT_1:14;
assume
p |-count k = 0
; :: thesis: contradiction

then not p divides k by A3, NAT_3:27;

hence contradiction by A2, NAT_3:36; :: thesis: verum

end;then not p divides k by A3, NAT_3:27;

hence contradiction by A2, NAT_3:36; :: thesis: verum

p |-count k <= 1 by A1, Th24;

then p |-count k = 1 by A4, XXREAL_0:1;

then (ppf k) . p = p |^ 1 by A2, NAT_3:def 9

.= p ;

hence (PFactors k) . i = (ppf k) . i by A2, Def6; :: thesis: verum

hence Radical k = k by NAT_3:61; :: thesis: verum