let n be Element of NAT ; :: thesis:
assume A1: ( 1 <= n & n < 4001 ) ; :: thesis:
A2: for a, n, p being Element of NAT st a <= n & p <= 2 * a holds
p <= 2 * n

proof

let a, n, p be Element of NAT ; :: thesis:
assume A3: ( a <= n & p <= 2 * a ) ; :: thesis:
then 2 * a <= 2 * n by XREAL_1:66;
hence p <= 2 * n by A3, XXREAL_0:2; :: thesis:

end;

per cases by A1;

suppose A4: ( 1 <= n & n < 2 ) ; :: thesis:

2 <= 2 * 1 ;
then ( n < 2 & 2 <= 2 * n ) by A2, A4;
hence ex p being Prime st
( n < p & p <= 2 * n ) by INT_2:44; :: thesis:

end;

suppose A5: ( 2 <= n & n < 3 ) ; :: thesis:

3 <= 2 * 2 ;
then ( n < 3 & 3 <= 2 * n ) by A2, A5;
hence ex p being Prime st
( n < p & p <= 2 * n ) by PEPIN:44; :: thesis:

end;

suppose A6: ( 3 <= n & n < 5 ) ; :: thesis:

5 <= 2 * 3 ;
then ( n < 5 & 5 <= 2 * n ) by A2, A6;
hence ex p being Prime st
( n < p & p <= 2 * n ) by PEPIN:64; :: thesis:

end;

suppose A7: ( 5 <= n & n < 7 ) ; :: thesis:

7 <= 2 * 5 ;
then ( n < 7 & 7 <= 2 * n ) by A2, A7;
hence ex p being Prime st
( n < p & p <= 2 * n ) by Th26; :: thesis:

end;

suppose A8: ( 7 <= n & n < 13 ) ; :: thesis:

13 <= 2 * 7 ;
then ( n < 13 & 13 <= 2 * n ) by A2, A8;
hence ex p being Prime st
( n < p & p <= 2 * n ) by Th28; :: thesis:

end;

suppose A9: ( 13 <= n & n < 23 ) ; :: thesis:

23 <= 2 * 13 ;
then ( n < 23 & 23 <= 2 * n ) by A2, A9;
hence ex p being Prime st
( n < p & p <= 2 * n ) by Th30; :: thesis:

end;

suppose A10: ( 23 <= n & n < 43 ) ; :: thesis:

43 <= 2 * 23 ;
then ( n < 43 & 43 <= 2 * n ) by A2, A10;
hence ex p being Prime st
( n < p & p <= 2 * n ) by Th32; :: thesis:

end;

suppose A11: ( 43 <= n & n < 83 ) ; :: thesis:

83 <= 2 * 43 ;
then ( n < 83 & 83 <= 2 * n ) by A2, A11;
hence ex p being Prime st
( n < p & p <= 2 * n ) by Th33; :: thesis:

end;

suppose A12: ( 83 <= n & n < 163 ) ; :: thesis:

163 <= 2 * 83 ;
then ( n < 163 & 163 <= 2 * n ) by A2, A12;
hence ex p being Prime st
( n < p & p <= 2 * n ) by Th35; :: thesis:

end;

suppose A13: ( 163 <= n & n < 317 ) ; :: thesis:

317 <= 2 * 163 ;
then ( n < 317 & 317 <= 2 * n ) by A2, A13;
hence ex p being Prime st
( n < p & p <= 2 * n ) by Th36; :: thesis:

end;

suppose A14: ( 317 <= n & n < 631 ) ; :: thesis:

631 <= 2 * 317 ;
then ( n < 631 & 631 <= 2 * n ) by A2, A14;
hence ex p being Prime st
( n < p & p <= 2 * n ) by Th37; :: thesis:

end;

suppose A15: ( 631 <= n & n < 1259 ) ; :: thesis:

1259 <= 2 * 631 ;
then ( n < 1259 & 1259 <= 2 * n ) by A2, A15;
hence ex p being Prime st
( n < p & p <= 2 * n ) by Th38; :: thesis:

end;

suppose A16: ( 1259 <= n & n < 2503 ) ; :: thesis:

2503 <= 2 * 1259 ;
then ( n < 2503 & 2503 <= 2 * n ) by A2, A16;
hence ex p being Prime st
( n < p & p <= 2 * n ) by Th39; :: thesis:

end;

suppose A17: ( 2503 <= n & n < 4001 ) ; :: thesis:

4001 <= 2 * 2503 ;
then ( n < 4001 & 4001 <= 2 * n ) by A2, A17;
hence ex p being Prime st
( n < p & p <= 2 * n ) by Th40; :: thesis:

end;

end;