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 ;
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 ;
A8: a = (mm * t) - (mm * (xx * n)) by
.= 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 ;
A10: a = (- (mm * t)) - (mm * (xx * n)) by
.= 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 ; :: 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 ;
hence a gcd b divides |.(a + (xx * b)).| by ; :: 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 ;
hence a gcd b divides |.(a + (xx * b)).| by ; :: thesis: verum
end;
end;
end;
then |.(a + (xx * b)).| gcd |.b.| = a gcd b by ;
hence (a + (xx * b)) gcd b = a gcd b by INT_2:34; :: thesis: verum