reconsider b' = b as Integer ;

now

per cases ( 0 <= b' or b' < 0 ) ;

case 0 <= b' ; :: thesis: ex b₁, r being Element of st
( a = (b₁ * b) + r & 0. INT.Ring <= r & r < abs b )

hence ex b₁, r being Element of st
( a = (b₁ * b) + r & 0. INT.Ring <= r & r < abs b ) by A1, Lm8; :: thesis: verum

end;

case A2: b' < 0 ; :: thesis: ex b₁, r being Element of st
( a = (b₁ * b) + r & 0. INT.Ring <= r & r < abs b )

reconsider c = - b' as Element of ;
0 < - b' by A2, XREAL_1:60;
then consider q, r being Element of such that
A3: a = (q * c) + r and
A4: 0. INT.Ring <= r and
A5: r < abs c by Lm3, Lm8;
reconsider t = - q as Element of ;
A6: (t * b) + r = a by A3;
absint . c = absreal . c by Def6
.= abs (- b') by EUCLID:def 2
.= - b' by A2, ABSVALUE:def 1
.= abs b' by A2, ABSVALUE:def 1
.= absreal . b' by EUCLID:def 2
.= absint . b by Def6
.= abs b by Th1 ;
then r < abs b by A5, Th1;
hence ex b₁, r being Element of st
( a = (b₁ * b) + r & 0. INT.Ring <= r & r < abs b ) by A4, A6; :: thesis: verum

end;

end;

end;

hence ex b₁, r being Element of st
( a = (b₁ * b) + r & 0. INT.Ring <= r & r < abs b ) ; :: thesis: verum