let n be Element of NAT ; :: thesis: ( 1 <= n & n < 4001 implies ex p being Prime st
( n < p & p <= 2 * n ) )
A1: 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: ( a <= n & p <= 2 * a implies p <= 2 * n )
assume that
A2: a <= n and
A3: p <= 2 * a ; :: thesis: p <= 2 * n
2 * a <= 2 * n by A2, XREAL_1:64;
hence p <= 2 * n by A3, XXREAL_0:2; :: thesis: verum
end;
assume A4: ( 1 <= n & n < 4001 ) ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )
per cases ( ( 1 <= n & n < 2 ) or ( 2 <= n & n < 3 ) or ( 3 <= n & n < 5 ) or ( 5 <= n & n < 7 ) or ( 7 <= n & n < 13 ) or ( 13 <= n & n < 23 ) or ( 23 <= n & n < 43 ) or ( 43 <= n & n < 83 ) or ( 83 <= n & n < 163 ) or ( 163 <= n & n < 317 ) or ( 317 <= n & n < 631 ) or ( 631 <= n & n < 1259 ) or ( 1259 <= n & n < 2503 ) or ( 2503 <= n & n < 4001 ) ) by A4;
suppose A5: ( 1 <= n & n < 2 ) ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )
2 <= 2 * 1 ;
then 2 <= 2 * n by A1, A5;
hence ex p being Prime st
( n < p & p <= 2 * n ) by A5, INT_2:28; :: thesis: verum
end;
suppose A6: ( 2 <= n & n < 3 ) ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )
3 <= 2 * 2 ;
then 3 <= 2 * n by A1, A6;
hence ex p being Prime st
( n < p & p <= 2 * n ) by A6, PEPIN:41; :: thesis: verum
end;
suppose A7: ( 3 <= n & n < 5 ) ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )
5 <= 2 * 3 ;
then 5 <= 2 * n by A1, A7;
hence ex p being Prime st
( n < p & p <= 2 * n ) by A7, PEPIN:59; :: thesis: verum
end;
suppose A8: ( 5 <= n & n < 7 ) ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )
7 <= 2 * 5 ;
then 7 <= 2 * n by A1, A8;
hence ex p being Prime st
( n < p & p <= 2 * n ) by A8, Th26; :: thesis: verum
end;
suppose A9: ( 7 <= n & n < 13 ) ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )
13 <= 2 * 7 ;
then 13 <= 2 * n by A1, A9;
hence ex p being Prime st
( n < p & p <= 2 * n ) by A9, Th28; :: thesis: verum
end;
suppose A10: ( 13 <= n & n < 23 ) ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )
23 <= 2 * 13 ;
then 23 <= 2 * n by A1, A10;
hence ex p being Prime st
( n < p & p <= 2 * n ) by A10, Th30; :: thesis: verum
end;
suppose A11: ( 23 <= n & n < 43 ) ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )
43 <= 2 * 23 ;
then 43 <= 2 * n by A1, A11;
hence ex p being Prime st
( n < p & p <= 2 * n ) by A11, Th32; :: thesis: verum
end;
suppose A12: ( 43 <= n & n < 83 ) ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )
83 <= 2 * 43 ;
then 83 <= 2 * n by A1, A12;
hence ex p being Prime st
( n < p & p <= 2 * n ) by A12, Th33; :: thesis: verum
end;
suppose A13: ( 83 <= n & n < 163 ) ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )
163 <= 2 * 83 ;
then 163 <= 2 * n by A1, A13;
hence ex p being Prime st
( n < p & p <= 2 * n ) by A13, Th35; :: thesis: verum
end;
suppose A14: ( 163 <= n & n < 317 ) ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )
317 <= 2 * 163 ;
then 317 <= 2 * n by A1, A14;
hence ex p being Prime st
( n < p & p <= 2 * n ) by A14, Th36; :: thesis: verum
end;
suppose A15: ( 317 <= n & n < 631 ) ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )
631 <= 2 * 317 ;
then 631 <= 2 * n by A1, A15;
hence ex p being Prime st
( n < p & p <= 2 * n ) by A15, Th37; :: thesis: verum
end;
suppose A16: ( 631 <= n & n < 1259 ) ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )
1259 <= 2 * 631 ;
then 1259 <= 2 * n by A1, A16;
hence ex p being Prime st
( n < p & p <= 2 * n ) by A16, Th38; :: thesis: verum
end;
suppose A17: ( 1259 <= n & n < 2503 ) ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )
2503 <= 2 * 1259 ;
then 2503 <= 2 * n by A1, A17;
hence ex p being Prime st
( n < p & p <= 2 * n ) by A17, Th39; :: thesis: verum
end;
suppose A18: ( 2503 <= n & n < 4001 ) ; :: thesis: ex p being Prime st
( n < p & p <= 2 * n )
4001 <= 2 * 2503 ;
then 4001 <= 2 * n by A1, A18;
hence ex p being Prime st
( n < p & p <= 2 * n ) by A18, Th40; :: thesis: verum
end;
end;