thus Sum (digits (4975,10)) = 25 by Th1376; :: according to NUMBER11:def 1 :: thesis:
4975 = 199 * 25 ;
hence 25 divides 4975 by INT_1:def 3; :: thesis:
let m be Nat; :: thesis:
assume A1: ( Sum (digits (m,10)) = 25 & 25 divides m ) ; :: thesis:
then consider j being Nat such that
A2: m = 25 * j by NAT_D:def 3;
assume m < 4975 ; :: thesis:
then 25 * j < 25 * 199 by A2;
then j < 198 + 1 by XREAL_1:64;
then j <= 198 by NAT_1:9;
then ( j <= 99 or ( j >= 99 + 1 & j <= 198 ) ) by NAT_1:9;
then ( not not j = 0 & ... & not j = 99 or not not j = 100 & ... & not j = 198 ) ;

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 or j = 109 or j = 110 or j = 111 or j = 112 or j = 113 or j = 114 or j = 115 or j = 116 or j = 117 or j = 118 or j = 119 or j = 120 or j = 121 or j = 122 or j = 123 or j = 124 or j = 125 or j = 126 or j = 127 or j = 128 or j = 129 or j = 130 or j = 131 or j = 132 or j = 133 or j = 134 or j = 135 or j = 136 or j = 137 or j = 138 or j = 139 or j = 140 or j = 141 or j = 142 or j = 143 or j = 144 or j = 145 or j = 146 or j = 147 or j = 148 or j = 149 or j = 150 or j = 151 or j = 152 or j = 153 or j = 154 or j = 155 or j = 156 or j = 157 or j = 158 or j = 159 or j = 160 or j = 161 or j = 162 or j = 163 or j = 164 or j = 165 or j = 166 or j = 167 or j = 168 or j = 169 or j = 170 or j = 171 or j = 172 or j = 173 or j = 174 or j = 175 or j = 176 or j = 177 or j = 178 or j = 179 or j = 180 or j = 181 or j = 182 or j = 183 or j = 184 or j = 185 or j = 186 or j = 187 or j = 188 or j = 189 or j = 190 or j = 191 or j = 192 or j = 193 or j = 194 or j = 195 or j = 196 or j = 197 or j = 198 ) ;

suppose j = 0 ; :: thesis:

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

end;

suppose j = 1 ; :: thesis:

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

end;

suppose j = 2 ; :: thesis:

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

end;

suppose j = 3 ; :: thesis:

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

end;

suppose j = 4 ; :: thesis:

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

end;

suppose j = 5 ; :: thesis:

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

end;

suppose j = 6 ; :: thesis:

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

end;

suppose j = 7 ; :: thesis:

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

end;

suppose j = 8 ; :: thesis:

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

end;

suppose j = 9 ; :: thesis:

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

end;

suppose j = 10 ; :: thesis:

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

end;

suppose j = 11 ; :: thesis:

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

end;

suppose j = 12 ; :: thesis:

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

end;

suppose j = 13 ; :: thesis:

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

end;

suppose j = 14 ; :: thesis:

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

end;

suppose j = 15 ; :: thesis:

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

end;

suppose j = 16 ; :: thesis:

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

end;

suppose j = 17 ; :: thesis:

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

end;

suppose j = 18 ; :: thesis:

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

end;

suppose j = 19 ; :: thesis:

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

end;

suppose j = 20 ; :: thesis:

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

end;

suppose j = 21 ; :: thesis:

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

end;

suppose j = 22 ; :: thesis:

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

end;

suppose j = 23 ; :: thesis:

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

end;

suppose j = 24 ; :: thesis:

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

end;

suppose j = 25 ; :: thesis:

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

end;

suppose j = 26 ; :: thesis:

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

end;

suppose j = 27 ; :: thesis:

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

end;

suppose j = 28 ; :: thesis:

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

end;

suppose j = 29 ; :: thesis:

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

end;

suppose j = 30 ; :: thesis:

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

end;

suppose j = 31 ; :: thesis:

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

end;

suppose j = 32 ; :: thesis:

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

end;

suppose j = 33 ; :: thesis:

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

end;

suppose j = 34 ; :: thesis:

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

end;

suppose j = 35 ; :: thesis:

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

end;

suppose j = 36 ; :: thesis:

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

end;

suppose j = 37 ; :: thesis:

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

end;

suppose j = 38 ; :: thesis:

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

end;

suppose j = 39 ; :: thesis:

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

end;

suppose j = 40 ; :: thesis:

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

end;

suppose j = 41 ; :: thesis:

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

end;

suppose j = 42 ; :: thesis:

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

end;

suppose j = 43 ; :: thesis:

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

end;

suppose j = 44 ; :: thesis:

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

end;

suppose j = 45 ; :: thesis:

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

end;

suppose j = 46 ; :: thesis:

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

end;

suppose j = 47 ; :: thesis:

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

end;

suppose j = 48 ; :: thesis:

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

end;

suppose j = 49 ; :: thesis:

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

end;

suppose j = 50 ; :: thesis:

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

end;

suppose j = 51 ; :: thesis:

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

end;

suppose j = 52 ; :: thesis:

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

end;

suppose j = 53 ; :: thesis:

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

end;

suppose j = 54 ; :: thesis:

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

end;

suppose j = 55 ; :: thesis:

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

end;

suppose j = 56 ; :: thesis:

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

end;

suppose j = 57 ; :: thesis:

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

end;

suppose j = 58 ; :: thesis:

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

end;

suppose j = 59 ; :: thesis:

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

end;

suppose j = 60 ; :: thesis:

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

end;

suppose j = 61 ; :: thesis:

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

end;

suppose j = 62 ; :: thesis:

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

end;

suppose j = 63 ; :: thesis:

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

end;

suppose j = 64 ; :: thesis:

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

end;

suppose j = 65 ; :: thesis:

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

end;

suppose j = 66 ; :: thesis:

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

end;

suppose j = 67 ; :: thesis:

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

end;

suppose j = 68 ; :: thesis:

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

end;

suppose j = 69 ; :: thesis:

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

end;

suppose j = 70 ; :: thesis:

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

end;

suppose j = 71 ; :: thesis:

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

end;

suppose j = 72 ; :: thesis:

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

end;

suppose j = 73 ; :: thesis:

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

end;

suppose j = 74 ; :: thesis:

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

end;

suppose j = 75 ; :: thesis:

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

end;

suppose j = 76 ; :: thesis:

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

end;

suppose j = 77 ; :: thesis:

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

end;

suppose j = 78 ; :: thesis:

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

end;

suppose j = 79 ; :: thesis:

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

end;

suppose j = 80 ; :: thesis:

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

end;

suppose j = 81 ; :: thesis:

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

end;

suppose j = 82 ; :: thesis:

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

end;

suppose j = 83 ; :: thesis:

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

end;

suppose j = 84 ; :: thesis:

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

end;

suppose j = 85 ; :: thesis:

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

end;

suppose j = 86 ; :: thesis:

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

end;

suppose j = 87 ; :: thesis:

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

end;

suppose j = 88 ; :: thesis:

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

end;

suppose j = 89 ; :: thesis:

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

end;

suppose j = 90 ; :: thesis:

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

end;

suppose j = 91 ; :: thesis:

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

end;

suppose j = 92 ; :: thesis:

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

end;

suppose j = 93 ; :: thesis:

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

end;

suppose j = 94 ; :: thesis:

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

end;

suppose j = 95 ; :: thesis:

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

end;

suppose j = 96 ; :: thesis:

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

end;

suppose j = 97 ; :: thesis:

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

end;

suppose j = 98 ; :: thesis:

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

end;

suppose j = 99 ; :: thesis:

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

end;

suppose j = 100 ; :: thesis:

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

end;

suppose j = 101 ; :: thesis:

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

end;

suppose j = 102 ; :: thesis:

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

end;

suppose j = 103 ; :: thesis:

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

end;

suppose j = 104 ; :: thesis:

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

end;

suppose j = 105 ; :: thesis:

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

end;

suppose j = 106 ; :: thesis:

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

end;

suppose j = 107 ; :: thesis:

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

end;

suppose j = 108 ; :: thesis:

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

end;

suppose j = 109 ; :: thesis:

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

end;

suppose j = 110 ; :: thesis:

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

end;

suppose j = 111 ; :: thesis:

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

end;

suppose j = 112 ; :: thesis:

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

end;

suppose j = 113 ; :: thesis:

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

end;

suppose j = 114 ; :: thesis:

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

end;

suppose j = 115 ; :: thesis:

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

end;

suppose j = 116 ; :: thesis:

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

end;

suppose j = 117 ; :: thesis:

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

end;

suppose j = 118 ; :: thesis:

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

end;

suppose j = 119 ; :: thesis:

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

end;

suppose j = 120 ; :: thesis:

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

end;

suppose j = 121 ; :: thesis:

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

end;

suppose j = 122 ; :: thesis:

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

end;

suppose j = 123 ; :: thesis:

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

end;

suppose j = 124 ; :: thesis:

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

end;

suppose j = 125 ; :: thesis:

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

end;

suppose j = 126 ; :: thesis:

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

end;

suppose j = 127 ; :: thesis:

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

end;

suppose j = 128 ; :: thesis:

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

end;

suppose j = 129 ; :: thesis:

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

end;

suppose j = 130 ; :: thesis:

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

end;

suppose j = 131 ; :: thesis:

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

end;

suppose j = 132 ; :: thesis:

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

end;

suppose j = 133 ; :: thesis:

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

end;

suppose j = 134 ; :: thesis:

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

end;

suppose j = 135 ; :: thesis:

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

end;

suppose j = 136 ; :: thesis:

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

end;

suppose j = 137 ; :: thesis:

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

end;

suppose j = 138 ; :: thesis:

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

end;

suppose j = 139 ; :: thesis:

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

end;

suppose j = 140 ; :: thesis:

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

end;

suppose j = 141 ; :: thesis:

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

end;

suppose j = 142 ; :: thesis:

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

end;

suppose j = 143 ; :: thesis:

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

end;

suppose j = 144 ; :: thesis:

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

end;

suppose j = 145 ; :: thesis:

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

end;

suppose j = 146 ; :: thesis:

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

end;

suppose j = 147 ; :: thesis:

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

end;

suppose j = 148 ; :: thesis:

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

end;

suppose j = 149 ; :: thesis:

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

end;

suppose j = 150 ; :: thesis:

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

end;

suppose j = 151 ; :: thesis:

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

end;

suppose j = 152 ; :: thesis:

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

end;

suppose j = 153 ; :: thesis:

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

end;

suppose j = 154 ; :: thesis:

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

end;

suppose j = 155 ; :: thesis:

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

end;

suppose j = 156 ; :: thesis:

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

end;

suppose j = 157 ; :: thesis:

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

end;

suppose j = 158 ; :: thesis:

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

end;

suppose j = 159 ; :: thesis:

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

end;

suppose j = 160 ; :: thesis:

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

end;

suppose j = 161 ; :: thesis:

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

end;

suppose j = 162 ; :: thesis:

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

end;

suppose j = 163 ; :: thesis:

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

end;

suppose j = 164 ; :: thesis:

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

end;

suppose j = 165 ; :: thesis:

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

end;

suppose j = 166 ; :: thesis:

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

end;

suppose j = 167 ; :: thesis:

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

end;

suppose j = 168 ; :: thesis:

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

end;

suppose j = 169 ; :: thesis:

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

end;

suppose j = 170 ; :: thesis:

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

end;

suppose j = 171 ; :: thesis:

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

end;

suppose j = 172 ; :: thesis:

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

end;

suppose j = 173 ; :: thesis:

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

end;

suppose j = 174 ; :: thesis:

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

end;

suppose j = 175 ; :: thesis:

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

end;

suppose j = 176 ; :: thesis:

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

end;

suppose j = 177 ; :: thesis:

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

end;

suppose j = 178 ; :: thesis:

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

end;

suppose j = 179 ; :: thesis:

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

end;

suppose j = 180 ; :: thesis:

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

end;

suppose j = 181 ; :: thesis:

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

end;

suppose j = 182 ; :: thesis:

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

end;

suppose j = 183 ; :: thesis:

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

end;

suppose j = 184 ; :: thesis:

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

end;

suppose j = 185 ; :: thesis:

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

end;

suppose j = 186 ; :: thesis:

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

end;

suppose j = 187 ; :: thesis:

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

end;

suppose j = 188 ; :: thesis:

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

end;

suppose j = 189 ; :: thesis:

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

end;

suppose j = 190 ; :: thesis:

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

end;

suppose j = 191 ; :: thesis:

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

end;

suppose j = 192 ; :: thesis:

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

end;

suppose j = 193 ; :: thesis:

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

end;

suppose j = 194 ; :: thesis:

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

end;

suppose j = 195 ; :: thesis:

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

end;

suppose j = 196 ; :: thesis:

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

end;

suppose j = 197 ; :: thesis:

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

end;

suppose j = 198 ; :: thesis:

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

end;

end;