let a, b be Element of INT.Ring; :: according to INT_3:def 9 :: thesis: ( b <> 0. INT.Ring implies 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 ; :: thesis: ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )
per cases ( 0 <= b or b < 0 ) ;
suppose 0 <= b ; :: thesis: ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )
hence ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) by A1, Lm2; :: thesis: verum
end;
suppose A2: b < 0 ; :: thesis: ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )
reconsider c = - b as Element of INT.Ring ;
0 < - b by A2, XREAL_1:58;
then consider q, r being Element of INT.Ring such that
A3: a = (q * c) + r and
A4: ( r = 0. INT.Ring or absint . r < absint . c ) by Lm2;
A5: ( r = 0. INT.Ring or absint . r < absint . b )
proof
assume A6: r <> 0. INT.Ring ; :: thesis: absint . r < absint . b
absint . c = absreal . c by Def5
.= |.(- b).| by EUCLID:def 2
.= - b by A2, ABSVALUE:def 1
.= |.b.| by A2, ABSVALUE:def 1
.= absreal . b by EUCLID:def 2
.= absint . b by Def5 ;
hence absint . r < absint . b by A4, A6; :: thesis: verum
end;
reconsider t = - q as Element of INT.Ring ;
(t * b) + r = a by A3;
hence ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) by A5; :: thesis: verum
end;
end;