let a, b be Element of INT.Ring; :: thesis: ( b <> 0. INT.Ring implies for b9 being Integer st b9 = b & 0 <= b9 holds

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: for b9 being Integer st b9 = b & 0 <= b9 holds

ex q, r being Element of INT.Ring st

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

reconsider a9 = a as Integer ;

let b9 be Integer; :: thesis: ( b9 = b & 0 <= b9 implies ex q, r being Element of INT.Ring st

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

assume A2: b9 = b ; :: thesis: ( not 0 <= b9 or ex q, r being Element of INT.Ring st

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

defpred S_{1}[ Nat] means ex s being Integer st $1 = a9 - (s * b9);

assume A3: 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 ) )

A4: ex k being Nat st S_{1}[k]

( S_{1}[k] & ( for n being Nat st S_{1}[n] holds

k <= n ) ) from NAT_1:sch 5(A4);

then consider k9 being Nat such that

A6: ex s being Integer st

( k9 = a9 - (s * b9) & ( for n being Nat st ex s9 being Integer st n = a9 - (s9 * b9) holds

k9 <= n ) ) ;

consider l9 being Integer such that

A7: k9 = a9 - (l9 * b9) by A6;

reconsider k = k9, l = l9 as Element of INT.Ring by INT_1:def 2;

A8: ( k9 = 0 or k9 < b9 )

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

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

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: for b9 being Integer st b9 = b & 0 <= b9 holds

ex q, r being Element of INT.Ring st

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

reconsider a9 = a as Integer ;

let b9 be Integer; :: thesis: ( b9 = b & 0 <= b9 implies ex q, r being Element of INT.Ring st

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

assume A2: b9 = b ; :: thesis: ( not 0 <= b9 or ex q, r being Element of INT.Ring st

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

defpred S

assume A3: 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 ) )

A4: ex k being Nat st S

proof
_{1}[k]
; :: thesis: verum

end;

ex k being Nat st now :: thesis: ( ( 0 <= a9 & ex k being Nat st S_{1}[k] ) or ( a9 < 0 & ex k being Nat st S_{1}[k] ) )end;

hence
ex k being Nat st Sper cases
( 0 <= a9 or a9 < 0 )
;

end;

case
0 <= a9
; :: thesis: ex k being Nat st S_{1}[k]

then reconsider a9 = a9 as Element of NAT by INT_1:3;

a9 - (0 * b9) = a9 ;

hence ex k being Nat st S_{1}[k]
; :: thesis: verum

end;a9 - (0 * b9) = a9 ;

hence ex k being Nat st S

case A5:
a9 < 0
; :: thesis: ex k being Nat st S_{1}[k]

1 + 0 <= b9
by A1, A2, A3, INT_1:7;

then 1 - 1 <= b9 - 1 by XREAL_1:9;

then reconsider m = b9 - 1 as Element of NAT by INT_1:3;

reconsider n = - a9 as Element of NAT by A5, INT_1:3;

( a9 - (a9 * b9) = (- a9) * (b9 - 1) & n * m is Element of NAT ) by ORDINAL1:def 12;

hence ex k being Nat st S_{1}[k]
; :: thesis: verum

end;then 1 - 1 <= b9 - 1 by XREAL_1:9;

then reconsider m = b9 - 1 as Element of NAT by INT_1:3;

reconsider n = - a9 as Element of NAT by A5, INT_1:3;

( a9 - (a9 * b9) = (- a9) * (b9 - 1) & n * m is Element of NAT ) by ORDINAL1:def 12;

hence ex k being Nat st S

( S

k <= n ) ) from NAT_1:sch 5(A4);

then consider k9 being Nat such that

A6: ex s being Integer st

( k9 = a9 - (s * b9) & ( for n being Nat st ex s9 being Integer st n = a9 - (s9 * b9) holds

k9 <= n ) ) ;

consider l9 being Integer such that

A7: k9 = a9 - (l9 * b9) by A6;

reconsider k = k9, l = l9 as Element of INT.Ring by INT_1:def 2;

A8: ( k9 = 0 or k9 < b9 )

proof

A11:
( k = 0. INT.Ring or absint . k < absint . b )
assume
k9 <> 0
; :: thesis: k9 < b9

assume b9 <= k9 ; :: thesis: contradiction

then reconsider k = k9 - b9 as Element of NAT by INT_1:5;

A9: k9 > k

hence contradiction by A6, A9; :: thesis: verum

end;assume b9 <= k9 ; :: thesis: contradiction

then reconsider k = k9 - b9 as Element of NAT by INT_1:5;

A9: k9 > k

proof

k9 - b9 = a9 - ((l9 + 1) * b9)
by A7;
reconsider b9 = b9 as Element of NAT by A3, INT_1:3;

assume k9 <= k ; :: thesis: contradiction

then consider x being Nat such that

A10: k = k9 + x by NAT_1:10;

- x = b9 by A10;

hence contradiction by A1, A2; :: thesis: verum

end;assume k9 <= k ; :: thesis: contradiction

then consider x being Nat such that

A10: k = k9 + x by NAT_1:10;

- x = b9 by A10;

hence contradiction by A1, A2; :: thesis: verum

hence contradiction by A6, A9; :: thesis: verum

proof

k + (l * b) = a
by A2, A7;
reconsider b9 = b9 as Element of NAT by A3, INT_1:3;

assume A12: k <> 0. INT.Ring ; :: thesis: absint . k < absint . b

A13: absint . k = absreal . k by Def5

.= |.k9.| by EUCLID:def 2

.= k9 by ABSVALUE:def 1 ;

absint . b = absreal . b9 by A2, Def5

.= |.b9.| by EUCLID:def 2

.= b9 by ABSVALUE:def 1 ;

hence absint . k < absint . b by A8, A12, A13; :: thesis: verum

end;assume A12: k <> 0. INT.Ring ; :: thesis: absint . k < absint . b

A13: absint . k = absreal . k by Def5

.= |.k9.| by EUCLID:def 2

.= k9 by ABSVALUE:def 1 ;

absint . b = absreal . b9 by A2, Def5

.= |.b9.| by EUCLID:def 2

.= b9 by ABSVALUE:def 1 ;

hence absint . k < absint . b by A8, A12, A13; :: thesis: verum

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

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