take absint ; :: according to INT_3:def 8 :: thesis: for a, b being Element of INT.Ring st b <> 0. INT.Ring holds
ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) )
let a, b be Element of INT.Ring; :: 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 ) ) )
reconsider b9 = b as Integer ;
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 ) )
now :: thesis: ( ( 0 <= b9 & ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) ) or ( b9 < 0 & 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 <= b9 or b9 < 0 ) ;
case 0 <= b9 ; :: 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;
case A2: b9 < 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 = - b9 as Element of INT.Ring by INT_1:def 2;
0 < - b9 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
.= |.(- b9).| by EUCLID:def 2
.= - b9 by A2, ABSVALUE:def 1
.= |.b9.| by A2, ABSVALUE:def 1
.= absreal . b9 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;
end;
hence ex q, r being Element of INT.Ring st
( a = (q * b) + r & ( r = 0. INT.Ring or absint . r < absint . b ) ) ; :: thesis: verum