consider d being Element of ;
let a, b be Element of ; :: thesis: ( b <> 0. INT.Ring implies for b' being Integer st b' = b & 0 <= b' holds
ex q, r being Element of 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 st
( a = (q * b) + r & 0. INT.Ring <= r & r < abs b )
reconsider a' = a as Integer ;
let b' be Integer; :: thesis: ( b' = b & 0 <= b' implies ex q, r being Element of 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 st
( a = (q * b) + r & 0. INT.Ring <= r & r < abs b ) )
defpred S1[ Nat] means ex s being Integer st $1 = a' - (s * b');
assume A3: 0 <= b' ; :: thesis: ex q, r being Element of st
( a = (q * b) + r & 0. INT.Ring <= r & r < abs b )
A4: ex k being Nat st S1[k]
proof
now
per cases ( 0 <= a' or a' < 0 ) ;
case 0 <= a' ; :: thesis: ex k being Nat st S1[k]
then reconsider a' = a' as Element of NAT by INT_1:16;
a' - (0 * b') = a' ;
hence ex k being Nat st S1[k] ; :: thesis: verum
end;
case A5: a' < 0 ; :: thesis: ex k being Nat st S1[k]
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;
reconsider n = - a' as Element of NAT by A5, INT_1:16;
( a' - (a' * b') = (- a') * (b' - 1) & n * m is Element of NAT ) ;
hence ex k being Nat st S1[k] ; :: thesis: verum
end;
end;
end;
hence ex k being Nat st S1[k] ; :: thesis: verum
end;
ex k being Nat st
( S1[k] & ( for n being Nat st S1[n] holds
k <= n ) ) from NAT_1:sch 5(A4);
 then consider k' being Nat such that
A6: 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
A7: k' = a' - (l' * b') by A6;
reconsider k = k', l = l' as Element of by INT_1:def 2;
A8: ( 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;
A9: k' > k
proof
reconsider b' = b' as Element of NAT by A3, INT_1:16;
assume k' <= k ; :: thesis: contradiction
then consider x being Nat such that
A10: k = k' + x by NAT_1:10;
- x = b' by A10;
hence contradiction by A1, A2, Lm2, FUNCT_7:def 1; :: thesis: verum
end;
k' - b' = a' - ((l' + 1) * b') by A7;
hence contradiction by A6, A9; :: thesis: verum
end;
A11: ( 0. INT.Ring <= k & k < abs b )
proof
reconsider b' = b' as Element of NAT by A3, INT_1:16;
reconsider k' = k' as Element of NAT by ORDINAL1:def 13;
A12: absint . b = absreal . b' by A2, Def6
.= abs b' by EUCLID:def 2
.= b' by ABSVALUE:def 1 ;
now
per cases ( k' = 0 or k' < b' ) by A8;
case k' = 0 ; :: thesis: ( 0. INT.Ring <= k & k < abs b )
hence ( 0. INT.Ring <= k & k < abs b ) by A1, A2, A12, 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 A12, Lm2, Th1, FUNCT_7:def 1; :: thesis: verum
end;
end;
end;
hence ( 0. INT.Ring <= k & k < abs b ) ; :: thesis: verum
end;
k + (l * b) = a by A2, A7;
hence ex q, r being Element of st
( a = (q * b) + r & 0. INT.Ring <= r & r < abs b ) by A11; :: thesis: verum