let n be non zero Nat; ( Radical n = 1 iff n = 1 )
thus
( Radical n = 1 implies n = 1 )
( n = 1 implies Radical n = 1 )proof
A1:
rng (PFactors n) c= NAT
by VALUED_0:def 6;
consider f being
FinSequence of
COMPLEX such that A2:
Product (PFactors n) = Product f
and A3:
f = (PFactors n) * (canFS (support (PFactors n)))
by NAT_3:def 5;
rng f c= rng (PFactors n)
by A3, RELAT_1:26;
then
rng f c= NAT
by A1;
then reconsider f =
f as
FinSequence of
NAT by FINSEQ_1:def 4;
assume A4:
Radical n = 1
;
n = 1
assume
n <> 1
;
contradiction
then consider p being
Prime such that A5:
p divides n
by Th5;
A6:
p in support (pfexp n)
by A5, NAT_3:37;
then A7:
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 A8:
(
y in dom (canFS (support (PFactors n))) &
p = (canFS (support (PFactors n))) . y )
by FUNCT_1:def 3;
(PFactors n) . p = p
by A6, Def6;
then A9:
f . y = p
by A3, A8, FUNCT_1:13;
support (PFactors n) c= dom (PFactors n)
by PRE_POLY:37;
then
y in dom f
by A3, A7, A8, FUNCT_1:11;
then
( 1
< p &
p in rng f )
by A9, FUNCT_1:3, INT_2:def 4;
hence
contradiction
by A4, A2, NAT_3:7, NAT_D:7;
verum
end;
thus
( n = 1 implies Radical n = 1 )
by Th45, NAT_3:20; verum