let a, b be Element of INT.Ring ; :: thesis: ( b <> 0. INT.Ring implies for b' being Integer st b' = b & 0 <= b' holds
ex q, r being Element of INT.Ring st
( a = (q * b) + r & 0. INT.Ring <= r & r < abs b ) )
assume A1: b <> 0. INT.Ring ; :: thesis: for b' being Integer st b' = b & 0 <= b' holds
ex q, r being Element of INT.Ring st
( a = (q * b) + r & 0. INT.Ring <= r & r < abs b )
let b' be Integer; :: thesis: ( b' = b & 0 <= b' implies ex q, r being Element of INT.Ring st
( a = (q * b) + r & 0. INT.Ring <= r & r < abs b ) )
assume A2: b' = b ; :: thesis: ( not 0 <= b' or ex q, r being Element of INT.Ring st
( a = (q * b) + r & 0. INT.Ring <= r & r < abs b ) )
assume A3: 0 <= b' ; :: thesis: ex q, r being Element of INT.Ring st
( a = (q * b) + r & 0. INT.Ring <= r & r < abs b )
reconsider a' = a as Integer ;
defpred S₁[ Nat] means ex s being Integer st $1 = a' - (s * b');
A4: ex k being Nat st S₁[k]

proof

now

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

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

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

end;

case A5: a' < 0 ; :: thesis: ex k being Nat st S₁[k]

A6: a' - (a' * b') = (- a') * (b' - 1) ;
0 < - a' by A5, XREAL_1:60;
then reconsider n = - a' as Element of NAT by INT_1:16;
1 + 0 <= b' by A1, A2, A3, Lm3, INT_1:20;
then 1 - 1 <= b' - 1 by XREAL_1:11;
then reconsider m = b' - 1 as Element of NAT by INT_1:16;
n * m is Element of NAT ;
hence ex k being Nat st S₁[k] by A6; :: 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 k' being Nat such that
A7: ex s being Integer st
( k' = a' - (s * b') & ( for n being Nat st ex s' being Integer st n = a' - (s' * b') holds
k' <= n ) ) ;
consider l' being Integer such that
A8: k' = a' - (l' * b') by A7;
A9: ( k' = 0 or k' < b' )

proof

assume k' <> 0 ; :: thesis: k' < b'
assume b' <= k' ; :: thesis: contradiction
then reconsider k = k' - b' as Element of NAT by INT_1:18;
A10: k' > k

proof

assume k' <= k ; :: thesis: contradiction
then consider x being Nat such that
A11: k = k' + x by NAT_1:10;
reconsider b' = b' as Element of NAT by A3, INT_1:16;
A12: 0 < b' by A1, A2, Lm3;
- x = b' by A11;
hence contradiction by A12; :: thesis: verum

end;

k' - b' = a' - ((l' + 1) * b') by A8;
hence contradiction by A7, A10; :: thesis: verum

end;

reconsider k = k', l = l' as Element of INT.Ring by INT_1:def 2;
consider d being Element of INT.Ring ;
A13: k + (l * b) = a by A2, A8;
( 0. INT.Ring <= k & k < abs b )

proof

reconsider k' = k' as Element of NAT by ORDINAL1:def 13;
reconsider b' = b' as Element of NAT by A3, INT_1:16;
A14: absint . b = b'

proof

absint . b = absreal . b' by A2, Def6
.= abs b' by EUCLID:def 2
.= b' by ABSVALUE:def 1 ;
hence absint . b = b' ; :: thesis: verum

end;

then A15: abs b <> 0. INT.Ring by A1, A2, Th1;

now

per cases ( k' = 0 or k' < b' ) by A9;

case k' = 0 ; :: thesis: ( 0. INT.Ring <= k & k < abs b )

hence ( 0. INT.Ring <= k & k < abs b ) by A14, A15, Lm3, Th1; :: thesis: verum

end;

case k' < b' ; :: thesis: ( 0. INT.Ring <= k & k < abs b )

hence ( 0. INT.Ring <= k & k < abs b ) by A14, Lm2, Th1, FUNCT_7:def 1; :: thesis: verum

end;

end;

end;

hence ( 0. INT.Ring <= k & k < abs b ) ; :: thesis: verum

end;

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