let n be Nat; :: thesis: ( 11 <= n implies card (primeNumbers (n,100)) <= 24 )
assume A1: 11 <= n ; :: thesis: card (primeNumbers (n,100)) <= 24
set M2 = multiples 2;
set M3 = multiples 3;
set M5 = multiples 5;
set M7 = multiples 7;
set M11 = multiples 11;
set M2357 = (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7);
set M = ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11);
set S = seq (n,100);
A2: primeNumbers (n,100) misses (seq (n,100)) /\ (((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11))

proof

assume primeNumbers (n,100) meets (seq (n,100)) /\ (((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11)) ; :: thesis: contradiction
then consider x being object such that
A3: ( x in primeNumbers (n,100) & x in (seq (n,100)) /\ (((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11)) ) by XBOOLE_0:3;
reconsider x = x as Nat by A3;
A4: ( x is prime & n < x ) by A3, Th74;
( x in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) or x in multiples 11 ) by A3, XBOOLE_0:def 3;
then ( 2 divides x or 3 divides x or 5 divides x or 7 divides x or 11 divides x ) by Lm9, NUMBER14:62;
then ( x = 2 or x = 3 or x = 5 or x = 7 or x = 11 ) by A4;
hence contradiction by A3, Th74, A1, XXREAL_0:2; :: thesis: verum

end;

primeNumbers (n,100) = (seq (n,100)) /\ SetPrimes by NUMBER14:def 17;
then ( card ((primeNumbers (n,100)) \/ ((seq (n,100)) /\ (((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11)))) <= card (seq (n,100)) & card (seq (n,100)) = 100 ) by NAT_1:43, NUMBER14:73, XBOOLE_1:8;
then A5: (card (primeNumbers (n,100))) + (card ((seq (n,100)) /\ (((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11)))) <= 100 by A2, CARD_2:40;
set nm = n mod 2310;
set nd = n div 2310;
A6: n = ((n div 2310) * 2310) + (n mod 2310) by INT_1:59;
( 2 divides 2 * (((3 * 5) * 7) * 11) & 3 divides 3 * (((2 * 5) * 7) * 11) & 5 divides 5 * (((2 * 3) * 7) * 11) & 7 divides 7 * (((2 * 3) * 5) * 11) & 11 divides 11 * (((2 * 3) * 5) * 7) ) ;
then A7: ( 2 divides (n div 2310) * 2310 & 3 divides (n div 2310) * 2310 & 5 divides (n div 2310) * 2310 & 7 divides (n div 2310) * 2310 & 11 divides (n div 2310) * 2310 ) by INT_2:2;
A8: card ((seq (n,100)) /\ (((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11))) = card ((seq ((n mod 2310),100)) /\ (((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11))) by A6, A7, Th88;
n mod 2310 < 2310 by INT_1:58;
then card ((seq (n,100)) /\ (((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11))) >= 76 by A8, Th95;
then ((card (primeNumbers (n,100))) + (card ((seq (n,100)) /\ (((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11))))) - (card ((seq (n,100)) /\ (((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11)))) <= 100 - 76 by A5, XREAL_1:13;
hence card (primeNumbers (n,100)) <= 24 ; :: thesis: verum