let a, b be Element of INT.Ring; ( 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
; 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; ( 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
; ( 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 S1[ Nat] means ex s being Integer st $1 = a9 - (s * b9);
assume A3:
0 <= b9
; 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 S1[k]
proof
now ( ( 0 <= a9 & ex k being Nat st S1[k] ) or ( a9 < 0 & ex k being Nat st S1[k] ) )end;
hence
ex
k being
Nat st
S1[
k]
;
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 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
;
k9 < b9
assume
b9 <= k9
;
contradiction
then reconsider k =
k9 - b9 as
Element of
NAT by INT_1:5;
A9:
k9 > k
k9 - b9 = a9 - ((l9 + 1) * b9)
by A7;
hence
contradiction
by A6, A9;
verum
end;
A11:
( k = 0. INT.Ring or absint . k < absint . b )
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; verum