let r be Real; :: thesis: frac |.r.| = (sgn (frac r)) * ((1 / 2) + ((sgn r) * ((frac r) - (1 / 2))))

per cases ( r is integer or not r is integer ) ;

suppose r is integer ; :: thesis: frac |.r.| = (sgn (frac r)) * ((1 / 2) + ((sgn r) * ((frac r) - (1 / 2))))

then ( frac |.r.| = 0 & frac r = 0 ) ;
hence frac |.r.| = (sgn (frac r)) * ((1 / 2) + ((sgn r) * ((frac r) - (1 / 2)))) ; :: thesis: verum

end;

suppose not r is integer ; :: thesis: frac |.r.| = (sgn (frac r)) * ((1 / 2) + ((sgn r) * ((frac r) - (1 / 2))))

then reconsider r = r as non integer Real ;

per cases ( r is positive or r is negative ) ;

suppose r is positive ; :: thesis: frac |.r.| = (sgn (frac r)) * ((1 / 2) + ((sgn r) * ((frac r) - (1 / 2))))

then reconsider r = r as positive Real ;
( r = |.r.| & sgn r = 1 & sgn (frac r) = 1 ) by ABSVALUE:def 2;
hence frac |.r.| = (sgn (frac r)) * ((1 / 2) + ((sgn r) * ((frac r) - (1 / 2)))) ; :: thesis: verum

end;

suppose r is negative ; :: thesis: frac |.r.| = (sgn (frac r)) * ((1 / 2) + ((sgn r) * ((frac r) - (1 / 2))))

then reconsider r = r as negative Real ;
B2: ( sgn r = - 1 & sgn (frac r) = 1 ) by ABSVALUE:def 2;
(1 / 2) + ((sgn r) * ((frac r) - (1 / 2))) = (1 / 2) + ((- 1) * ((frac r) - (1 / 2))) by ABSVALUE:def 2
.= 1 - (frac r)
.= ((frac r) + (frac (- r))) - (frac r) by FAA
.= frac |.r.| by ABSVALUE:def 1 ;
hence frac |.r.| = (sgn (frac r)) * ((1 / 2) + ((sgn r) * ((frac r) - (1 / 2)))) by B2; :: thesis: verum

end;

end;

end;

end;