let b be Real; :: thesis: for d being Integer st d <> 5 holds
(b + (((- d) + |.d.|) + 4)) + 1 <> b + d
let d be Integer; :: thesis: ( d <> 5 implies (b + (((- d) + |.d.|) + 4)) + 1 <> b + d )
assume A1: d <> 5 ; :: thesis: (b + (((- d) + |.d.|) + 4)) + 1 <> b + d
assume A2: (b + (((- d) + |.d.|) + 4)) + 1 = b + d ; :: thesis: contradiction

per cases ( d >= 0 or d < 0 ) ;

suppose d >= 0 ; :: thesis: contradiction

then |.d.| = d by ABSVALUE:def 1;
hence contradiction by A1, A2; :: thesis: verum

end;

suppose d < 0 ; :: thesis: contradiction

then |.d.| = - d by ABSVALUE:def 1;
hence contradiction by A2, Lm3; :: thesis: verum

end;

end;