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

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 or j = 46 or j = 47 or j = 48 or j = 49 or j = 50 or j = 51 or j = 52 or j = 53 or j = 54 or j = 55 or j = 56 or j = 57 or j = 58 or j = 59 or j = 60 or j = 61 or j = 62 or j = 63 or j = 64 or j = 65 or j = 66 or j = 67 or j = 68 or j = 69 or j = 70 or j = 71 or j = 72 ) ;

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

end;

suppose j = 2 ; :: thesis: contradiction

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

end;

suppose j = 3 ; :: thesis: contradiction

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

end;

suppose j = 4 ; :: thesis: contradiction

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

end;

suppose j = 5 ; :: thesis: contradiction

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

end;

suppose j = 6 ; :: thesis: contradiction

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

end;

suppose j = 7 ; :: thesis: contradiction

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

end;

suppose j = 8 ; :: thesis: contradiction

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

end;

suppose j = 9 ; :: thesis: contradiction

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

end;

suppose j = 10 ; :: thesis: contradiction

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

end;

suppose j = 11 ; :: thesis: contradiction

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

end;

suppose j = 12 ; :: thesis: contradiction

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

end;

suppose j = 13 ; :: thesis: contradiction

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

end;

suppose j = 14 ; :: thesis: contradiction

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

end;

suppose j = 15 ; :: thesis: contradiction

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

end;

suppose j = 16 ; :: thesis: contradiction

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

end;

suppose j = 17 ; :: thesis: contradiction

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

end;

suppose j = 18 ; :: thesis: contradiction

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

end;

suppose j = 19 ; :: thesis: contradiction

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

end;

suppose j = 20 ; :: thesis: contradiction

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

end;

suppose j = 21 ; :: thesis: contradiction

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

end;

suppose j = 22 ; :: thesis: contradiction

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

end;

suppose j = 23 ; :: thesis: contradiction

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

end;

suppose j = 24 ; :: thesis: contradiction

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

end;

suppose j = 25 ; :: thesis: contradiction

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

end;

suppose j = 26 ; :: thesis: contradiction

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

end;

suppose j = 27 ; :: thesis: contradiction

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

end;

suppose j = 28 ; :: thesis: contradiction

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

end;

suppose j = 29 ; :: thesis: contradiction

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

end;

suppose j = 30 ; :: thesis: contradiction

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

end;

suppose j = 31 ; :: thesis: contradiction

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

end;

suppose j = 32 ; :: thesis: contradiction

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

end;

suppose j = 33 ; :: thesis: contradiction

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

end;

suppose j = 34 ; :: thesis: contradiction

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

end;

suppose j = 35 ; :: thesis: contradiction

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

end;

suppose j = 36 ; :: thesis: contradiction

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

end;

suppose j = 37 ; :: thesis: contradiction

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

end;

suppose j = 38 ; :: thesis: contradiction

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

end;

suppose j = 39 ; :: thesis: contradiction

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

end;

suppose j = 40 ; :: thesis: contradiction

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

end;

suppose j = 41 ; :: thesis: contradiction

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

end;

suppose j = 42 ; :: thesis: contradiction

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

end;

suppose j = 43 ; :: thesis: contradiction

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

end;

suppose j = 44 ; :: thesis: contradiction

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

end;

suppose j = 45 ; :: thesis: contradiction

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

end;

suppose j = 46 ; :: thesis: contradiction

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

end;

suppose j = 47 ; :: thesis: contradiction

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

end;

suppose j = 48 ; :: thesis: contradiction

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

end;

suppose j = 49 ; :: thesis: contradiction

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

end;

suppose j = 50 ; :: thesis: contradiction

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

end;

suppose j = 51 ; :: thesis: contradiction

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

end;

suppose j = 52 ; :: thesis: contradiction

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

end;

suppose j = 53 ; :: thesis: contradiction

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

end;

suppose j = 54 ; :: thesis: contradiction

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

end;

suppose j = 55 ; :: thesis: contradiction

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

end;

suppose j = 56 ; :: thesis: contradiction

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

end;

suppose j = 57 ; :: thesis: contradiction

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

end;

suppose j = 58 ; :: thesis: contradiction

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

end;

suppose j = 59 ; :: thesis: contradiction

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

end;

suppose j = 60 ; :: thesis: contradiction

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

end;

suppose j = 61 ; :: thesis: contradiction

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

end;

suppose j = 62 ; :: thesis: contradiction

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

end;

suppose j = 63 ; :: thesis: contradiction

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

end;

suppose j = 64 ; :: thesis: contradiction

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

end;

suppose j = 65 ; :: thesis: contradiction

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

end;

suppose j = 66 ; :: thesis: contradiction

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

end;

suppose j = 67 ; :: thesis: contradiction

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

end;

suppose j = 68 ; :: thesis: contradiction

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

end;

suppose j = 69 ; :: thesis: contradiction

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

end;

suppose j = 70 ; :: thesis: contradiction

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

end;

suppose j = 71 ; :: thesis: contradiction

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

end;

suppose j = 72 ; :: thesis: contradiction

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

end;

end;