let a, b, q1, q2, r1, r2 be Element of ; :: 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 r2' = r2 as Integer ;
reconsider r1' = r1 as Integer ;
reconsider q2' = q2 as Integer ;
reconsider q1' = q1 as Integer ;
reconsider b' = b as Integer ;
now
per cases ( 0 <= r1' - r2' or r1' - r2' < 0 ) ;
case A8: 0 <= r1' - r2' ; :: thesis: q1 = q2
A9: (q2' - q1') * b' = r1' - r2' by A2, A5;
now
per cases ( 0 = r1' - r2' or 0 <> r1' - r2' ) ;
case 0 = r1' - r2' ; :: thesis: q1 = q2
then ( q2' - q1' = 0 or b' = 0 ) by A9, XCMPLX_1:6;
hence q1 = q2 by A1, FUNCT_7:def 1; :: thesis: verum
end;
case 0 <> r1' - r2' ; :: thesis: q1 = q2
then A10: 0 <> q2' - q1' by A9;
A11: (absreal . (q2' - q1')) * (absreal . b') >= absreal . b'
proof
reconsider e = q2 + (- q1) as Element of ;
reconsider d' = q2' - q1' as Integer ;
absreal . b' = absint . b by Def6;
then reconsider c = absreal . b' as Element of NAT ;
absreal . d' = absint . e by Def6;
then reconsider d = absreal . d' as Element of NAT ;
d * c >= 1 * c by A10, Lm6, NAT_1:4;
hence (absreal . (q2' - q1')) * (absreal . b') >= absreal . b' ; :: thesis: verum
end;
A12: r1' + (- r2') <= r1' + 0 by A6, Lm3, XREAL_1:8;
A13: abs b = absint . b by Th1
.= absreal . b by Def6 ;
r1' - r2' = abs ((q2' - q1') * b') by A2, A5, A8, ABSVALUE:def 1
.= (abs (q2' - q1')) * (abs b') by COMPLEX1:151
.= (absreal . (q2' - q1')) * (abs b') by EUCLID:def 2
.= (absreal . (q2' - q1')) * (absreal . b') 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: r1' - r2' < 0 ; :: thesis: q1 = q2
( - (r1' - r2') = r2' - r1' & (q1' - q2') * b' = r2' - r1' ) by A2, A5;
then A15: 0 <> q1' - q2' by A14, XREAL_1:60;
A16: (absreal . (q1' - q2')) * (absreal . b') >= absreal . b'
proof
reconsider e = q1 + (- q2) as Element of ;
reconsider d' = q1' - q2' as Integer ;
absreal . b' = absint . b by Def6;
then reconsider c = absreal . b' as Element of NAT ;
absreal . d' = absint . e by Def6;
then reconsider d = absreal . d' as Element of NAT ;
d * c >= 1 * c by A15, Lm6, NAT_1:4;
hence (absreal . (q1' - q2')) * (absreal . b') >= absreal . b' ; :: thesis: verum
end;
A17: abs b = absint . b by Th1
.= absreal . b by Def6 ;
- (r1' - r2') > 0 by A14, XREAL_1:60;
then A18: r2' - r1' = abs ((q1' - q2') * b') by A2, A5, ABSVALUE:def 1
.= (abs (q1' - q2')) * (abs b') by COMPLEX1:151
.= (absreal . (q1' - q2')) * (abs b') by EUCLID:def 2
.= (absreal . (q1' - q2')) * (absreal . b') by EUCLID:def 2 ;
r2' + (- r1') <= r2' + 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