let a, b be Nat; :: thesis: for x being Integer st a <> 0 holds
(a + (x * b)) gcd b = a gcd b
let xx be Integer; :: thesis: ( a <> 0 implies (a + (xx * b)) gcd b = a gcd b )
set i = a gcd b;
A1: b = |.b.| by ABSVALUE:def 1;
assume A2: a <> 0 ; :: thesis: (a + (xx * b)) gcd b = a gcd b
A3: for m being Nat st m divides |.(a + (xx * b)).| & m divides |.b.| holds
m divides a gcd b

proof

let mm be Nat; :: thesis: ( mm divides |.(a + (xx * b)).| & mm divides |.b.| implies mm divides a gcd b )
assume that
A4: mm divides |.(a + (xx * b)).| and
A5: mm divides |.b.| ; :: thesis: mm divides a gcd b
consider n being Nat such that
A6: b = mm * n by A1, A5, NAT_D:def 3;
reconsider mm = mm as Element of NAT by ORDINAL1:def 12;

now :: thesis: mm divides a

per cases ( a + (xx * b) >= 0 or a + (xx * b) < 0 ) ;

suppose a + (xx * b) >= 0 ; :: thesis: mm divides a

then |.(a + (xx * b)).| = a + (xx * b) by ABSVALUE:def 1;
then consider t being Integer such that
A7: a + (xx * b) = mm * t by A4, INT_1:def 3;
A8: a = (mm * t) - (mm * (xx * n)) by A6, A7, XCMPLX_1:26
.= mm * (t - (xx * n)) ;
then t - (xx * n) >= 0 by A2;
then reconsider tt = t - (xx * n) as Element of NAT by INT_1:3;
a = mm * tt by A8;
hence mm divides a by NAT_D:def 3; :: thesis: verum

end;

suppose a + (xx * b) < 0 ; :: thesis: mm divides a

then |.(a + (xx * b)).| = - (a + (xx * b)) by ABSVALUE:def 1;
then consider t being Integer such that
A9: - (a + (xx * b)) = mm * t by A4, INT_1:def 3;
A10: a = (- (mm * t)) - (mm * (xx * n)) by A6, A9, XCMPLX_1:26
.= mm * ((- t) - (xx * n)) ;
then (- t) - (xx * n) >= 0 by A2;
then reconsider tt = (- t) - (xx * n) as Element of NAT by INT_1:3;
a = mm * tt by A10;
hence mm divides a by NAT_D:def 3; :: thesis: verum

end;

end;

end;

hence mm divides a gcd b by A1, A5, NEWTON:50; :: thesis: verum

end;

a gcd b divides a by NAT_D:def 5;
then A11: a = (a gcd b) * (a div (a gcd b)) by NAT_D:3;
A12: a gcd b divides b by NAT_D:def 5;
then A13: b = (a gcd b) * (b div (a gcd b)) by NAT_D:3;
a gcd b divides |.(a + (xx * b)).|

proof

per cases ( a + (xx * b) < 0 or a + (xx * b) >= 0 ) ;

suppose a + (xx * b) < 0 ; :: thesis: a gcd b divides |.(a + (xx * b)).|

then A14: |.(a + (xx * b)).| = - (a + (xx * b)) by ABSVALUE:def 1;
- (a + (xx * b)) = (a gcd b) * (- ((a div (a gcd b)) + (xx * (b div (a gcd b))))) by A11, A13;
hence a gcd b divides |.(a + (xx * b)).| by A14, INT_1:def 3; :: thesis: verum

end;

suppose a + (xx * b) >= 0 ; :: thesis: a gcd b divides |.(a + (xx * b)).|

then A15: |.(a + (xx * b)).| = a + (xx * b) by ABSVALUE:def 1;
a + (xx * b) = (a gcd b) * ((a div (a gcd b)) + (xx * (b div (a gcd b)))) by A11, A13;
hence a gcd b divides |.(a + (xx * b)).| by A15, INT_1:def 3; :: thesis: verum

end;

end;

end;

then |.(a + (xx * b)).| gcd |.b.| = a gcd b by A1, A12, A3, NAT_D:def 5;
hence (a + (xx * b)) gcd b = a gcd b by INT_2:34; :: thesis: verum