thus Sum (digits (888,10)) = 24 by Th1073; :: according to NUMBER11:def 1 :: thesis: ( 24 divides 888 & ( for m being Nat st Sum (digits (m,10)) = 24 & 24 divides m holds
888 <= m ) )
888 = 37 * 24 ;
hence 24 divides 888 by INT_1:def 3; :: thesis: for m being Nat st Sum (digits (m,10)) = 24 & 24 divides m holds
888 <= m
let m be Nat; :: thesis: ( Sum (digits (m,10)) = 24 & 24 divides m implies 888 <= m )
assume A1: ( Sum (digits (m,10)) = 24 & 24 divides m ) ; :: thesis: 888 <= m
then consider j being Nat such that
A2: m = 24 * j by NAT_D:def 3;
assume m < 888 ; :: thesis: contradiction
then 24 * j < 24 * 37 by A2;
then j < 36 + 1 by XREAL_1:64;
then j <= 36 by NAT_1:9;
then not not j = 0 & ... & not j = 36 ;

per cases then ( j = 0 or j = 1 or j = 2 or j = 3 or j = 4 or j = 5 or j = 6 or j = 7 or j = 8 or j = 9 or j = 10 or j = 11 or j = 12 or j = 13 or j = 14 or j = 15 or j = 16 or j = 17 or j = 18 or j = 19 or j = 20 or j = 21 or j = 22 or j = 23 or j = 24 or j = 25 or j = 26 or j = 27 or j = 28 or j = 29 or j = 30 or j = 31 or j = 32 or j = 33 or j = 34 or j = 35 or j = 36 ) ;

suppose j = 0 ; :: thesis: contradiction

then Sum (digits (m,10)) = 0 by A2, Th6;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 1 ; :: thesis: contradiction

then Sum (digits (m,10)) = 6 by A2, Th95;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 2 ; :: thesis: contradiction

then Sum (digits (m,10)) = 12 by A2, Th99;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 3 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th273;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 4 ; :: thesis: contradiction

then Sum (digits (m,10)) = 15 by A2, Th185;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 5 ; :: thesis: contradiction

then Sum (digits (m,10)) = 3 by A2, Th39;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 6 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th189;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 7 ; :: thesis: contradiction

then Sum (digits (m,10)) = 15 by A2, Th153;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 8 ; :: thesis: contradiction

then Sum (digits (m,10)) = 12 by A2, Th191;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 9 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th1049;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 10 ; :: thesis: contradiction

then Sum (digits (m,10)) = 6 by A2, Th193;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 11 ; :: thesis: contradiction

then Sum (digits (m,10)) = 12 by A2, Th751;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 12 ; :: thesis: contradiction

then Sum (digits (m,10)) = 18 by A2, Th199;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 13 ; :: thesis: contradiction

then Sum (digits (m,10)) = 6 by A2, Th1051;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 14 ; :: thesis: contradiction

then Sum (digits (m,10)) = 12 by A2, Th205;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 15 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th371;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 16 ; :: thesis: contradiction

then Sum (digits (m,10)) = 15 by A2, Th211;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 17 ; :: thesis: contradiction

then Sum (digits (m,10)) = 12 by A2, Th258;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 18 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th217;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 19 ; :: thesis: contradiction

then Sum (digits (m,10)) = 15 by A2, Th314;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 20 ; :: thesis: contradiction

then Sum (digits (m,10)) = 12 by A2, Th379;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 21 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th1053;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 22 ; :: thesis: contradiction

then Sum (digits (m,10)) = 15 by A2, Th767;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 23 ; :: thesis: contradiction

then Sum (digits (m,10)) = 12 by A2, Th958;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 24 ; :: thesis: contradiction

then Sum (digits (m,10)) = 18 by A2, Th1055;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 25 ; :: thesis: contradiction

then Sum (digits (m,10)) = 6 by A2, Th391;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 26 ; :: thesis: contradiction

then Sum (digits (m,10)) = 12 by A2, Th1057;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 27 ; :: thesis: contradiction

then Sum (digits (m,10)) = 18 by A2, Th1059;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 28 ; :: thesis: contradiction

then Sum (digits (m,10)) = 15 by A2, Th1061;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 29 ; :: thesis: contradiction

then Sum (digits (m,10)) = 21 by A2, Th1063;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 30 ; :: thesis: contradiction

then Sum (digits (m,10)) = 9 by A2, Th403;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 31 ; :: thesis: contradiction

then Sum (digits (m,10)) = 15 by A2, Th1065;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 32 ; :: thesis: contradiction

then Sum (digits (m,10)) = 21 by A2, Th1067;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 33 ; :: thesis: contradiction

then Sum (digits (m,10)) = 18 by A2, Th789;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 34 ; :: thesis: contradiction

then Sum (digits (m,10)) = 15 by A2, Th1069;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 35 ; :: thesis: contradiction

then Sum (digits (m,10)) = 12 by A2, Th413;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 36 ; :: thesis: contradiction

then Sum (digits (m,10)) = 18 by A2, Th1071;
hence contradiction by A1; :: thesis: verum

end;

end;