thus Sum (digits (2398,10)) = 22 by Th919; :: according to NUMBER11:def 1 :: thesis: ( 22 divides 2398 & ( for m being Nat st Sum (digits (m,10)) = 22 & 22 divides m holds
2398 <= m ) )
2398 = 109 * 22 ;
hence 22 divides 2398 by INT_1:def 3; :: thesis: for m being Nat st Sum (digits (m,10)) = 22 & 22 divides m holds
2398 <= m
let m be Nat; :: thesis: ( Sum (digits (m,10)) = 22 & 22 divides m implies 2398 <= m )
assume A1: ( Sum (digits (m,10)) = 22 & 22 divides m ) ; :: thesis: 2398 <= m
then consider j being Nat such that
A2: m = 22 * j by NAT_D:def 3;
assume m < 2398 ; :: thesis: contradiction
then 22 * j < 22 * 109 by A2;
then j < 108 + 1 by XREAL_1:64;
then j <= 108 by NAT_1:9;
then ( j <= 99 or ( j >= 99 + 1 & j <= 108 ) ) by NAT_1:9;
then ( not not j = 0 & ... & not j = 99 or not not j = 100 & ... & not j = 108 ) ;

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 or j = 73 or j = 74 or j = 75 or j = 76 or j = 77 or j = 78 or j = 79 or j = 80 or j = 81 or j = 82 or j = 83 or j = 84 or j = 85 or j = 86 or j = 87 or j = 88 or j = 89 or j = 90 or j = 91 or j = 92 or j = 93 or j = 94 or j = 95 or j = 96 or j = 97 or j = 98 or j = 99 or j = 100 or j = 101 or j = 102 or j = 103 or j = 104 or j = 105 or j = 106 or j = 107 or j = 108 ) ;

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

end;

suppose j = 2 ; :: thesis: contradiction

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

end;

suppose j = 3 ; :: thesis: contradiction

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

end;

suppose j = 4 ; :: thesis: contradiction

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

end;

suppose j = 5 ; :: thesis: contradiction

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

end;

suppose j = 6 ; :: thesis: contradiction

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

end;

suppose j = 7 ; :: thesis: contradiction

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

end;

suppose j = 8 ; :: thesis: contradiction

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

end;

suppose j = 9 ; :: thesis: contradiction

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

end;

suppose j = 10 ; :: thesis: contradiction

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

end;

suppose j = 11 ; :: thesis: contradiction

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

end;

suppose j = 12 ; :: thesis: contradiction

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

end;

suppose j = 13 ; :: thesis: contradiction

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

end;

suppose j = 14 ; :: thesis: contradiction

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

end;

suppose j = 15 ; :: thesis: contradiction

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

end;

suppose j = 16 ; :: thesis: contradiction

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

end;

suppose j = 17 ; :: thesis: contradiction

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

end;

suppose j = 18 ; :: thesis: contradiction

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

end;

suppose j = 19 ; :: thesis: contradiction

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

end;

suppose j = 20 ; :: thesis: contradiction

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

end;

suppose j = 21 ; :: thesis: contradiction

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

end;

suppose j = 22 ; :: thesis: contradiction

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

end;

suppose j = 23 ; :: thesis: contradiction

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

end;

suppose j = 24 ; :: thesis: contradiction

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

end;

suppose j = 25 ; :: thesis: contradiction

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

end;

suppose j = 26 ; :: thesis: contradiction

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

end;

suppose j = 27 ; :: thesis: contradiction

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

end;

suppose j = 28 ; :: thesis: contradiction

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

end;

suppose j = 29 ; :: thesis: contradiction

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

end;

suppose j = 30 ; :: thesis: contradiction

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

end;

suppose j = 31 ; :: thesis: contradiction

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

end;

suppose j = 32 ; :: thesis: contradiction

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

end;

suppose j = 33 ; :: thesis: contradiction

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

end;

suppose j = 34 ; :: thesis: contradiction

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

end;

suppose j = 35 ; :: thesis: contradiction

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

end;

suppose j = 36 ; :: thesis: contradiction

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

end;

suppose j = 37 ; :: thesis: contradiction

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

end;

suppose j = 38 ; :: thesis: contradiction

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

end;

suppose j = 39 ; :: thesis: contradiction

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

end;

suppose j = 40 ; :: thesis: contradiction

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

end;

suppose j = 41 ; :: thesis: contradiction

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

end;

suppose j = 42 ; :: thesis: contradiction

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

end;

suppose j = 43 ; :: thesis: contradiction

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

end;

suppose j = 44 ; :: thesis: contradiction

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

end;

suppose j = 45 ; :: thesis: contradiction

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

end;

suppose j = 46 ; :: thesis: contradiction

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

end;

suppose j = 47 ; :: thesis: contradiction

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

end;

suppose j = 48 ; :: thesis: contradiction

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

end;

suppose j = 49 ; :: thesis: contradiction

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

end;

suppose j = 50 ; :: thesis: contradiction

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

end;

suppose j = 51 ; :: thesis: contradiction

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

end;

suppose j = 52 ; :: thesis: contradiction

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

end;

suppose j = 53 ; :: thesis: contradiction

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

end;

suppose j = 54 ; :: thesis: contradiction

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

end;

suppose j = 55 ; :: thesis: contradiction

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

end;

suppose j = 56 ; :: thesis: contradiction

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

end;

suppose j = 57 ; :: thesis: contradiction

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

end;

suppose j = 58 ; :: thesis: contradiction

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

end;

suppose j = 59 ; :: thesis: contradiction

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

end;

suppose j = 60 ; :: thesis: contradiction

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

end;

suppose j = 61 ; :: thesis: contradiction

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

end;

suppose j = 62 ; :: thesis: contradiction

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

end;

suppose j = 63 ; :: thesis: contradiction

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

end;

suppose j = 64 ; :: thesis: contradiction

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

end;

suppose j = 65 ; :: thesis: contradiction

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

end;

suppose j = 66 ; :: thesis: contradiction

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

end;

suppose j = 67 ; :: thesis: contradiction

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

end;

suppose j = 68 ; :: thesis: contradiction

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

end;

suppose j = 69 ; :: thesis: contradiction

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

end;

suppose j = 70 ; :: thesis: contradiction

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

end;

suppose j = 71 ; :: thesis: contradiction

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

end;

suppose j = 72 ; :: thesis: contradiction

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

end;

suppose j = 73 ; :: thesis: contradiction

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

end;

suppose j = 74 ; :: thesis: contradiction

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

end;

suppose j = 75 ; :: thesis: contradiction

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

end;

suppose j = 76 ; :: thesis: contradiction

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

end;

suppose j = 77 ; :: thesis: contradiction

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

end;

suppose j = 78 ; :: thesis: contradiction

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

end;

suppose j = 79 ; :: thesis: contradiction

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

end;

suppose j = 80 ; :: thesis: contradiction

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

end;

suppose j = 81 ; :: thesis: contradiction

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

end;

suppose j = 82 ; :: thesis: contradiction

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

end;

suppose j = 83 ; :: thesis: contradiction

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

end;

suppose j = 84 ; :: thesis: contradiction

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

end;

suppose j = 85 ; :: thesis: contradiction

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

end;

suppose j = 86 ; :: thesis: contradiction

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

end;

suppose j = 87 ; :: thesis: contradiction

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

end;

suppose j = 88 ; :: thesis: contradiction

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

end;

suppose j = 89 ; :: thesis: contradiction

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

end;

suppose j = 90 ; :: thesis: contradiction

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

end;

suppose j = 91 ; :: thesis: contradiction

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

end;

suppose j = 92 ; :: thesis: contradiction

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

end;

suppose j = 93 ; :: thesis: contradiction

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

end;

suppose j = 94 ; :: thesis: contradiction

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

end;

suppose j = 95 ; :: thesis: contradiction

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

end;

suppose j = 96 ; :: thesis: contradiction

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

end;

suppose j = 97 ; :: thesis: contradiction

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

end;

suppose j = 98 ; :: thesis: contradiction

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

end;

suppose j = 99 ; :: thesis: contradiction

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

end;

suppose j = 100 ; :: thesis: contradiction

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

end;

suppose j = 101 ; :: thesis: contradiction

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

end;

suppose j = 102 ; :: thesis: contradiction

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

end;

suppose j = 103 ; :: thesis: contradiction

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

end;

suppose j = 104 ; :: thesis: contradiction

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

end;

suppose j = 105 ; :: thesis: contradiction

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

end;

suppose j = 106 ; :: thesis: contradiction

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

end;

suppose j = 107 ; :: thesis: contradiction

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

end;

suppose j = 108 ; :: thesis: contradiction

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

end;

end;