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₁[ 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₁[k]

proof

now :: thesis: ( ( 0 <= a9 & ex k being Nat st S₁[k] ) or ( a9 < 0 & ex k being Nat st S₁[k] ) )

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

case 0 <= a9 ; :: thesis: ex k being Nat st S₁[k]

then reconsider a9 = a9 as Element of NAT by INT_1:3;
a9 - (0 * b9) = a9 ;
hence ex k being Nat st S₁[k] ; :: thesis: verum

end;

case A5: a9 < 0 ; :: thesis: ex k being Nat st S₁[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₁[k] ; :: thesis: verum

end;

end;

end;

hence ex k being Nat st S₁[k] ; :: thesis: verum

end;

ex k being Nat st
( S₁[k] & ( for n being Nat st S₁[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 )

proof

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

proof

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;

k9 - b9 = a9 - ((l9 + 1) * b9) by A7;
hence contradiction by A6, A9; :: thesis: verum

end;

A11: ( k = 0. INT.Ring or absint . k < absint . b )

proof

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;

k + (l * b) = a by A2, A7;
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