let n, c be Nat; :: thesis: ( 0 <= n & n < 30 & c = card ((seq (n,100)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) implies ( c >= 72 & ( not c = 72 or n = 9 or n = 10 ) ) )
assume that
A1: ( 0 <= n & n < 30 ) and
A2: c = card ((seq (n,100)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) ; :: thesis: ( c >= 72 & ( not c = 72 or n = 9 or n = 10 ) )
set M2 = multiples 2;
set M3 = multiples 3;
set M23 = (multiples 2) \/ (multiples 3);
set M5 = multiples 5;
set M = ((multiples 2) \/ (multiples 3)) \/ (multiples 5);
A3: (seq (n,10)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) misses (seq ((n + 10),(30 * 3))) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) by Th75, XBOOLE_1:76;
seq (n,(10 + (30 * 3))) = (seq (n,10)) \/ (seq ((n + 10),(30 * 3))) by Th77;
then (seq (n,(10 + (30 * 3)))) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) = ((seq (n,10)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) \/ ((seq ((n + 10),(30 * 3))) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) by XBOOLE_1:23;
then A4: card ((seq (n,(10 + (30 * 3)))) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) = (card ((seq (n,10)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) + (card ((seq ((n + 10),(30 * 3))) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) by A3, CARD_2:40;
A5: card ((seq ((n + 10),(30 * 3))) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) = 66

proof

( 30 = (2 * 3) * 5 & (2 * 3) * 5 = 2 * (3 * 5) & 2 * (3 * 5) = 3 * (2 * 5) ) ;
then A6: ( 2 divides 30 & 3 divides 30 & 5 divides 30 ) ;
((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 card ((seq ((n + 10),(30 * 3))) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) = 3 * (card ((seq (0,30)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) by A6, Th90
.= 3 * 22 by Th92 ;
hence card ((seq ((n + 10),(30 * 3))) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) = 66 ; :: thesis: verum

end;

A7: 2 divides 2 * 2 ;
A8: 2 divides 2 * 3 ;
A9: 2 divides 2 * 4 ;
A10: 2 divides 2 * 5 ;
A11: 2 divides 2 * 6 ;
A12: 2 divides 2 * 7 ;
A13: 2 divides 2 * 8 ;
A14: 2 divides 2 * 9 ;
A15: 2 divides 2 * 10 ;
A16: 2 divides 2 * 11 ;
A17: 2 divides 2 * 12 ;
A18: 2 divides 2 * 13 ;
A19: 2 divides 2 * 14 ;
A20: 2 divides 2 * 15 ;
A21: 2 divides 2 * 16 ;
A22: 2 divides 2 * 17 ;
A23: 2 divides 2 * 18 ;
A24: 2 divides 2 * 19 ;
A25: 3 divides 3 * 3 ;
A26: 3 divides 3 * 5 ;
A27: 3 divides 3 * 7 ;
A28: 3 divides 3 * 9 ;
A29: 3 divides 3 * 11 ;
A30: 3 divides 3 * 13 ;
A31: 5 divides 5 * 5 ;
A32: 5 divides 5 * 7 ;
A33: ( 10 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 12 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 14 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 15 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 16 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 18 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & 20 in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) ) by Lm6, A10, A11, A12, A26, A13, A14, A15;
A34: (seq (9,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) c= {11,13,17,19}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (seq (9,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) or y in {11,13,17,19} )
assume A35: y in (seq (9,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) ; :: thesis: y in {11,13,17,19}
reconsider y = y as Nat by A35;
( 10 = 9 + 1 & 9 + 1 <= y & y <= 9 + 10 ) by CALCUL_2:1, A35;
then not not y = 10 + 0 & ... & not y = 10 + 9 by NAT_1:62;
hence y in {11,13,17,19} by A33, A35, XBOOLE_0:def 5, ENUMSET1:def 2; :: thesis: verum

end;

A36: (seq (10,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) c= {11,13,17,19}

proof

let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in (seq (10,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) or y in {11,13,17,19} )
assume A37: y in (seq (10,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) ; :: thesis: y in {11,13,17,19}
reconsider y = y as Nat by A37;
( 11 = 10 + 1 & 10 + 1 <= y & y <= 10 + 10 & 10 + 10 = 11 + 9 ) by A37, CALCUL_2:1;
then not not y = 11 + 0 & ... & not y = 11 + 9 by NAT_1:62;
hence y in {11,13,17,19} by A33, A37, XBOOLE_0:def 5, ENUMSET1:def 2; :: thesis: verum

end;

( card ((seq (9,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= card {11,13,17,19} & card {11,13,17,19} <= 4 & card ((seq (10,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= card {11,13,17,19} ) by A34, A36, NAT_1:43, CARD_2:52;
then A38: ( card ((seq (9,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 4 & card ((seq (10,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 4 ) by XXREAL_0:2;
A39: for x, y, z being Element of NAT
for i, j being Nat st ( for k being Nat st not not (i + 1) + 0 = k & ... & not (i + 1) + (j + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = x & not k = y holds
k = z ) holds
for w being Nat st i <= w & w <= i + j holds
card ((seq (w,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3

proof

let x, y, z be Element of NAT ; :: thesis: for i, j being Nat st ( for k being Nat st not not (i + 1) + 0 = k & ... & not (i + 1) + (j + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = x & not k = y holds
k = z ) holds
for w being Nat st i <= w & w <= i + j holds
card ((seq (w,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3
let i, j be Nat; :: thesis: ( ( for k being Nat st not not (i + 1) + 0 = k & ... & not (i + 1) + (j + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = x & not k = y holds
k = z ) implies for w being Nat st i <= w & w <= i + j holds
card ((seq (w,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3 )
assume A40: for k being Nat st not not (i + 1) + 0 = k & ... & not (i + 1) + (j + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = x & not k = y holds
k = z ; :: thesis: for w being Nat st i <= w & w <= i + j holds
card ((seq (w,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3
let w be Nat; :: thesis: ( i <= w & w <= i + j implies card ((seq (w,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3 )
assume A41: ( i <= w & w <= i + j ) ; :: thesis: card ((seq (w,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3
(seq (w,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) c= {x,y,z}

proof

let a be object ; :: according to TARSKI:def 3 :: thesis: ( not a in (seq (w,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) or a in {x,y,z} )
assume A42: a in (seq (w,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)) ; :: thesis: a in {x,y,z}
reconsider a = a as Nat by A42;
A43: ( a in seq (w,10) & not a in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) ) by A42, XBOOLE_0:def 5;
( w < a & a <= w + 10 & w + 10 <= (i + j) + 10 ) by A41, Th73, A42, XREAL_1:6;
then ( i < a & a <= (i + j) + 10 ) by A41, XXREAL_0:2;
then ( (i + 1) + 0 = i + 1 & i + 1 <= a & a <= (i + j) + 10 & (i + j) + 10 = (i + 1) + (j + 9) ) by NAT_1:13;
then not not (i + 1) + 0 = a & ... & not (i + 1) + (j + 9) = a by NAT_1:62;
then ( a = x or a = y or a = z ) by A40, A43;
hence a in {x,y,z} by ENUMSET1:def 1; :: thesis: verum

end;

then ( card ((seq (w,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= card {x,y,z} & card {x,y,z} <= 3 ) by NAT_1:43, CARD_2:51;
hence card ((seq (w,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3 by XXREAL_0:2; :: thesis: verum

end;

A44: ( n <> 9 & n <> 10 implies card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3 )

proof

assume A45: ( n <> 9 & n <> 10 ) ; :: thesis: card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3

per cases ( ( 0 <= n & n <= 2 + 0 & 2 + 0 = 2 ) or ( 2 < n & n <= 6 ) or ( 6 < n & n <= 8 ) or ( 8 < n & n <= 10 ) or ( 10 < n & n <= 12 ) or ( 12 < n & n <= 18 ) or ( 18 < n & n <= 26 ) or ( 26 < n & n < 30 & 30 = 29 + 1 ) ) by A1;

suppose A46: ( 0 <= n & n <= 2 + 0 & 2 + 0 = 2 ) ; :: thesis: card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3

for k being Nat st not not (0 + 1) + 0 = k & ... & not (0 + 1) + (2 + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = 1 + 0 & not k = 1 + 6 holds
k = 1 + 10

proof

let k be Nat; :: thesis: ( not not (0 + 1) + 0 = k & ... & not (0 + 1) + (2 + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = 1 + 0 & not k = 1 + 6 implies k = 1 + 10 )
assume that
A47: not not (0 + 1) + 0 = k & ... & not (0 + 1) + (2 + 9) = k and
A48: not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) ; :: thesis: ( k = 1 + 0 or k = 1 + 6 or k = 1 + 10 )
not not 1 + 0 = k & ... & not 1 + 11 = k by A47;
hence ( k = 1 + 0 or k = 1 + 6 or k = 1 + 10 ) by A48, A7, A8, A9, A10, A11, A25, Lm6; :: thesis: verum

end;

hence card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3 by A46, A39; :: thesis: verum

end;

suppose ( 2 < n & n <= 6 ) ; :: thesis: card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3

then A49: ( 3 = 2 + 1 & 2 + 1 <= n & n <= 3 + 3 ) by NAT_1:13;
for k being Nat st not not (3 + 1) + 0 = k & ... & not (3 + 1) + (3 + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = 4 + 3 & not k = 4 + 7 holds
k = 4 + 9

proof

let k be Nat; :: thesis: ( not not (3 + 1) + 0 = k & ... & not (3 + 1) + (3 + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = 4 + 3 & not k = 4 + 7 implies k = 4 + 9 )
assume that
A50: not not (3 + 1) + 0 = k & ... & not (3 + 1) + (3 + 9) = k and
A51: not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) ; :: thesis: ( k = 4 + 3 or k = 4 + 7 or k = 4 + 9 )
not not 4 + 0 = k & ... & not 4 + 12 = k by A50;
hence ( k = 4 + 3 or k = 4 + 7 or k = 4 + 9 ) by A51, A7, A8, A9, A10, A11, A12, A13, A25, A26, Lm6; :: thesis: verum

end;

hence card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3 by A49, A39; :: thesis: verum

end;

suppose ( 6 < n & n <= 8 ) ; :: thesis: card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3

then A52: ( 7 = 6 + 1 & 6 + 1 <= n & n <= 7 + 1 ) by NAT_1:13;
for k being Nat st not not (7 + 1) + 0 = k & ... & not (7 + 1) + (1 + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = 8 + 3 & not k = 8 + 5 holds
k = 8 + 9

proof

let k be Nat; :: thesis: ( not not (7 + 1) + 0 = k & ... & not (7 + 1) + (1 + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = 8 + 3 & not k = 8 + 5 implies k = 8 + 9 )
assume that
A53: not not (7 + 1) + 0 = k & ... & not (7 + 1) + (1 + 9) = k and
A54: not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) ; :: thesis: ( k = 8 + 3 or k = 8 + 5 or k = 8 + 9 )
not not 8 + 0 = k & ... & not 8 + 10 = k by A53;
hence ( k = 8 + 3 or k = 8 + 5 or k = 8 + 9 ) by A54, A9, A10, A11, A12, A13, A14, A25, A26, Lm6; :: thesis: verum

end;

hence card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3 by A52, A39; :: thesis: verum

end;

suppose ( 8 < n & n <= 10 ) ; :: thesis: card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3

then ( 9 = 8 + 1 & 8 + 1 <= n & n <= 9 + 1 ) by NAT_1:13;
hence card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3 by A45, NAT_1:9; :: thesis: verum

end;

suppose ( 10 < n & n <= 12 ) ; :: thesis: card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3

then A55: ( 11 = 10 + 1 & 10 + 1 <= n & n <= 11 + 1 ) by NAT_1:13;
for k being Nat st not not (11 + 1) + 0 = k & ... & not (11 + 1) + (1 + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = 12 + 1 & not k = 12 + 5 holds
k = 12 + 7

proof

let k be Nat; :: thesis: ( not not (11 + 1) + 0 = k & ... & not (11 + 1) + (1 + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = 12 + 1 & not k = 12 + 5 implies k = 12 + 7 )
assume that
A56: not not (11 + 1) + 0 = k & ... & not (11 + 1) + (1 + 9) = k and
A57: not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) ; :: thesis: ( k = 12 + 1 or k = 12 + 5 or k = 12 + 7 )
not not 12 + 0 = k & ... & not 12 + 10 = k by A56;

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

suppose ( 12 + 0 = k or 12 + 1 = k ) ; :: thesis: ( k = 12 + 1 or k = 12 + 5 or k = 12 + 7 )

hence ( k = 12 + 1 or k = 12 + 5 or k = 12 + 7 ) by A57, A11, Lm6; :: thesis: verum

end;

suppose ( 12 + 2 = k or 12 + 3 = k ) ; :: thesis: ( k = 12 + 1 or k = 12 + 5 or k = 12 + 7 )

hence ( k = 12 + 1 or k = 12 + 5 or k = 12 + 7 ) by A57, A12, A26, Lm6; :: thesis: verum

end;

suppose ( 12 + 4 = k or 12 + 5 = k ) ; :: thesis: ( k = 12 + 1 or k = 12 + 5 or k = 12 + 7 )

hence ( k = 12 + 1 or k = 12 + 5 or k = 12 + 7 ) by A57, A13, Lm6; :: thesis: verum

end;

suppose ( 12 + 6 = k or 12 + 7 = k ) ; :: thesis: ( k = 12 + 1 or k = 12 + 5 or k = 12 + 7 )

hence ( k = 12 + 1 or k = 12 + 5 or k = 12 + 7 ) by A57, A14, Lm6; :: thesis: verum

end;

suppose ( 12 + 8 = k or 12 + 9 = k or 12 + 10 = k ) ; :: thesis: ( k = 12 + 1 or k = 12 + 5 or k = 12 + 7 )

hence ( k = 12 + 1 or k = 12 + 5 or k = 12 + 7 ) by A57, A15, A16, A27, Lm6; :: thesis: verum

end;

end;

end;

hence card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3 by A55, A39; :: thesis: verum

end;

suppose ( 12 < n & n <= 18 ) ; :: thesis: card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3

then A58: ( 13 = 12 + 1 & 12 + 1 <= n & n <= 13 + 5 ) by NAT_1:13;
for k being Nat st not not (13 + 1) + 0 = k & ... & not (13 + 1) + (5 + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = 14 + 3 & not k = 14 + 5 holds
k = 14 + 9

proof

let k be Nat; :: thesis: ( not not (13 + 1) + 0 = k & ... & not (13 + 1) + (5 + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = 14 + 3 & not k = 14 + 5 implies k = 14 + 9 )
assume that
A59: not not (13 + 1) + 0 = k & ... & not (13 + 1) + (5 + 9) = k and
A60: not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) ; :: thesis: ( k = 14 + 3 or k = 14 + 5 or k = 14 + 9 )
not not 14 + 0 = k & ... & not 14 + 14 = k by A59;
hence ( k = 14 + 3 or k = 14 + 5 or k = 14 + 9 ) by A60, A12, A13, A14, A15, A16, A17, A18, A19, A26, A27, A28, A31, Lm6; :: thesis: verum

end;

hence card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3 by A58, A39; :: thesis: verum

end;

suppose ( 18 < n & n <= 26 ) ; :: thesis: card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3

then A61: ( 19 = 18 + 1 & 18 + 1 <= n & n <= 19 + 7 ) by NAT_1:13;
for k being Nat st not not (19 + 1) + 0 = k & ... & not (19 + 1) + (7 + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = 20 + 3 & not k = 20 + 9 holds
k = 20 + 11

proof

let k be Nat; :: thesis: ( not not (19 + 1) + 0 = k & ... & not (19 + 1) + (7 + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = 20 + 3 & not k = 20 + 9 implies k = 20 + 11 )
assume that
A62: not not (19 + 1) + 0 = k & ... & not (19 + 1) + (7 + 9) = k and
A63: not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) ; :: thesis: ( k = 20 + 3 or k = 20 + 9 or k = 20 + 11 )
not not 20 + 0 = k & ... & not 20 + 16 = k by A62;

per cases then ( 20 + 0 = k or 20 + 1 = k or 20 + 2 = k or 20 + 3 = k or 20 + 4 = k or 20 + 5 = k or 20 + 6 = k or 20 + 7 = k or 20 + 8 = k or 20 + 9 = k or 20 + 10 = k or 20 + 11 = k or 20 + 12 = k or 20 + 13 = k or 20 + 14 = k or 20 + 15 = k or 20 + 16 = k ) ;

suppose ( 20 + 0 = k or 20 + 1 = k or 20 + 2 = k or 20 + 3 = k ) ; :: thesis: ( k = 20 + 3 or k = 20 + 9 or k = 20 + 11 )

hence ( k = 20 + 3 or k = 20 + 9 or k = 20 + 11 ) by A63, A15, A16, A27, Lm6; :: thesis: verum

end;

suppose ( 20 + 4 = k or 20 + 5 = k or 20 + 6 = k or 20 + 7 = k ) ; :: thesis: ( k = 20 + 3 or k = 20 + 9 or k = 20 + 11 )

hence ( k = 20 + 3 or k = 20 + 9 or k = 20 + 11 ) by A63, A17, A31, A18, A28, Lm6; :: thesis: verum

end;

suppose ( 20 + 8 = k or 20 + 9 = k or 20 + 10 = k or 20 + 11 = k ) ; :: thesis: ( k = 20 + 3 or k = 20 + 9 or k = 20 + 11 )

hence ( k = 20 + 3 or k = 20 + 9 or k = 20 + 11 ) by A63, A19, A20, Lm6; :: thesis: verum

end;

suppose ( 20 + 12 = k or 20 + 13 = k or 20 + 14 = k or 20 + 15 = k or 20 + 16 = k ) ; :: thesis: ( k = 20 + 3 or k = 20 + 9 or k = 20 + 11 )

hence ( k = 20 + 3 or k = 20 + 9 or k = 20 + 11 ) by A63, A21, A29, A22, A32, A23, Lm6; :: thesis: verum

end;

end;

end;

hence card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3 by A61, A39; :: thesis: verum

end;

suppose ( 26 < n & n < 30 & 30 = 29 + 1 ) ; :: thesis: card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3

then A64: ( 27 = 26 + 1 & 26 + 1 <= n & n <= 27 + 2 ) by NAT_1:13;
for k being Nat st not not (27 + 1) + 0 = k & ... & not (27 + 1) + (2 + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = 27 + 2 & not k = 27 + 4 holds
k = 27 + 10

proof

let k be Nat; :: thesis: ( not not (27 + 1) + 0 = k & ... & not (27 + 1) + (2 + 9) = k & not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) & not k = 27 + 2 & not k = 27 + 4 implies k = 27 + 10 )
assume that
A65: not not (27 + 1) + 0 = k & ... & not (27 + 1) + (2 + 9) = k and
A66: not k in ((multiples 2) \/ (multiples 3)) \/ (multiples 5) ; :: thesis: ( k = 27 + 2 or k = 27 + 4 or k = 27 + 10 )
not not 28 + 0 = k & ... & not 28 + 11 = k by A65;

per cases then ( k = 28 + 0 or k = 28 + 1 or k = 28 + 2 or k = 28 + 3 or k = 28 + 4 or k = 28 + 5 or k = 28 + 6 or k = 28 + 7 or k = 28 + 8 or k = 28 + 9 or k = 28 + 10 or k = 28 + 11 ) ;

suppose ( k = 28 + 0 or k = 28 + 1 ) ; :: thesis: ( k = 27 + 2 or k = 27 + 4 or k = 27 + 10 )

hence ( k = 27 + 2 or k = 27 + 4 or k = 27 + 10 ) by A66, A19, Lm6; :: thesis: verum

end;

suppose ( k = 28 + 2 or k = 28 + 3 ) ; :: thesis: ( k = 27 + 2 or k = 27 + 4 or k = 27 + 10 )

hence ( k = 27 + 2 or k = 27 + 4 or k = 27 + 10 ) by A66, A20, Lm6; :: thesis: verum

end;

suppose ( k = 28 + 4 or k = 28 + 5 ) ; :: thesis: ( k = 27 + 2 or k = 27 + 4 or k = 27 + 10 )

hence ( k = 27 + 2 or k = 27 + 4 or k = 27 + 10 ) by A66, A21, A29, Lm6; :: thesis: verum

end;

suppose ( k = 28 + 6 or k = 28 + 7 ) ; :: thesis: ( k = 27 + 2 or k = 27 + 4 or k = 27 + 10 )

hence ( k = 27 + 2 or k = 27 + 4 or k = 27 + 10 ) by A66, A22, A32, Lm6; :: thesis: verum

end;

suppose ( k = 28 + 8 or k = 28 + 9 ) ; :: thesis: ( k = 27 + 2 or k = 27 + 4 or k = 27 + 10 )

hence ( k = 27 + 2 or k = 27 + 4 or k = 27 + 10 ) by A66, A23, Lm6; :: thesis: verum

end;

suppose ( k = 28 + 10 or k = 28 + 11 ) ; :: thesis: ( k = 27 + 2 or k = 27 + 4 or k = 27 + 10 )

hence ( k = 27 + 2 or k = 27 + 4 or k = 27 + 10 ) by A66, A24, A30, Lm6; :: thesis: verum

end;

end;

end;

hence card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) <= 3 by A64, A39; :: thesis: verum

end;

end;

end;

A67: card (seq (n,10)) = 10 by NUMBER14:73;
seq (n,10) = ((seq (n,10)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) \/ ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) ;
then 10 = (card ((seq (n,10)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) + (card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) by A67, XBOOLE_1:89, CARD_2:40;
then A68: card ((seq (n,10)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) = 10 - (card ((seq (n,10)) \ (((multiples 2) \/ (multiples 3)) \/ (multiples 5)))) ;
A69: ( n <> 9 & n <> 10 implies c > 72 )

proof

assume ( n <> 9 & n <> 10 ) ; :: thesis: c > 72
then card ((seq (n,10)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) >= 10 - 3 by A44, A68, XREAL_1:10;
then ( card ((seq (n,(10 + (30 * 3)))) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) >= 66 + 7 & 66 + 7 = 72 + 1 ) by A4, A5, XREAL_1:6;
hence c > 72 by A2, NAT_1:13; :: thesis: verum

end;

( ( n = 9 or n = 10 ) implies c >= 72 )

proof

assume ( n = 9 or n = 10 ) ; :: thesis: c >= 72
then card ((seq (n,10)) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) >= 10 - 4 by A38, A68, XREAL_1:10;
then ( card ((seq (n,(10 + (30 * 3)))) /\ (((multiples 2) \/ (multiples 3)) \/ (multiples 5))) >= 66 + 6 & 66 + 6 = 72 ) by A4, A5, XREAL_1:6;
hence c >= 72 by A2; :: thesis: verum

end;

hence ( c >= 72 & ( not c = 72 or n = 9 or n = 10 ) ) by A69; :: thesis: verum