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