take
absint
; :: according to INT_3:def 8 :: thesis: for a, b being Element of INT.Ring st b <> 0. INT.Ring holds

ex q, r being Element of INT.Ring st

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )

let a, b be Element of INT.Ring; :: thesis: ( b <> 0. INT.Ring implies ex q, r being Element of INT.Ring st

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) )

reconsider b9 = b as Integer ;

assume A1: b <> 0. INT.Ring ; :: thesis: ex q, r being Element of INT.Ring st

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) ; :: thesis: verum

ex q, r being Element of INT.Ring st

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )

let a, b be Element of INT.Ring; :: thesis: ( b <> 0. INT.Ring implies ex q, r being Element of INT.Ring st

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) )

reconsider b9 = b as Integer ;

assume A1: b <> 0. INT.Ring ; :: thesis: ex q, r being Element of INT.Ring st

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )

now :: thesis: ( ( 0 <= b9 & ex q, r being Element of INT.Ring st

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) ) or ( b9 < 0 & ex q, r being Element of INT.Ring st

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) ) )end;

hence
ex q, r being Element of INT.Ring st ( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) ) or ( b9 < 0 & ex q, r being Element of INT.Ring st

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) ) )

per cases
( 0 <= b9 or b9 < 0 )
;

end;

case
0 <= b9
; :: thesis: ex q, r being Element of INT.Ring st

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )

hence
ex q, r being Element of INT.Ring st

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) by A1, Lm2; :: thesis: verum

end;( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) by A1, Lm2; :: thesis: verum

case A2:
b9 < 0
; :: thesis: ex q, r being Element of INT.Ring st

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )

reconsider c = - b9 as Element of INT.Ring by INT_1:def 2;

0 < - b9 by A2, XREAL_1:58;

then consider q, r being Element of INT.Ring such that

A3: a = (q * c) + r and

A4: ( r = 0. INT.Ring or absint . r < absint . c ) by Lm2;

A5: ( r = 0. INT.Ring or absint . r < absint . b )

(t * b) + r = a by A3;

hence ex q, r being Element of INT.Ring st

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) by A5; :: thesis: verum

end;0 < - b9 by A2, XREAL_1:58;

then consider q, r being Element of INT.Ring such that

A3: a = (q * c) + r and

A4: ( r = 0. INT.Ring or absint . r < absint . c ) by Lm2;

A5: ( r = 0. INT.Ring or absint . r < absint . b )

proof

reconsider t = - q as Element of INT.Ring ;
assume A6:
r <> 0. INT.Ring
; :: thesis: absint . r < absint . b

absint . c = absreal . c by Def5

.= |.(- b9).| by EUCLID:def 2

.= - b9 by A2, ABSVALUE:def 1

.= |.b9.| by A2, ABSVALUE:def 1

.= absreal . b9 by EUCLID:def 2

.= absint . b by Def5 ;

hence absint . r < absint . b by A4, A6; :: thesis: verum

end;absint . c = absreal . c by Def5

.= |.(- b9).| by EUCLID:def 2

.= - b9 by A2, ABSVALUE:def 1

.= |.b9.| by A2, ABSVALUE:def 1

.= absreal . b9 by EUCLID:def 2

.= absint . b by Def5 ;

hence absint . r < absint . b by A4, A6; :: thesis: verum

(t * b) + r = a by A3;

hence ex q, r being Element of INT.Ring st

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) by A5; :: thesis: verum

( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) ; :: thesis: verum