let n, c be Nat; :: thesis: ( c = card ((seq (n,100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) implies ( c >= 75 & ( not c = 75 or n mod 210 = 9 or n mod 210 = 10 or n mod 210 = 99 or n mod 210 = 100 ) ) )
set M2 = multiples 2;
set M3 = multiples 3;
set M5 = multiples 5;
set M7 = multiples 7;
set M = (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7);
assume A1: c = card ((seq (n,100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) ; :: thesis: ( c >= 75 & ( not c = 75 or n mod 210 = 9 or n mod 210 = 10 or n mod 210 = 99 or n mod 210 = 100 ) )
set nm = n mod 210;
set nd = n div 210;
A2: n = ((n div 210) * 210) + (n mod 210) by INT_1:59;
( 2 divides 2 * ((3 * 5) * 7) & 3 divides 3 * ((2 * 5) * 7) & 5 divides 5 * ((2 * 3) * 7) & 7 divides 7 * ((2 * 3) * 5) ) ;
then A3: ( 2 divides (n div 210) * 210 & 3 divides (n div 210) * 210 & 5 divides (n div 210) * 210 & 7 divides (n div 210) * 210 ) by INT_2:2;
(((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) = ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 7) by XBOOLE_1:6;
then A4: c = card ((seq ((n mod 210),100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) by A1, A2, A3, Th88;
n mod 210 < 210 by INT_1:58;
hence ( c >= 75 & ( not c = 75 or n mod 210 = 9 or n mod 210 = 10 or n mod 210 = 99 or n mod 210 = 100 ) ) by Lm8, A4; :: thesis: verum