let p be Prime; for n being non zero Nat holds
( p divides n iff p divides Radical n )
let n be non zero Nat; ( p divides n iff p divides Radical n )
thus
( p divides n implies p divides Radical n )
( p divides Radical n implies p divides n )proof
assume that A1:
p divides n
and A2:
not
p divides Radical n
;
contradiction
A3:
p in support (pfexp n)
by A1, NAT_3:37;
then A4:
p in support (PFactors n)
by Def6;
then
p in rng (canFS (support (PFactors n)))
by FUNCT_2:def 3;
then consider y being
object such that A5:
y in dom (canFS (support (PFactors n)))
and A6:
p = (canFS (support (PFactors n))) . y
by FUNCT_1:def 3;
consider f being
FinSequence of
COMPLEX such that A7:
Product (PFactors n) = Product f
and A8:
f = (PFactors n) * (canFS (support (PFactors n)))
by NAT_3:def 5;
(
rng (PFactors n) c= NAT &
rng f c= rng (PFactors n) )
by A8, RELAT_1:26, VALUED_0:def 6;
then A9:
rng f c= NAT
;
support (PFactors n) c= dom (PFactors n)
by PRE_POLY:37;
then A10:
y in dom f
by A4, A8, A5, A6, FUNCT_1:11;
reconsider f =
f as
FinSequence of
NAT by A9, FINSEQ_1:def 4;
(PFactors n) . p = p
by A3, Def6;
then
f . y = p
by A8, A6, A10, FUNCT_1:12;
then
p in rng f
by A10, FUNCT_1:3;
hence
contradiction
by A2, A7, NAT_3:7;
verum
end;
assume A11:
p divides Radical n
; p divides n
Radical n divides n
by Th55;
hence
p divides n
by A11, NAT_D:4; verum