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

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 or j = 37 or j = 38 or j = 39 or j = 40 or j = 41 or j = 42 or j = 43 or j = 44 or j = 45 ) ;

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)) = 10 by A2, Th280;
hence contradiction by A1; :: thesis: verum

end;

suppose j = 2 ; :: thesis: contradiction

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

end;

suppose j = 3 ; :: thesis: contradiction

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

end;

suppose j = 4 ; :: thesis: contradiction

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

end;

suppose j = 5 ; :: thesis: contradiction

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

end;

suppose j = 6 ; :: thesis: contradiction

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

end;

suppose j = 7 ; :: thesis: contradiction

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

end;

suppose j = 8 ; :: thesis: contradiction

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

end;

suppose j = 9 ; :: thesis: contradiction

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

end;

suppose j = 10 ; :: thesis: contradiction

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

end;

suppose j = 11 ; :: thesis: contradiction

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

end;

suppose j = 12 ; :: thesis: contradiction

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

end;

suppose j = 13 ; :: thesis: contradiction

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

end;

suppose j = 14 ; :: thesis: contradiction

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

end;

suppose j = 15 ; :: thesis: contradiction

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

end;

suppose j = 16 ; :: thesis: contradiction

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

end;

suppose j = 17 ; :: thesis: contradiction

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

end;

suppose j = 18 ; :: thesis: contradiction

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

end;

suppose j = 19 ; :: thesis: contradiction

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

end;

suppose j = 20 ; :: thesis: contradiction

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

end;

suppose j = 21 ; :: thesis: contradiction

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

end;

suppose j = 22 ; :: thesis: contradiction

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

end;

suppose j = 23 ; :: thesis: contradiction

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

end;

suppose j = 24 ; :: thesis: contradiction

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

end;

suppose j = 25 ; :: thesis: contradiction

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

end;

suppose j = 26 ; :: thesis: contradiction

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

end;

suppose j = 27 ; :: thesis: contradiction

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

end;

suppose j = 28 ; :: thesis: contradiction

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

end;

suppose j = 29 ; :: thesis: contradiction

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

end;

suppose j = 30 ; :: thesis: contradiction

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

end;

suppose j = 31 ; :: thesis: contradiction

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

end;

suppose j = 32 ; :: thesis: contradiction

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

end;

suppose j = 33 ; :: thesis: contradiction

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

end;

suppose j = 34 ; :: thesis: contradiction

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

end;

suppose j = 35 ; :: thesis: contradiction

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

end;

suppose j = 36 ; :: thesis: contradiction

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

end;

suppose j = 37 ; :: thesis: contradiction

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

end;

suppose j = 38 ; :: thesis: contradiction

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

end;

suppose j = 39 ; :: thesis: contradiction

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

end;

suppose j = 40 ; :: thesis: contradiction

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

end;

suppose j = 41 ; :: thesis: contradiction

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

end;

suppose j = 42 ; :: thesis: contradiction

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

end;

suppose j = 43 ; :: thesis: contradiction

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

end;

suppose j = 44 ; :: thesis: contradiction

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

end;

suppose j = 45 ; :: thesis: contradiction

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

end;

end;