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;