let m, n be Nat; ( PrimeDivisors n = {m} implies ( m |-count n >= 1 & n = m |^ (m |-count n) ) )
assume a1:
PrimeDivisors n = {m}
; ( m |-count n >= 1 & n = m |^ (m |-count n) )
a2:
m in {m}
by TARSKI:def 1;
then consider P being Prime such that
a3:
( P = m & P divides n )
by a1;
set k = m |-count n;
m |-count n >= 0 + 1
by a1, a3, PrimeSet0, MOEBIUS1:6, NAT_1:13;
hence
m |-count n >= 1
; n = m |^ (m |-count n)
reconsider n = n as non zero Nat by a1, PrimeSet0;
a4:
support (pfexp n) = PrimeDivisors n
by NUMBER14:48;
consider f being FinSequence of COMPLEX such that
a5:
Product (ppf n) = Product f
and
a6:
f = (ppf n) * (canFS (support (ppf n)))
by NAT_3:def 5;
a7:
support (ppf n) c= dom (ppf n)
by PRE_POLY:37;
a8:
support (ppf n) = support (pfexp n)
by NAT_3:def 9;
then f =
(ppf n) * (canFS {m})
by a1, a6, NUMBER14:48
.=
(ppf n) * <*m*>
by FINSEQ_1:94
.=
<*((ppf n) . m)*>
by a1, a2, a4, a7, a8, FINSEQ_2:34
.=
<*(m |^ (m |-count n))*>
by a1, a2, a4, NAT_3:def 9
;
hence
n = m |^ (m |-count n)
by a5, NAT_3:61; verum