let a, b, q1, q2, r1, r2 be Element of INT.Ring ; :: thesis: ( b <> 0. INT.Ring & a = (q1 * b) + r1 & 0. INT.Ring <= r1 & r1 < abs b & a = (q2 * b) + r2 & 0. INT.Ring <= r2 & r2 < abs b implies ( q1 = q2 & r1 = r2 ) )
assume that
A1: b <> 0. INT.Ring and
A2: a = (q1 * b) + r1 and
A3: 0. INT.Ring <= r1 and
A4: r1 < abs b and
A5: a = (q2 * b) + r2 and
A6: 0. INT.Ring <= r2 and
A7: r2 < abs b ; :: thesis: ( q1 = q2 & r1 = r2 )
reconsider r29 = r2 as Integer ;
reconsider r19 = r1 as Integer ;
reconsider q29 = q2 as Integer ;
reconsider q19 = q1 as Integer ;
reconsider b9 = b as Integer ;

now

per cases ( 0 <= r19 - r29 or r19 - r29 < 0 ) ;

case A8: 0 <= r19 - r29 ; :: thesis: q1 = q2

A9: (q29 - q19) * b9 = r19 - r29 by A2, A5;

now

per cases ( 0 = r19 - r29 or 0 <> r19 - r29 ) ;

case 0 = r19 - r29 ; :: thesis: q1 = q2

then ( q29 - q19 = 0 or b9 = 0 ) by A9, XCMPLX_1:6;
hence q1 = q2 by A1, FUNCT_7:def 1; :: thesis: verum

end;

case 0 <> r19 - r29 ; :: thesis: q1 = q2

then A10: 0 <> q29 - q19 by A9;
A11: (absreal . (q29 - q19)) * (absreal . b9) >= absreal . b9

proof

reconsider e = q2 + (- q1) as Element of INT.Ring ;
reconsider d9 = q29 - q19 as Integer ;
absreal . b9 = absint . b by Def6;
then reconsider c = absreal . b9 as Element of NAT ;
absreal . d9 = absint . e by Def6;
then reconsider d = absreal . d9 as Element of NAT ;
d * c >= 1 * c by A10, Lm6, NAT_1:4;
hence (absreal . (q29 - q19)) * (absreal . b9) >= absreal . b9 ; :: thesis: verum

end;

A12: r19 + (- r29) <= r19 + 0 by A6, Lm3, XREAL_1:8;
A13: abs b = absint . b by Th1
.= absreal . b by Def6 ;
r19 - r29 = abs ((q29 - q19) * b9) by A2, A5, A8, ABSVALUE:def 1
.= (abs (q29 - q19)) * (abs b9) by COMPLEX1:151
.= (absreal . (q29 - q19)) * (abs b9) by EUCLID:def 2
.= (absreal . (q29 - q19)) * (absreal . b9) by EUCLID:def 2 ;
hence q1 = q2 by A4, A11, A12, A13, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence q1 = q2 ; :: thesis: verum

end;

case A14: r19 - r29 < 0 ; :: thesis: q1 = q2

( - (r19 - r29) = r29 - r19 & (q19 - q29) * b9 = r29 - r19 ) by A2, A5;
then A15: 0 <> q19 - q29 by A14, XREAL_1:60;
A16: (absreal . (q19 - q29)) * (absreal . b9) >= absreal . b9

proof

reconsider e = q1 + (- q2) as Element of INT.Ring ;
reconsider d9 = q19 - q29 as Integer ;
absreal . b9 = absint . b by Def6;
then reconsider c = absreal . b9 as Element of NAT ;
absreal . d9 = absint . e by Def6;
then reconsider d = absreal . d9 as Element of NAT ;
d * c >= 1 * c by A15, Lm6, NAT_1:4;
hence (absreal . (q19 - q29)) * (absreal . b9) >= absreal . b9 ; :: thesis: verum

end;

A17: abs b = absint . b by Th1
.= absreal . b by Def6 ;
- (r19 - r29) > 0 by A14, XREAL_1:60;
then A18: r29 - r19 = abs ((q19 - q29) * b9) by A2, A5, ABSVALUE:def 1
.= (abs (q19 - q29)) * (abs b9) by COMPLEX1:151
.= (absreal . (q19 - q29)) * (abs b9) by EUCLID:def 2
.= (absreal . (q19 - q29)) * (absreal . b9) by EUCLID:def 2 ;
r29 + (- r19) <= r29 + 0 by A3, Lm3, XREAL_1:8;
hence q1 = q2 by A7, A16, A17, A18, XXREAL_0:2; :: thesis: verum

end;

end;

end;

hence ( q1 = q2 & r1 = r2 ) by A2, A5; :: thesis: verum