let n be non zero Nat; :: thesis: ex k being Element of NAT st support (ppf n) c= Seg k

A1: support (ppf n) = support (pfexp n) by NAT_3:def 9;

A1: support (ppf n) = support (pfexp n) by NAT_3:def 9;

per cases
( support (ppf n) is empty or not support (ppf n) is empty )
;

end;

suppose A2:
support (ppf n) is empty
; :: thesis: ex k being Element of NAT st support (ppf n) c= Seg k

end;

end;

suppose
not support (ppf n) is empty
; :: thesis: ex k being Element of NAT st support (ppf n) c= Seg k

then reconsider S = support (ppf n) as non empty finite Subset of NAT by XBOOLE_1:1;

take max S ; :: thesis: ( max S is set & max S is Element of NAT & support (ppf n) c= Seg (max S) )

A3: max S is Element of NAT by ORDINAL1:def 12;

support (ppf n) c= Seg (max S)

end;take max S ; :: thesis: ( max S is set & max S is Element of NAT & support (ppf n) c= Seg (max S) )

A3: max S is Element of NAT by ORDINAL1:def 12;

support (ppf n) c= Seg (max S)

proof

hence
( max S is set & max S is Element of NAT & support (ppf n) c= Seg (max S) )
by A3; :: thesis: verum
let x be object ; :: according to TARSKI:def 3 :: thesis: ( not x in support (ppf n) or x in Seg (max S) )

assume A4: x in support (ppf n) ; :: thesis: x in Seg (max S)

then reconsider m = x as Nat ;

x is Prime by A1, A4, NAT_3:34;

then A5: 1 <= m by INT_2:def 4;

m <= max S by A4, XXREAL_2:def 8;

hence x in Seg (max S) by A5, FINSEQ_1:1; :: thesis: verum

end;assume A4: x in support (ppf n) ; :: thesis: x in Seg (max S)

then reconsider m = x as Nat ;

x is Prime by A1, A4, NAT_3:34;

then A5: 1 <= m by INT_2:def 4;

m <= max S by A4, XXREAL_2:def 8;

hence x in Seg (max S) by A5, FINSEQ_1:1; :: thesis: verum