let n be non zero Nat; :: thesis: primenumber (1 + (primeindex (LP<=6n+1 n))) >= (6 * n) + 5
set M = LP<=6n+1 n;
set N = 1 + (primeindex (LP<=6n+1 n));
assume primenumber (1 + (primeindex (LP<=6n+1 n))) < (6 * n) + 5 ; :: thesis: contradiction
then A1: primenumber (1 + (primeindex (LP<=6n+1 n))) < ((6 * n) + 4) + 1 ;
A2: n >= 0 + 1 by NAT_1:13;
then A3: 3 * n >= 3 * 1 by XREAL_1:66;
then (3 * n) + 1 >= 3 + 1 by XREAL_1:6;
then A4: (6 * n) + 2 <> 2 ;
2 divides 2 * ((3 * n) + 1) ;
then A5: not (6 * n) + 2 is prime by A4;
2 * n >= 2 * 1 by A2, XREAL_1:66;
then (2 * n) + 1 >= 2 + 1 by XREAL_1:6;
then A6: (6 * n) + 3 <> 3 ;
3 divides 3 * ((2 * n) + 1) ;
then A7: not (6 * n) + 3 is prime by A6;
(3 * n) + 2 >= 3 + 2 by A3, XREAL_1:6;
then 2 * ((3 * n) + 2) >= 2 * 5 by XREAL_1:64;
then A8: (6 * n) + 4 <> 2 ;
2 divides 2 * ((3 * n) + 2) ;
then A9: not (6 * n) + 4 is prime by A8;
A10: primenumber (1 + (primeindex (LP<=6n+1 n))) in SetPrimes by NEWTON:def 6;
primenumber (1 + (primeindex (LP<=6n+1 n))) <= ((6 * n) + 3) + 1 by A1, NAT_1:13;
then primenumber (1 + (primeindex (LP<=6n+1 n))) < ((6 * n) + 3) + 1 by A9, XXREAL_0:1;
then primenumber (1 + (primeindex (LP<=6n+1 n))) <= (6 * n) + 3 by NAT_1:13;
then primenumber (1 + (primeindex (LP<=6n+1 n))) < ((6 * n) + 2) + 1 by A7, XXREAL_0:1;
then primenumber (1 + (primeindex (LP<=6n+1 n))) <= ((6 * n) + 1) + 1 by NAT_1:13;
then primenumber (1 + (primeindex (LP<=6n+1 n))) < ((6 * n) + 1) + 1 by A5, XXREAL_0:1;
then primenumber (1 + (primeindex (LP<=6n+1 n))) <= (6 * n) + 1 by NAT_1:13;
then primenumber (1 + (primeindex (LP<=6n+1 n))) in <=6n+1 n ;
then primenumber (1 + (primeindex (LP<=6n+1 n))) in (<=6n+1 n) /\ SetPrimes by A10, XBOOLE_0:def 4;
then primenumber (1 + (primeindex (LP<=6n+1 n))) <= LP<=6n+1 n by XXREAL_2:def 8;
hence contradiction by Th28; :: thesis: verum