let k be Nat; :: thesis: for n being non zero Element of NAT st support (ppf n) c= Seg (k + 1) holds
ex m being non zero Element of NAT ex e being Element of NAT st
( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

let n be non zero Element of NAT ; :: thesis: ( support (ppf n) c= Seg (k + 1) implies ex m being non zero Element of NAT ex e being Element of NAT st
( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) ) )

assume A1: support (ppf n) c= Seg (k + 1) ; :: thesis: ex m being non zero Element of NAT ex e being Element of NAT st
( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

per cases ( support (ppf n) c= Seg k or not support (ppf n) c= Seg k ) ;
suppose A2: support (ppf n) c= Seg k ; :: thesis: ex m being non zero Element of NAT ex e being Element of NAT st
( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

take n ; :: thesis: ex e being Element of NAT st
( support (ppf n) c= Seg k & n = n * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf n) implies p |-count n = p |-count n ) & ( not p in support (ppf n) implies p |-count n <= p |-count n ) ) ) )

take e = 0 ; :: thesis: ( support (ppf n) c= Seg k & n = n * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf n) implies p |-count n = p |-count n ) & ( not p in support (ppf n) implies p |-count n <= p |-count n ) ) ) )

(k + 1) |^ e = 1 by NEWTON:4;
hence ( support (ppf n) c= Seg k & n = n * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf n) implies p |-count n = p |-count n ) & ( not p in support (ppf n) implies p |-count n <= p |-count n ) ) ) ) by A2; :: thesis: verum
end;
suppose A3: not support (ppf n) c= Seg k ; :: thesis: ex m being non zero Element of NAT ex e being Element of NAT st
( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

reconsider r = k + 1 as non zero Element of NAT ;
set e = r |-count n;
set s = r |^ (r |-count n);
now :: thesis: k + 1 in support (ppf n)
assume A4: not k + 1 in support (ppf n) ; :: thesis: contradiction
support (ppf n) c= Seg k
proof
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (ppf n) or x in Seg k )
assume A5: x in support (ppf n) ; :: thesis: x in Seg k
then reconsider m = x as Nat ;
x in support () by ;
then x is Prime by NAT_3:34;
then A6: 1 <= m by INT_2:def 4;
m <= k + 1 by ;
then m < k + 1 by ;
then m <= k by NAT_1:13;
hence x in Seg k by ; :: thesis: verum
end;
hence contradiction by A3; :: thesis: verum
end;
then k + 1 in support () by NAT_3:def 9;
then A7: r is Prime by NAT_3:34;
then A8: r > 1 by INT_2:def 4;
then r |^ (r |-count n) divides n by NAT_3:def 7;
then consider t being Nat such that
A9: n = (r |^ (r |-count n)) * t by NAT_D:def 3;
reconsider s = r |^ (r |-count n), t = t as non zero Element of NAT by ;
A10: support (ppf t) = support () by NAT_3:def 9;
A11: support (ppf t) c= Seg k
proof
set f = r |-count t;
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (ppf t) or x in Seg k )
assume A12: x in support (ppf t) ; :: thesis: x in Seg k
then reconsider m = x as Nat ;
A13: x in support () by ;
A14: now :: thesis: not m = r
assume A15: m = r ; :: thesis: contradiction
(pfexp t) . r = r |-count t by ;
then r |-count t <> 0 by ;
then r |-count t >= 0 + 1 by NAT_1:13;
then consider g being Nat such that
A16: r |-count t = 1 + g by NAT_1:10;
r |^ (r |-count t) divides t by ;
then consider u being Nat such that
A17: t = (r |^ (r |-count t)) * u by NAT_D:def 3;
reconsider g = g as Element of NAT by ORDINAL1:def 12;
n = s * (((r |^ g) * r) * u) by
.= (s * r) * ((r |^ g) * u)
.= (r |^ ((r |-count n) + 1)) * ((r |^ g) * u) by NEWTON:6 ;
then r |^ ((r |-count n) + 1) divides n by NAT_D:def 3;
hence contradiction by A8, NAT_3:def 7; :: thesis: verum
end;
support () c= support () by ;
then support (ppf t) c= support (ppf n) by ;
then m in support (ppf n) by A12;
then m <= k + 1 by ;
then m < r by ;
then A18: m <= k by NAT_1:13;
x is Prime by ;
then 1 <= m by INT_2:def 4;
hence x in Seg k by ; :: thesis: verum
end;
A19: r |-count n <> 0
proof
assume r |-count n = 0 ; :: thesis: contradiction
then n = 1 * t by ;
hence contradiction by A3, A11; :: thesis: verum
end;
take m = t; :: thesis: ex e being Element of NAT st
( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

take e = (k + 1) |-count n; :: thesis: ( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) )

support (ppf s) = support () by NAT_3:def 9;
then A20: support (ppf s) = {r} by ;
A21: now :: thesis: not support (ppf s) meets support (ppf t)
assume support (ppf s) meets support (ppf t) ; :: thesis: contradiction
then consider x being object such that
A22: x in support (ppf s) and
A23: x in support (ppf t) by XBOOLE_0:3;
x = r by ;
then r <= k by ;
hence contradiction by NAT_1:13; :: thesis: verum
end;
for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) )
proof
let p be Prime; :: thesis: ( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) )
hereby :: thesis: ( not p in support (ppf m) implies p |-count m <= p |-count n ) end;
assume not p in support (ppf m) ; :: thesis: p |-count m <= p |-count n
hence p |-count m <= p |-count n by Th15; :: thesis: verum
end;
hence ( support (ppf m) c= Seg k & n = m * ((k + 1) |^ e) & ( for p being Prime holds
( ( p in support (ppf m) implies p |-count m = p |-count n ) & ( not p in support (ppf m) implies p |-count m <= p |-count n ) ) ) ) by ; :: thesis: verum
end;
end;