let i, j be Integer; :: thesis: ( i >= 0 & j >= 0 implies ( |.i.| mod |.j.| = i mod j & |.i.| div |.j.| = i div j ) )
assume that
A1: i >= 0 and
A2: j >= 0 ; :: thesis: ( |.i.| mod |.j.| = i mod j & |.i.| div |.j.| = i div j )

per cases ( j > 0 or j = 0 ) by A2;

suppose A3: j > 0 ; :: thesis: ( |.i.| mod |.j.| = i mod j & |.i.| div |.j.| = i div j )

i = |.i.| by A1, ABSVALUE:def 1;
hence ( |.i.| mod |.j.| = i mod j & |.i.| div |.j.| = i div j ) by A3, ABSVALUE:def 1; :: thesis: verum

end;

suppose A4: j = 0 ; :: thesis: ( |.i.| mod |.j.| = i mod j & |.i.| div |.j.| = i div j )

|.0.| = 0 by ABSVALUE:def 1;
then ( |.i.| mod |.0.| = 0 & |.i.| div |.0.| = 0 ) by INT_1:48, INT_1:def 10;
hence ( |.i.| mod |.j.| = i mod j & |.i.| div |.j.| = i div j ) by A4, INT_1:48, INT_1:def 10; :: thesis: verum

end;

end;