let n be non zero natural number ; :: thesis: ( Radical n = 1 iff n = 1 )
thus
( Radical n = 1 implies n = 1 )
:: thesis: ( n = 1 implies Radical n = 1 )proof
assume A1:
Radical n = 1
;
:: thesis: n = 1
assume
n <> 1
;
:: thesis: contradiction
then consider p being
Prime such that A2:
p divides n
by Th5;
A3:
1
< p
by INT_2:def 5;
A4:
p in support (pfexp n)
by A2, NAT_3:37;
then A5:
(PFactors n) . p = p
by Def6;
consider f being
FinSequence of
COMPLEX such that A6:
(
Product (PFactors n) = Product f &
f = (PFactors n) * (canFS (support (PFactors n))) )
by NAT_3:def 5;
A7:
rng f c= rng (PFactors n)
by A6, RELAT_1:45;
rng (PFactors n) c= NAT
by VALUED_0:def 6;
then
rng f c= NAT
by A7, XBOOLE_1:1;
then reconsider f =
f as
FinSequence of
NAT by FINSEQ_1:def 4;
A8:
support (PFactors n) c= dom (PFactors n)
by POLYNOM1:41;
A9:
p in support (PFactors n)
by A4, Def6;
then
p in rng (canFS (support (PFactors n)))
by FUNCT_2:def 3;
then consider y being
set such that A10:
(
y in dom (canFS (support (PFactors n))) &
p = (canFS (support (PFactors n))) . y )
by FUNCT_1:def 5;
A11:
y in dom f
by A6, A8, A9, A10, FUNCT_1:21;
f . y = p
by A5, A6, A10, FUNCT_1:23;
then
p in rng f
by A11, FUNCT_1:12;
hence
contradiction
by A1, A3, A6, NAT_3:7, NAT_D:7;
:: thesis: verum
end;
thus
( n = 1 implies Radical n = 1 )
by Th45, NAT_3:20; :: thesis: verum