let a, b be Element of INT.Ring; :: according to INT_3:def 9 :: 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 ) ) )

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 ) ) )

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 ) )

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

end;

suppose
0 <= b
; :: 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

suppose A2:
b < 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 = - b as Element of INT.Ring ;

0 < - b 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 < - b 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

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

.= - b by A2, ABSVALUE:def 1

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

.= absreal . b 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

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

.= - b by A2, ABSVALUE:def 1

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

.= absreal . b 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