theorem Th94: :: NUMBER19:94

for n, c being Nat st c = card ((seq (n,100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) holds
( 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 ) )