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

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 ) ;

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

end;

suppose j = 2 ; :: thesis: contradiction

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

end;

suppose j = 3 ; :: thesis: contradiction

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

end;

suppose j = 4 ; :: thesis: contradiction

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

end;

suppose j = 5 ; :: thesis: contradiction

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

end;

suppose j = 6 ; :: thesis: contradiction

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

end;

suppose j = 7 ; :: thesis: contradiction

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

end;

suppose j = 8 ; :: thesis: contradiction

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

end;

suppose j = 9 ; :: thesis: contradiction

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

end;

suppose j = 10 ; :: thesis: contradiction

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

end;

suppose j = 11 ; :: thesis: contradiction

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

end;

suppose j = 12 ; :: thesis: contradiction

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

end;

suppose j = 13 ; :: thesis: contradiction

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

end;

suppose j = 14 ; :: thesis: contradiction

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

end;

suppose j = 15 ; :: thesis: contradiction

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

end;

suppose j = 16 ; :: thesis: contradiction

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

end;

suppose j = 17 ; :: thesis: contradiction

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

end;

suppose j = 18 ; :: thesis: contradiction

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

end;

suppose j = 19 ; :: thesis: contradiction

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

end;

suppose j = 20 ; :: thesis: contradiction

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

end;

suppose j = 21 ; :: thesis: contradiction

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

end;

suppose j = 22 ; :: thesis: contradiction

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

end;

suppose j = 23 ; :: thesis: contradiction

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

end;

suppose j = 24 ; :: thesis: contradiction

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

end;

suppose j = 25 ; :: thesis: contradiction

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

end;

suppose j = 26 ; :: thesis: contradiction

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

end;

suppose j = 27 ; :: thesis: contradiction

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

end;

end;