let n, c be Nat; :: thesis: ( 0 <= n & n < 210 & c = card ((seq (n,100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) implies ( c >= 75 & ( not c = 75 or n = 9 or n = 10 or n = 99 or n = 100 ) ) )
assume that
A1: ( 0 <= n & n < 210 ) and
A2: c = card ((seq (n,100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) ; :: thesis: ( c >= 75 & ( not c = 75 or n = 9 or n = 10 or n = 99 or n = 100 ) )
set S = seq (n,100);
set M2 = multiples 2;
set M3 = multiples 3;
set M5 = multiples 5;
set M7 = multiples 7;
set M235 = ((multiples 2) \/ (multiples 3)) \/ (multiples 5);
set M = (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7);
(((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) = (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) by XBOOLE_1:39;
then A3: (seq (n,100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) = ((seq (n,100)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) \/ ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) by XBOOLE_1:23;
A4: (seq (n,100)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) misses (seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) by XBOOLE_1:76, XBOOLE_1:79;
then A5: card ((seq (n,100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) = (card ((seq (n,100)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) + (card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))))) by A3, CARD_2:40;
( not 2 divides (24 * 2) + 1 & not 3 divides (3 * 16) + 1 & not 5 divides (5 * 9) + 4 & 7 divides 7 * 7 ) by NAT_4:9;
then ( not 49 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 49 in multiples 7 ) by Lm6, NUMBER14:62;
then A6: 49 in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) by XBOOLE_0:def 5;
( not 2 divides (38 * 2) + 1 & not 3 divides (3 * 25) + 2 & not 5 divides (5 * 15) + 2 & 7 divides 11 * 7 ) by NAT_4:9;
then ( not 77 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 77 in multiples 7 ) by Lm6, NUMBER14:62;
then A7: 77 in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) by XBOOLE_0:def 5;
( not 2 divides (45 * 2) + 1 & not 3 divides (3 * 30) + 1 & not 5 divides (5 * 18) + 1 & 7 divides 13 * 7 ) by NAT_4:9;
then ( not 91 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 91 in multiples 7 ) by Lm6, NUMBER14:62;
then A8: 91 in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) by XBOOLE_0:def 5;
( not 2 divides (59 * 2) + 1 & not 3 divides (3 * 39) + 2 & not 5 divides (5 * 23) + 4 & 7 divides 17 * 7 ) by NAT_4:9;
then ( not 119 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 119 in multiples 7 ) by Lm6, NUMBER14:62;
then A9: 119 in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) by XBOOLE_0:def 5;
( not 2 divides (66 * 2) + 1 & not 3 divides (3 * 44) + 1 & not 5 divides (5 * 26) + 3 & 7 divides 19 * 7 ) by NAT_4:9;
then ( not 133 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 133 in multiples 7 ) by Lm6, NUMBER14:62;
then A10: 133 in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) by XBOOLE_0:def 5;
( not 2 divides (80 * 2) + 1 & not 3 divides (3 * 53) + 2 & not 5 divides (5 * 32) + 1 & 7 divides 23 * 7 ) by NAT_4:9;
then ( not 161 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 161 in multiples 7 ) by Lm6, NUMBER14:62;
then A11: 161 in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) by XBOOLE_0:def 5;
( not 2 divides (101 * 2) + 1 & not 3 divides (3 * 67) + 2 & not 5 divides (5 * 40) + 3 & 7 divides 29 * 7 ) by NAT_4:9;
then ( not 203 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 203 in multiples 7 ) by Lm6, NUMBER14:62;
then A12: 203 in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) by XBOOLE_0:def 5;
( not 2 divides (108 * 2) + 1 & not 3 divides (3 * 72) + 1 & not 5 divides (5 * 43) + 2 & 7 divides 31 * 7 ) by NAT_4:9;
then ( not 217 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 217 in multiples 7 ) by Lm6, NUMBER14:62;
then A13: 217 in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) by XBOOLE_0:def 5;
( not 2 divides (129 * 2) + 1 & not 3 divides (3 * 86) + 1 & not 5 divides (5 * 51) + 4 & 7 divides 37 * 7 ) by NAT_4:9;
then ( not 259 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 259 in multiples 7 ) by Lm6, NUMBER14:62;
then A14: 259 in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) by XBOOLE_0:def 5;
( not 2 divides (143 * 2) + 1 & not 3 divides (3 * 95) + 2 & not 5 divides (5 * 57) + 2 & 7 divides 41 * 7 ) by NAT_4:9;
then ( not 287 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 287 in multiples 7 ) by Lm6, NUMBER14:62;
then A15: 287 in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) by XBOOLE_0:def 5;
( not 2 divides (150 * 2) + 1 & not 3 divides (3 * 100) + 1 & not 5 divides (5 * 60) + 1 & 7 divides 43 * 7 ) by NAT_4:9;
then ( not 301 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 301 in multiples 7 ) by Lm6, NUMBER14:62;
then A16: 301 in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) by XBOOLE_0:def 5;
A17: for i, j, k being Element of NAT st n < i & i < j & j < k & k <= n + 100 & i in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) & j in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) & k in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) holds
card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3

proof

let i, j, k be Element of NAT ; :: thesis: ( n < i & i < j & j < k & k <= n + 100 & i in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) & j in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) & k in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) implies card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3 )
assume that
A18: ( n < i & i < j & j < k & k <= n + 100 ) and
A19: ( i in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) & j in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) & k in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) ) ; :: thesis: card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3
A20: ( i < k & n < j & j < n + 100 ) by A18, XXREAL_0:2;
then ( i < n + 100 & n < k ) by A18, XXREAL_0:2;
then ( i in seq (n,100) & j in seq (n,100) & k in seq (n,100) ) by A18, A20, Th73;
then ( i in (seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) & j in (seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) & k in (seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) ) by A19, XBOOLE_0:def 4;
then card {i,j,k} <= card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) by NAT_1:43, NOMIN_2:1;
hence card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3 by A18, CARD_2:58; :: thesis: verum

end;

A21: card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3

proof

per cases ( ( 0 <= n & n <= 18 ) or ( 18 < n & n <= 76 ) or ( 76 < n & n <= 118 ) or ( 118 < n & n <= 160 ) or ( 160 < n & n <= 202 ) or ( 202 < n & n < 210 ) ) by A1;

suppose A22: ( 0 <= n & n <= 18 ) ; :: thesis: card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3

100 + 0 <= 100 + n by XREAL_1:6;
then ( n < 49 & 49 < 77 & 77 < 91 & 91 <= n + 100 ) by A22, XXREAL_0:2;
hence card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3 by A6, A7, A8, A17; :: thesis: verum

end;

suppose A23: ( 18 < n & n <= 76 ) ; :: thesis: card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3

then 18 + 1 <= n by NAT_1:13;
then 100 + 19 <= 100 + n by XREAL_1:6;
then ( n < 77 & 77 < 91 & 91 < 119 & 119 <= n + 100 ) by A23, XXREAL_0:2;
hence card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3 by A7, A8, A9, A17; :: thesis: verum

end;

suppose A24: ( 76 < n & n <= 118 ) ; :: thesis: card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3

then 76 + 1 <= n by NAT_1:13;
then 100 + 77 <= 100 + n by XREAL_1:6;
then ( n < 119 & 119 < 133 & 133 < 161 & 161 <= n + 100 ) by A24, XXREAL_0:2;
hence card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3 by A9, A10, A11, A17; :: thesis: verum

end;

suppose A25: ( 118 < n & n <= 160 ) ; :: thesis: card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3

then 118 + 1 <= n by NAT_1:13;
then 100 + 119 <= 100 + n by XREAL_1:6;
then ( n < 161 & 161 < 203 & 203 < 217 & 217 <= n + 100 ) by A25, XXREAL_0:2;
hence card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3 by A11, A12, A13, A17; :: thesis: verum

end;

suppose A26: ( 160 < n & n <= 202 ) ; :: thesis: card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3

then 160 + 1 <= n by NAT_1:13;
then 100 + 161 <= 100 + n by XREAL_1:6;
then ( n < 203 & 203 < 217 & 217 < 259 & 259 <= n + 100 ) by A26, XXREAL_0:2;
hence card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3 by A12, A13, A14, A17; :: thesis: verum

end;

suppose A27: ( 202 < n & n < 210 ) ; :: thesis: card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3

then 202 + 1 <= n by NAT_1:13;
then 100 + 203 <= 100 + n by XREAL_1:6;
then ( n < 259 & 259 < 287 & 287 < 301 & 301 <= n + 100 ) by A27, XXREAL_0:2;
hence card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 3 by A14, A15, A16, A17; :: thesis: verum

end;

end;

end;

A28: card ((seq (n,100)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) >= 72 by Th93;
then card ((seq (n,100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) >= 72 + 3 by A21, A5, XREAL_1:7;
hence c >= 75 by A2; :: thesis: ( not c = 75 or n = 9 or n = 10 or n = 99 or n = 100 )
assume A29: c = 75 ; :: thesis: ( n = 9 or n = 10 or n = 99 or n = 100 )
then 72 + 3 = (card ((seq (n,100)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) + (card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))))) by A2, A4, A3, CARD_2:40;
then card ((seq (n,100)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 72 by A21, XREAL_1:8;
then A30: card ((seq (n,100)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) = 72 by A28, XXREAL_0:1;
then ( n mod 30 = 9 or n mod 30 = 10 ) by Th93;
then consider t being Nat such that
A31: ( ( n = (30 * t) + 9 & 9 < 30 ) or ( n = (30 * t) + 10 & 10 < 30 ) ) by NAT_D:def 2;
A32: for i, j, k, l being Element of NAT st n < i & i < j & j < k & k < l & l <= n + 100 & i in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) & j in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) & k in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) & l in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) holds
card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) > 3

proof

let i, j, k, l be Element of NAT ; :: thesis: ( n < i & i < j & j < k & k < l & l <= n + 100 & i in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) & j in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) & k in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) & l in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) implies card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) > 3 )
assume that
A33: ( n < i & i < j & j < k & k < l & l <= n + 100 ) and
A34: ( i in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) & j in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) & k in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) & l in (multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) ) ; :: thesis: card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) > 3
A35: ( i < k & j < l & n < j & k < n + 100 ) by A33, XXREAL_0:2;
then A36: ( n < k & i < l & j < n + 100 ) by A33, XXREAL_0:2;
( n < l & i < n + 100 ) by A35, XXREAL_0:2;
then ( i in seq (n,100) & j in seq (n,100) & k in seq (n,100) & l in seq (n,100) ) by A33, A35, A36, Th73;
then ( i in (seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) & j in (seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) & k in (seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) & l in (seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) ) by A34, XBOOLE_0:def 4;
then card {i,j,k,l} <= card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) by QUATERNI:5, NAT_1:43;
then ( card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) >= 4 & 4 = 3 + 1 ) by A33, A35, CARD_2:59;
hence card ((seq (n,100)) /\ ((multiples 7) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) > 3 by NAT_1:13; :: thesis: verum

end;

t < 6 + 1

proof

assume t >= 6 + 1 ; :: thesis: contradiction
then 30 * t >= 7 * 30 by XREAL_1:64;
then ( (30 * t) + 9 > (7 * 30) + 0 & (30 * t) + 10 > (7 * 30) + 0 ) by XREAL_1:8;
hence contradiction by A1, A31; :: thesis: verum

end;

then t <= 6 by NAT_1:13;
then not not t = 0 & ... & not t = 6 ;

per cases then ( t = 0 or t = 3 or t = 1 or t = 2 or t = 4 or t = 5 or t = 6 ) ;

suppose ( t = 0 or t = 3 ) ; :: thesis: ( n = 9 or n = 10 or n = 99 or n = 100 )

hence ( n = 9 or n = 10 or n = 99 or n = 100 ) by A31; :: thesis: verum

end;

suppose ( t = 1 or t = 2 ) ; :: thesis: ( n = 9 or n = 10 or n = 99 or n = 100 )

hence ( n = 9 or n = 10 or n = 99 or n = 100 ) by A29, A2, A5, A30, A31, A32, A7, A8, A9, A10; :: thesis: verum

end;

suppose t = 4 ; :: thesis: ( n = 9 or n = 10 or n = 99 or n = 100 )

hence ( n = 9 or n = 10 or n = 99 or n = 100 ) by A29, A2, A31, A5, A30, A32, A10, A11, A12, A13; :: thesis: verum

end;

suppose t = 5 ; :: thesis: ( n = 9 or n = 10 or n = 99 or n = 100 )

hence ( n = 9 or n = 10 or n = 99 or n = 100 ) by A29, A2, A5, A30, A31, A32, A14, A11, A12, A13; :: thesis: verum

end;

suppose t = 6 ; :: thesis: ( n = 9 or n = 10 or n = 99 or n = 100 )

hence ( n = 9 or n = 10 or n = 99 or n = 100 ) by A29, A2, A5, A30, A31, A32, A14, A15, A12, A13; :: thesis: verum

end;

end;