let n be Nat; :: thesis: ( 2 <= n implies ex k being non zero Nat st
( Product (primesFinS k) <= n & n < Product (primesFinS (k + 1)) ) )
assume A1: 2 <= n ; :: thesis: ex k being non zero Nat st
( Product (primesFinS k) <= n & n < Product (primesFinS (k + 1)) )
defpred S₁[ Nat] means n < Product (primesFinS ($1 + 1));
consider k being Nat such that
A2: ( 2 to_power k <= n & n < 2 to_power (k + 1) ) by A1, BINARI_6:2;
2 |^ (k + 1) <= Product (primesFinS (k + 1)) by Th26;
then n < Product (primesFinS (k + 1)) by A2, XXREAL_0:2;
then S₁[k] ;
then A3: ex k being Nat st S₁[k] ;
consider m being Nat such that
A4: S₁[m] and
A5: for w being Nat st S₁[w] holds
m <= w from NAT_1:sch 5(A3);
m <> 0 by A1, A4, NUMBER13:9;
then reconsider m = m as non zero Nat ;
take m ; :: thesis: ( Product (primesFinS m) <= n & n < Product (primesFinS (m + 1)) )
reconsider m1 = m - 1 as Nat ;
Product (primesFinS m) <= n

proof

assume n < Product (primesFinS m) ; :: thesis: contradiction
then S₁[m1] ;
then ( m1 + 1 = m & m <= m1 ) by A5;
hence contradiction by NAT_1:13; :: thesis: verum

end;

hence ( Product (primesFinS m) <= n & n < Product (primesFinS (m + 1)) ) by A4; :: thesis: verum