let n be non zero Nat; :: thesis: Radical n > 0

assume Radical n <= 0 ; :: thesis: contradiction

then Product (PFactors n) = 0 ;

then consider f being FinSequence of COMPLEX such that

A1: Product f = 0 and

A2: f = (PFactors n) * (canFS (support (PFactors n))) by NAT_3:def 5;

for k being Nat holds

( not k in dom f or not f . k = 0 )

assume Radical n <= 0 ; :: thesis: contradiction

then Product (PFactors n) = 0 ;

then consider f being FinSequence of COMPLEX such that

A1: Product f = 0 and

A2: f = (PFactors n) * (canFS (support (PFactors n))) by NAT_3:def 5;

for k being Nat holds

( not k in dom f or not f . k = 0 )

proof

hence
contradiction
by A1, RVSUM_1:103; :: thesis: verum
given k being Nat such that A3:
k in dom f
and

A4: f . k = 0 ; :: thesis: contradiction

k in dom (canFS (support (PFactors n))) by A2, A3, FUNCT_1:11;

then A5: ( rng (canFS (support (PFactors n))) c= support (PFactors n) & (canFS (support (PFactors n))) . k in rng (canFS (support (PFactors n))) ) by FINSEQ_1:def 4, FUNCT_1:3;

then (canFS (support (PFactors n))) . k in support (PFactors n) ;

then reconsider p = (canFS (support (PFactors n))) . k as prime Element of NAT by NEWTON:def 6;

p in support (PFactors n) by A5;

then A6: p in support (pfexp n) by Def6;

f . k = (PFactors n) . p by A2, A3, FUNCT_1:12

.= p by A6, Def6 ;

hence contradiction by A4; :: thesis: verum

end;A4: f . k = 0 ; :: thesis: contradiction

k in dom (canFS (support (PFactors n))) by A2, A3, FUNCT_1:11;

then A5: ( rng (canFS (support (PFactors n))) c= support (PFactors n) & (canFS (support (PFactors n))) . k in rng (canFS (support (PFactors n))) ) by FINSEQ_1:def 4, FUNCT_1:3;

then (canFS (support (PFactors n))) . k in support (PFactors n) ;

then reconsider p = (canFS (support (PFactors n))) . k as prime Element of NAT by NEWTON:def 6;

p in support (PFactors n) by A5;

then A6: p in support (pfexp n) by Def6;

f . k = (PFactors n) . p by A2, A3, FUNCT_1:12

.= p by A6, Def6 ;

hence contradiction by A4; :: thesis: verum