let k be Nat; :: thesis: ( 3 <= k implies (primenumber k) + (primenumber (k + 1)) <= Product (primesFinS k) )
assume A1: 3 <= k ; :: thesis: (primenumber k) + (primenumber (k + 1)) <= Product (primesFinS k)
set P = Product (primesFinS k);
Product (primesFinS k) >= ((primenumber 0) * (primenumber 1)) * (primenumber 2) by A1, Lm12;
then Product (primesFinS k) > 6 by XXREAL_0:2, MOEBIUS2:8, MOEBIUS2:10, MOEBIUS2:12;
then consider a, b being Nat such that
A2: a > 1 and
A3: b > 1 and
A4: Product (primesFinS k) = a + b and
A5: a,b are_coprime by NUMBER05:22;
consider p, q being Prime such that
A6: p divides a and
A7: not p divides b and
A8: q divides b and
A9: not q divides a and
A10: p <> q by A2, A3, A5, Th8;
( p <= a & q <= b ) by A2, A3, A6, A8, NAT_D:7;
then A11: p + q <= a + b by XREAL_1:7;

per cases ( p < q or q < p ) by A10, XXREAL_0:1;

suppose A12: p < q ; :: thesis: (primenumber k) + (primenumber (k + 1)) <= Product (primesFinS k)

A13: not p divides Product (primesFinS k)

proof

assume p divides Product (primesFinS k) ; :: thesis: contradiction
then p divides (a + b) - a by A4, A6, INT_5:1;
hence contradiction by A7; :: thesis: verum

end;

now :: thesis: p, Product (primesFinS k) are_coprime

assume not p, Product (primesFinS k) are_coprime ; :: thesis: contradiction
then consider z being Prime such that
A14: z divides p and
A15: z divides Product (primesFinS k) by PYTHTRIP:def 2;
( z = 1 or z = p ) by A14, INT_2:def 4;
hence contradiction by A13, A15, INT_2:def 4; :: thesis: verum

end;

then A16: primenumber k <= p by Th16;

per cases then ( primenumber k < p or primenumber k = p ) by XXREAL_0:1;

suppose primenumber k < p ; :: thesis: (primenumber k) + (primenumber (k + 1)) <= Product (primesFinS k)

then primenumber (k + 1) <= p by PRIMRECI:12;
then primenumber (k + 1) < q by A12, XXREAL_0:2;
then (primenumber k) + (primenumber (k + 1)) <= p + q by A16, XREAL_1:7;
hence (primenumber k) + (primenumber (k + 1)) <= Product (primesFinS k) by A4, A11, XXREAL_0:2; :: thesis: verum

end;

suppose primenumber k = p ; :: thesis: (primenumber k) + (primenumber (k + 1)) <= Product (primesFinS k)

then primenumber (k + 1) <= q by A12, PRIMRECI:12;
then (primenumber k) + (primenumber (k + 1)) <= p + q by A16, XREAL_1:7;
hence (primenumber k) + (primenumber (k + 1)) <= Product (primesFinS k) by A4, A11, XXREAL_0:2; :: thesis: verum

end;

end;

end;

suppose A17: q < p ; :: thesis: (primenumber k) + (primenumber (k + 1)) <= Product (primesFinS k)

A18: not q divides Product (primesFinS k)

proof

assume q divides Product (primesFinS k) ; :: thesis: contradiction
then q divides (a + b) - b by A4, A8, INT_5:1;
hence contradiction by A9; :: thesis: verum

end;

now :: thesis: q, Product (primesFinS k) are_coprime

assume not q, Product (primesFinS k) are_coprime ; :: thesis: contradiction
then consider z being Prime such that
A19: z divides q and
A20: z divides Product (primesFinS k) by PYTHTRIP:def 2;
( z = 1 or z = q ) by A19, INT_2:def 4;
hence contradiction by A18, A20, INT_2:def 4; :: thesis: verum

end;

then A21: primenumber k <= q by Th16;

per cases then ( primenumber k < q or primenumber k = q ) by XXREAL_0:1;

suppose primenumber k < q ; :: thesis: (primenumber k) + (primenumber (k + 1)) <= Product (primesFinS k)

then primenumber (k + 1) <= q by PRIMRECI:12;
then primenumber (k + 1) < p by A17, XXREAL_0:2;
then (primenumber k) + (primenumber (k + 1)) <= p + q by A21, XREAL_1:7;
hence (primenumber k) + (primenumber (k + 1)) <= Product (primesFinS k) by A4, A11, XXREAL_0:2; :: thesis: verum

end;

suppose primenumber k = q ; :: thesis: (primenumber k) + (primenumber (k + 1)) <= Product (primesFinS k)

then primenumber (k + 1) <= p by A17, PRIMRECI:12;
then (primenumber k) + (primenumber (k + 1)) <= p + q by A21, XREAL_1:7;
hence (primenumber k) + (primenumber (k + 1)) <= Product (primesFinS k) by A4, A11, XXREAL_0:2; :: thesis: verum

end;

end;

end;

end;