let a, b be Element of INT.Ring ; :: thesis: ( b <> 0. INT.Ring implies a = ((a div b) * b) + (a mod b) )
assume A1: b <> 0. INT.Ring ; :: thesis: a = ((a div b) * b) + (a mod b)
consider d being Element of INT.Ring such that
A2: d = a div b ;
consider c being Element of INT.Ring such that
A3: c = a mod b ;
consider r being Element of INT.Ring such that
A4: ( a = (d * b) + r & 0. INT.Ring <= r & r < abs b ) by A1, A2, Def7;
consider q being Element of INT.Ring such that
A5: ( a = (q * b) + c & 0. INT.Ring <= c & c < abs b ) by A1, A3, Def8;
thus a = ((a div b) * b) + (a mod b) by A1, A2, A3, A4, A5, Th2; :: thesis: verum