let p be Prime; :: thesis: for n being non zero Nat holds

( p divides n iff p divides Radical n )

let n be non zero Nat; :: thesis: ( p divides n iff p divides Radical n )

thus ( p divides n implies p divides Radical n ) :: thesis: ( p divides Radical n implies p divides n )

Radical n divides n by Th55;

hence p divides n by A11, NAT_D:4; :: thesis: verum

( p divides n iff p divides Radical n )

let n be non zero Nat; :: thesis: ( p divides n iff p divides Radical n )

thus ( p divides n implies p divides Radical n ) :: thesis: ( p divides Radical n implies p divides n )

proof

assume A11:
p divides Radical n
; :: thesis: p divides n
assume that

A1: p divides n and

A2: not p divides Radical n ; :: thesis: 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; :: thesis: verum

end;A1: p divides n and

A2: not p divides Radical n ; :: thesis: 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; :: thesis: verum

Radical n divides n by Th55;

hence p divides n by A11, NAT_D:4; :: thesis: verum