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 < |.b.| & a = (q2 * b) + r2 & 0. INT.Ring <= r2 & r2 < |.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 < |.b.| and
A5: a = (q2 * b) + r2 and
A6: 0. INT.Ring <= r2 and
A7: r2 < |.b.| ; :: thesis: ( q1 = q2 & r1 = r2 )
reconsider r29 = r2, r19 = r1, q29 = q2, q19 = q1, b9 = b as Integer ;
now :: thesis: ( ( 0 <= r19 - r29 & q1 = q2 ) or ( r19 - r29 < 0 & q1 = q2 ) )
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 :: thesis: ( ( 0 = r19 - r29 & q1 = q2 ) or ( 0 <> r19 - r29 & q1 = q2 ) )
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; :: 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 Def5;
then reconsider c = absreal . b9 as Element of NAT ;
absreal . d9 = absint . e by Def5;
then reconsider d = absreal . d9 as Element of NAT ;
d * c >= 1 * c by A10, Lm1, NAT_1:4;
hence (absreal . (q29 - q19)) * (absreal . b9) >= absreal . b9 ; :: thesis: verum
end;
A12: r19 + (- r29) <= r19 + 0 by A6, XREAL_1:6;
A13: |.b.| = absint . b by Th1
.= absreal . b by Def5 ;
r19 - r29 = |.((q29 - q19) * b9).| by A2, A5, A8, ABSVALUE:def 1
.= |.(q29 - q19).| * |.b9.| by COMPLEX1:65
.= (absreal . (q29 - q19)) * |.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:58;
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 Def5;
then reconsider c = absreal . b9 as Element of NAT ;
absreal . d9 = absint . e by Def5;
then reconsider d = absreal . d9 as Element of NAT ;
d * c >= 1 * c by A15, Lm1, NAT_1:4;
hence (absreal . (q19 - q29)) * (absreal . b9) >= absreal . b9 ; :: thesis: verum
end;
A17: |.b.| = absint . b by Th1
.= absreal . b by Def5 ;
- (r19 - r29) > 0 by A14, XREAL_1:58;
then A18: r29 - r19 = |.((q19 - q29) * b9).| by A2, A5, ABSVALUE:def 1
.= |.(q19 - q29).| * |.b9.| by COMPLEX1:65
.= (absreal . (q19 - q29)) * |.b9.| by EUCLID:def 2
.= (absreal . (q19 - q29)) * (absreal . b9) by EUCLID:def 2 ;
r29 + (- r19) <= r29 + 0 by A3, XREAL_1:6;
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