let n be Nat; :: thesis: ( 0 <= n & n < (((2 * 3) * 5) * 7) * 11 implies 76 <= card ((seq (n,100)) /\ (((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11))) )
assume A1: ( 0 <= n & n < (((2 * 3) * 5) * 7) * 11 ) ; :: thesis: 76 <= card ((seq (n,100)) /\ (((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11)))
set S = seq (n,100);
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);
assume A2: card ((seq (n,100)) /\ (((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11))) < 76 ; :: thesis: contradiction
((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11) = ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ ((multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) by XBOOLE_1:39;
then A3: (seq (n,100)) /\ (((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11)) = ((seq (n,100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) \/ ((seq (n,100)) /\ ((multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)))) by XBOOLE_1:23;
(seq (n,100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) misses (seq (n,100)) /\ ((multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) by XBOOLE_1:76, XBOOLE_1:79;
then A4: 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)))) + (card ((seq (n,100)) /\ ((multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))))) by A3, CARD_2:40;
card ((seq (n,100)) /\ (((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) \/ (multiples 11))) < 75 + 1 by A2;
then A5: ( (card ((seq (n,100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)))) + 0 <= 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))) <= 75 ) by NAT_1:13, A4, XREAL_1:7;
then A6: card ((seq (n,100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) <= 75 by XXREAL_0:2;
card ((seq (n,100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) >= 75 by Th94;
then A7: card ((seq (n,100)) /\ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) = 75 by A6, XXREAL_0:1;
then ( n mod 210 = 9 or n mod 210 = 10 or n mod 210 = 99 or n mod 210 = 100 ) by Th94;
then consider t being Nat such that
A8: ( ( n = (210 * t) + 9 & 9 < 210 ) or ( n = (210 * t) + 10 & 10 < 210 ) or ( n = (210 * t) + 99 & 99 < 210 ) or ( n = (210 * t) + 100 & 100 < 210 ) ) by NAT_D:def 2;
A9: (seq (n,100)) /\ ((multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7))) = {} by XREAL_1:8, A4, A5, A7;
A10: t < 10 + 1

proof

assume t >= 10 + 1 ; :: thesis: contradiction
then 210 * t >= 11 * 210 by XREAL_1:64;
then ( (210 * t) + 9 > (11 * 210) + 0 & (210 * t) + 10 > (11 * 210) + 0 & (210 * t) + 99 > (11 * 210) + 0 & (210 * t) + 100 > (11 * 210) + 0 ) by XREAL_1:8;
hence contradiction by A1, A8; :: thesis: verum

end;

A11: for i, k being Nat st i + 1 < k & k <= i + 100 & k in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) holds
( i <> n & i + 1 <> n )

proof

let i, k be Nat; :: thesis: ( i + 1 < k & k <= i + 100 & k in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) implies ( i <> n & i + 1 <> n ) )
assume A12: ( i + 1 < k & k <= i + 100 & k in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) ) ; :: thesis: ( i <> n & i + 1 <> n )
( i < k & k < (i + 100) + 1 & (i + 100) + 1 = (i + 1) + 100 ) by A12, NAT_1:13;
then ( k in seq (i,100) & k in seq ((i + 1),100) ) by A12, Th73;
hence ( i <> n & i + 1 <> n ) by A9, A12, XBOOLE_0:def 4; :: thesis: verum

end;

t <= 10 by A10, NAT_1:13;
then not not t = 0 & ... & not t = 10 ;

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

suppose A13: t = 0 ; :: thesis: contradiction

( not 2 divides (5 * 2) + 1 & not 3 divides (3 * 3) + 2 & not 5 divides (2 * 5) + 1 & not 7 divides (1 * 7) + 4 & 11 divides 11 * 1 ) by NAT_4:9;
then ( not 11 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 11 in multiples 11 ) by Lm9, NUMBER14:62;
then A14: 11 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( not 2 divides (60 * 2) + 1 & not 3 divides (40 * 3) + 1 & not 5 divides (24 * 5) + 1 & not 7 divides (17 * 7) + 2 & 11 divides 11 * 11 ) by NAT_4:9;
then ( not 121 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 121 in multiples 11 ) by Lm9, NUMBER14:62;
then A15: 121 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( 9 + 1 < 11 & 11 <= 9 + 100 & 99 + 1 < 121 & 121 <= 99 + 100 ) ;
hence contradiction by A13, A8, A11, A14, A15; :: thesis: verum

end;

suppose A16: t = 1 ; :: thesis: contradiction

( not 2 divides (159 * 2) + 1 & not 3 divides (106 * 3) + 1 & not 5 divides (63 * 5) + 4 & not 7 divides (45 * 7) + 4 & 11 divides 11 * 29 ) by NAT_4:9;
then ( not 319 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 319 in multiples 11 ) by Lm9, NUMBER14:62;
then A17: 319 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( 219 + 1 < 253 & 253 <= 219 + 100 & 309 + 1 < 319 & 319 <= 309 + 100 ) ;
hence contradiction by A16, A8, A11, A17; :: thesis: verum

end;

suppose A18: t = 2 ; :: thesis: contradiction

( not 2 divides (225 * 2) + 1 & not 3 divides (150 * 3) + 1 & not 5 divides (90 * 5) + 1 & not 7 divides (64 * 7) + 3 & 11 divides 11 * 41 ) by NAT_4:9;
then ( not 451 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 451 in multiples 11 ) by Lm9, NUMBER14:62;
then A19: 451 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( not 2 divides (291 * 2) + 1 & not 3 divides (194 * 3) + 1 & not 5 divides (116 * 5) + 3 & not 7 divides (83 * 7) + 2 & 11 divides 11 * 53 ) by NAT_4:9;
then ( not 583 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 583 in multiples 11 ) by Lm9, NUMBER14:62;
then A20: 583 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( 429 + 1 < 451 & 451 <= 429 + 100 & 519 + 1 < 583 & 583 <= 519 + 100 ) ;
hence contradiction by A18, A8, A11, A19, A20; :: thesis: verum

end;

suppose A21: t = 3 ; :: thesis: contradiction

( not 2 divides (368 * 2) + 1 & not 3 divides (245 * 3) + 2 & not 5 divides (147 * 5) + 2 & not 7 divides (105 * 7) + 2 & 11 divides 11 * 67 ) by NAT_4:9;
then ( not 737 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 737 in multiples 11 ) by Lm9, NUMBER14:62;
then A22: 737 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( 639 + 1 < 649 & 649 <= 639 + 100 & 729 + 1 < 737 & 737 <= 729 + 100 ) ;
hence contradiction by A21, A8, A11, A22; :: thesis: verum

end;

suppose A23: t = 4 ; :: thesis: contradiction

( not 2 divides (434 * 2) + 1 & not 3 divides (289 * 3) + 2 & not 5 divides (173 * 5) + 4 & not 7 divides (124 * 7) + 1 & 11 divides 11 * 79 ) by NAT_4:9;
then ( not 869 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 869 in multiples 11 ) by Lm9, NUMBER14:62;
then A24: 869 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( not 2 divides (489 * 2) + 1 & not 3 divides (326 * 3) + 1 & not 5 divides (195 * 5) + 4 & not 7 divides (139 * 7) + 6 & 11 divides 11 * 89 ) by NAT_4:9;
then ( not 979 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 979 in multiples 11 ) by Lm9, NUMBER14:62;
then A25: 979 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( 849 + 1 < 869 & 869 <= 849 + 100 & 939 + 1 < 979 & 979 <= 939 + 100 ) ;
hence contradiction by A23, A8, A11, A24, A25; :: thesis: verum

end;

suppose A26: t = 5 ; :: thesis: contradiction

( not 2 divides (533 * 2) + 1 & not 3 divides (355 * 3) + 2 & not 5 divides (213 * 5) + 2 & not 7 divides (152 * 7) + 3 & 11 divides 11 * 97 ) by NAT_4:9;
then ( not 1067 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 1067 in multiples 11 ) by Lm9, NUMBER14:62;
then A27: 1067 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( not 2 divides (588 * 2) + 1 & not 3 divides (392 * 3) + 1 & not 5 divides (235 * 5) + 2 & not 7 divides (168 * 7) + 1 & 11 divides 11 * 107 ) by NAT_4:9;
then ( not 1177 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 1177 in multiples 11 ) by Lm9, NUMBER14:62;
then A28: 1177 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( 1059 + 1 < 1067 & 1067 <= 1059 + 100 & 1149 + 1 < 1177 & 1177 <= 1149 + 100 ) ;
hence contradiction by A26, A8, A11, A27, A28; :: thesis: verum

end;

suppose A29: t = 6 ; :: thesis: contradiction

( not 2 divides (665 * 2) + 1 & not 3 divides (443 * 3) + 2 & not 5 divides (266 * 5) + 1 & not 7 divides (190 * 7) + 1 & 11 divides 11 * 121 ) by NAT_4:9;
then ( not 1331 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 1331 in multiples 11 ) by Lm9, NUMBER14:62;
then A30: 1331 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( not 2 divides (698 * 2) + 1 & not 3 divides (465 * 3) + 2 & not 5 divides (279 * 5) + 2 & not 7 divides (199 * 7) + 4 & 11 divides 11 * 127 ) by NAT_4:9;
then ( not 1397 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 1397 in multiples 11 ) by Lm9, NUMBER14:62;
then A31: 1397 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( 1269 + 1 < 1331 & 1331 <= 1269 + 100 & 1359 + 1 < 1397 & 1397 <= 1359 + 100 ) ;
hence contradiction by A29, A8, A11, A30, A31; :: thesis: verum

end;

suppose A32: t = 7 ; :: thesis: contradiction

( not 2 divides (786 * 2) + 1 & not 3 divides (524 * 3) + 1 & not 5 divides (314 * 5) + 3 & not 7 divides (224 * 7) + 5 & 11 divides 11 * 143 ) by NAT_4:9;
then ( not 1573 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 1573 in multiples 11 ) by Lm9, NUMBER14:62;
then A33: 1573 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( 1479 + 1 < 1507 & 1507 <= 1479 + 100 & 1569 + 1 < 1573 & 1573 <= 1569 + 100 ) ;
hence contradiction by A32, A8, A11, A33; :: thesis: verum

end;

suppose A34: t = 8 ; :: thesis: contradiction

( not 2 divides (863 * 2) + 1 & not 3 divides (575 * 3) + 2 & not 5 divides (345 * 5) + 2 & not 7 divides (246 * 7) + 5 & 11 divides 11 * 157 ) by NAT_4:9;
then ( not 1727 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 1727 in multiples 11 ) by Lm9, NUMBER14:62;
then A35: 1727 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( not 2 divides (896 * 2) + 1 & not 3 divides (597 * 3) + 2 & not 5 divides (358 * 5) + 3 & not 7 divides (256 * 7) + 1 & 11 divides 11 * 163 ) by NAT_4:9;
then ( not 1793 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 1793 in multiples 11 ) by Lm9, NUMBER14:62;
then A36: 1793 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( 1689 + 1 < 1727 & 1727 <= 1689 + 100 & 1779 + 1 < 1793 & 1793 <= 1779 + 100 ) ;
hence contradiction by A34, A8, A11, A35, A36; :: thesis: verum

end;

suppose A37: t = 9 ; :: thesis: contradiction

( not 2 divides (995 * 2) + 1 & not 3 divides (663 * 3) + 2 & not 5 divides (398 * 5) + 1 & not 7 divides (284 * 7) + 3 & 11 divides 11 * 181 ) by NAT_4:9;
then ( not 1991 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 1991 in multiples 11 ) by Lm9, NUMBER14:62;
then A38: 1991 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( 1899 + 1 < 1903 & 1903 <= 1899 + 100 & 1989 + 1 < 1991 & 1991 <= 1989 + 100 ) ;
hence contradiction by A37, A8, A11, A38; :: thesis: verum

end;

suppose A39: t = 10 ; :: thesis: contradiction

( not 2 divides (1061 * 2) + 1 & not 3 divides (707 * 3) + 2 & not 5 divides (424 * 5) + 3 & not 7 divides (303 * 7) + 2 & 11 divides 11 * 193 ) by NAT_4:9;
then ( not 2123 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 2123 in multiples 11 ) by Lm9, NUMBER14:62;
then A40: 2123 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( not 2 divides (1149 * 2) + 1 & not 3 divides (766 * 3) + 1 & not 5 divides (459 * 5) + 4 & not 7 divides (328 * 7) + 3 & 11 divides 11 * 209 ) by NAT_4:9;
then ( not 2299 in (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7) & 2299 in multiples 11 ) by Lm9, NUMBER14:62;
then A41: 2299 in (multiples 11) \ ((((multiples 2) \/ (multiples 3)) \/ (multiples 5)) \/ (multiples 7)) by XBOOLE_0:def 5;
( 2109 + 1 < 2123 & 2123 <= 2109 + 100 & 2199 + 1 < 2299 & 2299 <= 2199 + 100 ) ;
hence contradiction by A39, A8, A11, A40, A41; :: thesis: verum

end;

end;