let k, m be Nat; :: thesis: for p being Prime st p <= k holds
(multiples p) /\ (seq (k,m)) misses primeNumbers (k,m)
let p be Prime; :: thesis: ( p <= k implies (multiples p) /\ (seq (k,m)) misses primeNumbers (k,m) )
set A = primeNumbers (k,m);
set D = (multiples p) /\ (seq (k,m));
assume A1: p <= k ; :: thesis: (multiples p) /\ (seq (k,m)) misses primeNumbers (k,m)
assume (multiples p) /\ (seq (k,m)) meets primeNumbers (k,m) ; :: thesis: contradiction
then consider x being object such that
A2: x in (multiples p) /\ (seq (k,m)) and
A3: x in primeNumbers (k,m) by XBOOLE_0:3;
A4: x is Multiple of p by A2, Th61;
x in seq (k,m) by A2;
then consider n being Element of NAT such that
A5: x = n and
A6: k + 1 <= n and
n <= k + m ;
A7: p + 1 <= k + 1 by A1, XREAL_1:6;
n is prime by A3, A5, NEWTON:def 6;
then ( p = 1 or p = n ) by A4, A5, Def15;
then p + 1 <= p + 0 by A6, A7, XXREAL_0:2, INT_2:def 4;
hence contradiction by XREAL_1:6; :: thesis: verum