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

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)).|

hence (a + (xx * b)) gcd b = a gcd b by INT_2:34; :: thesis: verum

(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

a gcd b divides a
by NAT_D:def 5;
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;

end;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 aend;

hence
mm divides a gcd b
by A1, A5, NEWTON:50; :: thesis: verumper cases
( a + (xx * b) >= 0 or a + (xx * b) < 0 )
;

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

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;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

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;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

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
end;

then
|.(a + (xx * b)).| gcd |.b.| = a gcd b
by A1, A12, A3, NAT_D:def 5;per cases
( a + (xx * b) < 0 or a + (xx * b) >= 0 )
;

end;

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;- (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

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;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

hence (a + (xx * b)) gcd b = a gcd b by INT_2:34; :: thesis: verum