let n be Nat; :: thesis: ( 0 <= n & n < (2 * 3) * 5 implies 14 <= card ((seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) )
assume A1: ( 0 <= n & n < (2 * 3) * 5 ) ; :: thesis: 14 <= card ((seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))
set M2 = multiples 2;
set M3 = multiples 3;
set M5 = multiples 5;
set M23 = (multiples 2) \/ (multiples 3);
set M = ((multiples 2) \/ (multiples 3)) \/ (multiples 5);
set S = seq (n,21);
A2: card ((seq (n,21)) /\ ((multiples 2) \/ (multiples 3))) >= 13

proof

set nm = n mod 6;
set nd = n div 6;
A3: n = ((n div 6) * 6) + (n mod 6) by INT_1:59;
( 2 divides 2 * 3 & 3 divides 2 * 3 ) ;
then A4: ( 2 divides (n div 6) * 6 & 3 divides (n div 6) * 6 ) by INT_2:2;
(multiples 2) \/ (multiples 3) = ((multiples 2) \/ (multiples 3)) \/ (multiples 3) by XBOOLE_1:6
.= (((multiples 2) \/ (multiples 3)) \/ (multiples 3)) \/ (multiples 3) by XBOOLE_1:6
.= ((((multiples 2) \/ (multiples 3)) \/ (multiples 3)) \/ (multiples 3)) \/ (multiples 3) by XBOOLE_1:6 ;
then A5: card ((seq (n,21)) /\ ((multiples 2) \/ (multiples 3))) = card ((seq ((n mod 6),21)) /\ ((multiples 2) \/ (multiples 3))) by A3, A4, Th88;
n mod 6 < 6 by INT_1:58;
hence card ((seq (n,21)) /\ ((multiples 2) \/ (multiples 3))) >= 13 by A5, Lm10; :: thesis: verum

end;

A6: for i being Nat holds
( i in (seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) iff ( n < i & i <= n + 21 & 5 divides i & not 2 divides i & not 3 divides i ) )

proof

let i be Nat; :: thesis: ( i in (seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) iff ( n < i & i <= n + 21 & 5 divides i & not 2 divides i & not 3 divides i ) )

hereby :: thesis: ( n < i & i <= n + 21 & 5 divides i & not 2 divides i & not 3 divides i implies i in (seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) )

assume A7: i in (seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) ; :: thesis: ( n < i & i <= n + 21 & 5 divides i & not 2 divides i & not 3 divides i )
then A8: ( i in seq (n,21) & i in (multiples 5) \ ((multiples 2) \/ (multiples 3)) ) ;
( i in multiples 5 & not i in (multiples 2) \/ (multiples 3) ) by A7, XBOOLE_0:def 5;
then ( not i in multiples 2 & not i in multiples 3 ) by XBOOLE_0:def 3;
hence ( n < i & i <= n + 21 & 5 divides i & not 2 divides i & not 3 divides i ) by A8, NUMBER14:62, Th73; :: thesis: verum

end;

assume ( n < i & i <= n + 21 & 5 divides i & not 2 divides i & not 3 divides i ) ; :: thesis: i in (seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3)))
then A9: ( not i in multiples 2 & not i in multiples 3 & i in multiples 5 & i in seq (n,21) ) by Th73, NUMBER14:62;
then not i in (multiples 2) \/ (multiples 3) by XBOOLE_0:def 3;
then i in (multiples 5) \ ((multiples 2) \/ (multiples 3)) by A9, XBOOLE_0:def 5;
hence i in (seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) by A9, XBOOLE_0:def 4; :: thesis: verum

end;

not (seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) is empty

proof

per cases ( n < 5 or ( 5 <= n & n < 25 ) or n >= 25 ) ;

suppose A10: n < 5 ; :: thesis: not (seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) is empty

A11: ( 5 <= 5 + (n + 16) & 5 + (n + 16) = n + 21 ) by NAT_1:11;
( (2 * 2) + 1 = 5 & (3 * 1) + 2 = 5 ) ;
then ( not 2 divides 5 & not 3 divides 5 ) by NAT_4:9;
hence not (seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) is empty by A10, A11, A6; :: thesis: verum

end;

suppose A12: ( 5 <= n & n < 25 ) ; :: thesis: not (seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) is empty

then A13: 5 + 20 <= n + 21 by XREAL_1:7;
( (2 * 12) + 1 = 25 & (3 * 8) + 1 = 25 ) ;
then ( not 2 divides 25 & not 3 divides 25 & 5 divides 5 * 5 ) by NAT_4:9;
hence not (seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) is empty by A12, A13, A6; :: thesis: verum

end;

suppose n >= 25 ; :: thesis: not (seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) is empty

then A14: 25 + 10 <= n + 21 by XREAL_1:7;
A15: n < 35 by A1, XXREAL_0:2;
( (2 * 17) + 1 = 35 & (3 * 11) + 2 = 35 ) ;
then ( not 2 divides 35 & not 3 divides 35 & 5 divides 7 * 5 ) by NAT_4:9;
hence not (seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) is empty by A14, A15, A6; :: thesis: verum

end;

end;

end;

then A16: card ((seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3)))) >= 1 by NAT_1:14;
((multiples 2) \/ (multiples 3)) \/ (multiples 5) = ((multiples 2) \/ (multiples 3)) \/ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) by XBOOLE_1:39;
then A17: (seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) = ((seq (n,21)) /\ ((multiples 2) \/ (multiples 3))) \/ ((seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3)))) by XBOOLE_1:23;
(seq (n,21)) /\ ((multiples 2) \/ (multiples 3)) misses (seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))) by XBOOLE_1:76, XBOOLE_1:79;
then card ((seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) = (card ((seq (n,21)) /\ ((multiples 2) \/ (multiples 3)))) + (card ((seq (n,21)) /\ ((multiples 5) \ ((multiples 2) \/ (multiples 3))))) by A17, CARD_2:40;
then card ((seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) >= 13 + 1 by A16, A2, XREAL_1:7;
hence 14 <= card ((seq (n,21)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) ; :: thesis: verum